clasificados Superior y impredicativas tipos

Question

que desea implementar el stripPrefixBy siguiente función:

-- 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 

He intentado usar ImpredicativeTypes y RankNTypes pero sin suerte. ¿Cómo puedo implementar stripPrefixBy con el tipo que quiero que tenga?

Answer 1

El problema con su firma es que la lista que se pasa a stripPrefixBy se declara como una lista de funciones que tienen una cierta un como un argumento, y luego producir un Maybe b para cualquier b los picos de llamadas. Los únicos valores de las funciones de la lista se le permitió regresar son ⊥, Nothing y Just ⊥.

Es decir, cuando se utiliza el polimorfismo impredicativo, la forall no significa lo mismo que lo hace con un tipo cuantificada existencialmente: allí, el forall está aplicando el tipo del constructor , es decir

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

pero aquí, es decir que la función debe ser, literalmente, de tipo forall b. a -> Maybe b.

Aquí está un ejemplo corregido utilizando un tipo existencial:

{-# 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 

Creo que UHC apoya expresando el tipo que desea directamente, como

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

Answer 2

Otra respuesta es, "¿por qué lo quieres tener ese tipo? " Si usted es feliz para restringir la lista de funciones (el primer argumento de stripPrefixBy) que todos tengan el mismo tipo de resultado, se puede utilizar por ejemplo

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

y luego dar stripPrefixBy el siguiente tipo de Haskell98:

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

de manera equivalente, se puede observar que los resultados de las funciones en el primer argumento no se pueden utilizar (nada más menciones de tipo "B"), por lo que también podría tener una lista de predicados:

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 

Pero tal vez esta pregunta es la abstracción de un problema más complicado que tiene, ¿y la respuesta más simple no funcionará? Todo debería ser lo más simple posible, pero no más sencillo.