tipi superiori ordinati e impredicativa

Question

Voglio realizzare il stripPrefixBy seguente funzione:

-- psuedo code signature 
stripPrefixBy :: forall a. [forall b. a -> Maybe b] -> [a] -> Maybe [a] 
stripPrefixBy [] xs = Just xs 
stripPrefixBy _ [] = Nothing 
stripPrefixBy (p:ps) (x:xs) = case p x of 
    Just _ -> stripPrefixBy ps xs 
    Nothing -> Nothing 

res :: Maybe String 
res = stripPrefixBy [const (Just 0), Just] "abc" 

wantThisToBeTrue :: Bool 
wantThisToBeTrue = case res of 
    Just "c" -> True 
    _ -> False 

Ho provato con ImpredicativeTypes e RankNTypes, ma senza fortuna. Come posso implementare stripPrefixBy con il tipo che voglio avere?

Answer 1

Il problema con la vostra firma è che la lista passata a stripPrefixBy è dichiarata come una lista di funzioni che prendono un certo un come argomento, e quindi produrre un Maybe b per eventuali b le scelte del chiamante. Gli unici valori che le funzioni nell'elenco possono restituire sono ⊥, Nothing e Just ⊥.

Vale a dire, quando si utilizza il polimorfismo impredicativa, il forall non significa la stessa cosa che fa con un tipo esistenzialmente quantificata: lì, il forall è applicare al tipo di costruttore, cioè

data MyType = forall a. Foo a 
Foo :: forall a. a -> MyType 

ma qui, si dice che la funzione deve essere letteralmente di tipo forall b. a -> Maybe b.

Ecco un esempio corretto utilizzando un tipo esistenziale:

{-# LANGUAGE ExistentialQuantification #-} 

data Pred a = forall b. Pred (a -> Maybe b) 

stripPrefixBy :: [Pred a] -> [a] -> Maybe [a] 
stripPrefixBy [] xs = Just xs 
stripPrefixBy _ [] = Nothing 
stripPrefixBy (Pred p:ps) (x:xs) = case p x of 
    Just _ -> stripPrefixBy ps xs 
    Nothing -> Nothing 

res :: Maybe String 
res = stripPrefixBy [Pred $ const (Just 0), Pred Just] "abc" 

wantThisToBeTrue :: Bool 
wantThisToBeTrue = case res of 
    Just "c" -> True 
    _ -> False 

Credo che UHC supporta esprimere il tipo che si desidera direttamente, come

stripPrefixBy :: [exists b. a -> Maybe b] -> [a] -> Maybe [a] 

Answer 2

Un'altra risposta è: "Perché lo vuoi avere quel tipo? " Se sei felice di vincolare l'elenco delle funzioni (il primo argomento di stripPrefixBy) tutti di avere lo stesso tipo di risultato, è possibile usare, ad esempio

res :: Maybe String 
res = stripPrefixBy [const (Just undefined), Just] "abc" 

e poi dare stripPrefixBy il seguente tipo di Haskell98:

stripPrefixBy :: [a -> Maybe b] -> [a] -> Maybe [a] 

modo equivalente, si potrebbe osservare che i risultati delle funzioni del primo argomento non possono essere utilizzati (niente altro menziona tipo "b"), così si potrebbe anche avere una lista di predicati:

stripPrefixBy :: [a -> Bool] -> [a] -> Maybe [a] 
stripPrefixBy [] xs = Just xs 
stripPrefixBy _ [] = Nothing 
stripPrefixBy (p:ps) (x:xs) = case p x of 
    True -> stripPrefixBy ps xs 
    False -> Nothing 

res :: Maybe String 
res = stripPrefixBy (map (isJust.) [const (Just undefined), Just]) "abc" 

isJust :: Maybe a -> Bool 
isJust (Just _) = True 
isJust Nothing = False 

Ma forse questa domanda è l'astrazione di un problema più complicato che hai, e la risposta più semplice non funzionerà? Tutto dovrebbe essere il più semplice possibile, ma non più semplice.