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]