RE: Unification for rank-N types

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