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: [email protected] [mailto:glasgow-haskell-
| [email protected]] On Behalf Of Vladimir Reshetnikov
| Sent: 09 June 2009 13:48
| To: [email protected]
| Subject: Fwd: Unification for rank-N types
|
| Forwarding to GH list.
|
| ---------- Forwarded message ----------
| From: Vladimir Reshetnikov <[email protected]>
| Date: Tue, 9 Jun 2009 16:51:59 +0500
| Subject: Re: Unification for rank-N types
| To: haskell-cafe <[email protected]>
|
| 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 <[email protected]> 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
| >
| _______________________________________________
_______________________________________________
Glasgow-haskell-users mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
