Higher ranked and impredicative types

Question

I want to implement the following stripPrefixBy function:

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

I've tried using ImpredicativeTypes and RankNTypes but without luck. How can I implement stripPrefixBy with the type I want it to have?

Answer 1

The problem with your signature is that the list passed to stripPrefixBy is declared as a list of functions which take a certain a as an argument, and then produce a Maybe b for any b the caller picks. The only values the functions in the list are allowed to return are ⊥, Nothing and Just ⊥.

That is to say, when using impredicative polymorphism, the forall doesn't mean the same thing it does with an existentially quantified type: there, the forall is applying to the type of the constructor, i.e.

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

but here, it's saying that the function must literally be of type forall b. a -> Maybe b.

Here's a corrected example using an existential type:

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

I believe that UHC supports expressing the type you want directly, as

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

Answer 2

Another response is, "why do you want it to have that type?" If you're happy to constrain the list of functions (the first argument of stripPrefixBy) all to have the same result type, you can use eg

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

and then give stripPrefixBy the following Haskell98 type:

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

Equivalently, you could observe that the results of the functions in the first argument cannot be used (nothing else mentions type "b"), so you might as well have a list of predicates:

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

But maybe this question is the abstraction of a more complicated problem you have, and the simpler response won't work? Everything should be as simple as possible, but no simpler.