Simple example for ImpredicativeTypes

Question

The GHC user's guide describes the impredicative polymorphism extension with reference to the following example:

f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
f (Just g) = Just (g [3], g "hello")
f Nothing  = Nothing

However, when I define this example in a file and try to call it, I get a type error:

ghci> f (Just reverse)

<interactive>:8:9:
    Couldn't match expected type `forall a. [a] -> [a]'
                with actual type `[a0] -> [a0]'
    In the first argument of `Just', namely `reverse'
    In the first argument of `f', namely `(Just reverse)'
    In the expression: f (Just reverse)
ghci> f (Just id)

<interactive>:9:9:
    Couldn't match expected type `forall a. [a] -> [a]'
                with actual type `a0 -> a0'
    In the first argument of `Just', namely `id'
    In the first argument of `f', namely `(Just id)'
    In the expression: f (Just id)

Seemingly only undefined, Nothing, or Just undefined satisfies the type-checker.

I have two questions, therefore:

• Can the above function be called with Just f for any non-bottom f?
• Can someone provide an example of a value only definable with impredicative polymorphism, and usable in a non-trivial way?

The latter is particularly with the HaskellWiki page on Impredicative Polymorphism in mind, which currently makes a decidedly unconvincing case for the existence of the extension.

Antung

Interesting. It's acceptable to say forall a. [a] -> [a]. forall a. Maybe ([a] -> [a]) fails, because the type checker seems to try to instantiate a to both Int and Char. Maybe (forall a. [a] -> [a]) fails, because it expects forall a. [a] -> [a], but it gets a [a0] -> [a0] where a0 is fresh. So, with Maybe, the nested type scheme is only instantiated once, but without Maybe, everything is just fine. – Primp

Answer 1

Here's an example of how one project, const-math-ghc-plugin, uses ImpredicativeTypes to specify a list of matching rules.

The idea is that when we have an expression of the form App (PrimOp nameStr) (Lit litVal), we want to look up the appropriate rule based upon the primop name. A litVal will be either a MachFloat d or MachDouble d (d is a Rational). If we find a rule, we want to apply the function for that rule to d converted to the correct type.

The function mkUnaryCollapseIEEE does this for unary functions.

mkUnaryCollapseIEEE :: (forall a. RealFloat a => (a -> a))
                    -> Opts
                    -> CoreExpr
                    -> CoreM CoreExpr
mkUnaryCollapseIEEE fnE opts expr@(App f1 (App f2 (Lit lit)))
    | isDHash f2, MachDouble d <- lit = e d mkDoubleLitDouble
    | isFHash f2, MachFloat d  <- lit = e d mkFloatLitFloat
    where
        e d = evalUnaryIEEE opts fnE f1 f2 d expr

The first argument needs to have a Rank-2 type, because it will be instantiated at either Float or Double depending on the literal constructor. The list of rules looks like this:

unarySubIEEE :: String -> (forall a. RealFloat a => a -> a) -> CMSub
unarySubIEEE nm fn = CMSub nm (mkUnaryCollapseIEEE fn)

subs =
    [ unarySubIEEE "GHC.Float.exp"    exp
    , unarySubIEEE "GHC.Float.log"    log
    , unarySubIEEE "GHC.Float.sqrt"   sqrt
    -- lines omitted
    , unarySubIEEE "GHC.Float.atanh"  atanh
    ]

This is ok, if a bit too much boilerplate for my taste.

However, there's a similar function mkUnaryCollapsePrimIEEE. In this case, the rules are different for different GHC versions. If we want to support multiple GHCs, it gets a bit tricky. If we took the same approach, the subs definition would require a lot of CPP, which can be unmaintainable. Instead, we defined the rules in a separate file for each GHC version. However, mkUnaryCollapsePrimIEEE isn't available in those modules due to circular import issues. We could probably re-structure the modules to make it work, but instead we defined the rulesets as:

unaryPrimRules :: [(String, (forall a. RealFloat a => a -> a))]
unaryPrimRules =
    [ ("GHC.Prim.expDouble#"    , exp)
    , ("GHC.Prim.logDouble#"    , log)
    -- lines omitted
    , ("GHC.Prim.expFloat#"     , exp)
    , ("GHC.Prim.logFloat#"     , log)
    ]

By using ImpredicativeTypes, we can keep a list of Rank-2 functions, ready to use for the first argument to mkUnaryCollapsePrimIEEE. The alternatives would be much more CPP/boilerplate, changing the module structure (or circular imports), or a lot of code duplication. None of which I would like.

I do seem to recall GHC HQ indicating that they would like to drop support for the extension, but perhaps they've reconsidered. It is quite useful at times.

Limburg

Now both halves of my question are answered, but unfortunately not both in the same answer :) I'm accepting this one anyway, thanks! – Antung

Answer 2

Isn't it just that ImpredicativeTypes has been quietly dropped with the new typechecker in ghc-7+ ? Note that ideone.com still uses ghc-6.8 and indeed your program use to run fine :

{-# OPTIONS -fglasgow-exts  #-}

f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
f (Just g) = Just (g [3], g "hello")
f Nothing  = Nothing

main   = print $ f (Just reverse)

prints Just ([3],"olleh") as expected; see http://ideone.com/KMASZy

augustss gives a handsome use case -- some sort of imitation Python dsl -- and a defense of the extension here: http://augustss.blogspot.com/2011/07/impredicative-polymorphism-use-case-in.html referred to in the ticket here http://hackage.haskell.org/trac/ghc/ticket/4295

Divot

f requires ImpredicativeTypes to compile (if I give only RankNTypes, GHC even suggests the extension), so it certainly hasn't been completely dropped. – Antung

Yes, it immediately requires you to use the extension if you attempt the syntax Maybe (forall a . [a] -> [a]), as it used to do; but then it ignores the plain meaning of the signature, except in some vestigial cases. – Divot

I have some code that uses ImpredicativeTypes to achieve rules :: [(String, (forall a. RealFloat a => a -> a))], which works fine with ghc-7.6. The alternatives appear much less attractive. – Limburg

@JohnL: that would actually answer my second question if you want to post a quick summary. – Antung

Doesn't Lennart A's discussion answer your second question? A revision of your function following John L's works fine g :: [(Int, forall a. [a] -> [a])] -> Maybe ([Int], [Char]); g [] = Nothing ; g ((n,ff):nfs) = Just (ff [3], ff "hello") My thought was that you don't want to depend on it working in ghc-7.8 – Divot

Answer 3

Note this workaround:

justForF :: (forall a. [a] -> [a]) -> Maybe (forall a. [a] -> [a])
justForF = Just

ghci> f (justForF reverse)
Just ([3],"olleh")

Or this one (which is basically the same thing inlined):

ghci> f $ (Just :: (forall a. [a] -> [a]) -> Maybe (forall a. [a] -> [a])) reverse
Just ([3],"olleh")

Seems like the type inference has problems infering the type of the Just in your case and we have to tell it the type.

I have no clue if it's a bug or if there is a good reason for it.. :)

Fordone

Thanks, that's interesting! I had already tried annotating reverse but in retrospect that wasn't going to work. I won't accept this answer yet, though, because this solution is, uh, kind of icky :P – Antung

Impredicative polymorphism does not play nice with HM style typing. Universal types are in a sense "opened" automatically in Haskell and similar languages. That is, type variables are quantified at the outermost level. – Appendant