Unification for rank-N types

Simon Peyton-Jones simonpj at microsoft.com
Fri Jun 12 19:28:30 EDT 2009


Vladimir

[NB: the subject line is wrong: this email is all about impredicativity, and not at all about higher-rank types.]

| This does not type-check:
| {-# LANGUAGE RankNTypes, ImpredicativeTypes #-}
| f :: [forall a. t a -> t a] -> t b -> t b
...
| But this, very similar, does type-check:

The short answer is that impredicative polymorphism in GHC are not fully implemented.  And even if it were, the specification is relatively complex.  For example, it's quite possible that
        e  and  (\x. e x)
don't behave the same from a typing point of view.  To be honest I'm not sure whether your program fails to typecheck because of a bug in GHC, or because the specification says it shouldn't.  (I'm travelling, so I can't check the spec.)  I'm ccing Dimitrios who will probably know.

The longer answer is this.  It has slowly become clear that there are many possible design choices that allow impredicative polymorphism to be mixed with type inference; indeed two new papers were published only last year (by Dimitrios and Daan).  To my mind it is still not clear what the best trade-off is; the solutions that are nicest for the programmer are really rather complicated to implement, and vice versa.

I am not convinced that the design choice currently embodied in GHC is the right one -- and the implementation turned out to get tangled up with already-complex bits of the typechecker, rather than being modularly separable.  So the current implementation is a mess: hard to understand, and hard to maintain.


So the current situation is that
        - impredicative polymorphism in GHC is only partially implemented,
        and almost certainly has bugs

        - I'm quite inclined to take it out altogether, for the reasons
        described above

        - In due course I'd like to put in some simple, robust, but perhaps
        somewhat less convenient, way to allow impredicative polymorphism,
        but I'm not quite sure what form it should take

Meanwhile I'd be interested to know

  * does anyone impredicative polymorphism in GHC (-XImpredicativeTypes)?

My perception is that very few people do, but I could be wrong, and if so I should be more careful about taking it out again!

Simon

| -----Original Message-----
| From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-
| users-bounces at haskell.org] On Behalf Of Vladimir Reshetnikov
| Sent: 09 June 2009 13:48
| To: glasgow-haskell-users at haskell.org
| Subject: Fwd: Unification for rank-N types
|
| Forwarding to GH list.
|
| ---------- Forwarded message ----------
| From: Vladimir Reshetnikov <v.reshetnikov at gmail.com>
| Date: Tue, 9 Jun 2009 16:51:59 +0500
| Subject: Re: Unification for rank-N types
| To: haskell-cafe <haskell-cafe at haskell.org>
|
| One more example:
|
| This does not type-check:
| -------------------------------------------------------
| {-# LANGUAGE RankNTypes, ImpredicativeTypes #-}
|
| f :: [forall a. t a -> t a] -> t b -> t b
| f = foldr (.) id
| -------------------------------------------------------
|
|     Couldn't match expected type `forall a. f a -> f a'
|            against inferred type `b -> c'
|     In the first argument of `foldr', namely `(.)'
|
| But this, very similar, does type-check:
| -------------------------------------------------------
| {-# LANGUAGE RankNTypes, ImpredicativeTypes #-}
|
| f :: [forall a. t a -> t a] -> t b -> t b
| f = foldr (\g -> (.) g) id
| -------------------------------------------------------
|
| What is the reason for this?
|
| Thanks,
| Vladimir
|
|
| On 6/9/09, Vladimir Reshetnikov <v.reshetnikov at gmail.com> wrote:
| > Hi,
| >
| > I have the following code:
| > -------------------------------------------------------
| > {-# LANGUAGE RankNTypes #-}
| >
| > f :: ((forall a. a -> a) -> b) -> b
| > f x = x id
| >
| > g :: (forall c. Eq c => [c] -> [c]) -> ([Bool],[Int])
| > g y = (y [True], y [1])
| >
| > h :: ([Bool],[Int])
| > h = f g
| > -------------------------------------------------------
| >
| > GHC rejects it:
| >     Couldn't match expected type `forall a. a -> a'
| >            against inferred type `forall c. (Eq c) => [c] -> [c]'
| >       Expected type: forall a. a -> a
| >       Inferred type: forall c. (Eq c) => [c] -> [c]
| >     In the first argument of `f', namely `g'
| >     In the expression: f g
| >
| > But, intuitively, this code is type-safe, and actually I can convince
| > the typechecker in it with the following workaround:
| > -------------------------------------------------------
| > h :: ([Bool],[Int])
| > h = let g' = (\(x :: forall a. a -> a) -> g x) in f g'
| > -------------------------------------------------------
| >
| > So, is the current behavior of GHC correct ot it is a bug?
| > How unification for rank-N types should proceed?
| >
| > Thanks,
| > Vladimir
| >
| _______________________________________________


More information about the Glasgow-haskell-users mailing list