problems with impredicativity

[Simon Peyton-Jones]

Wolfgang

Dimitrios, Stephanie and I spent a long time trying to come up with a decent story for impredicative polymorphism (which would let you use types like [forlall a. a->a]), wrote several papers about it, and even implemented one version in GHC (hence -XImpredicativeTypes).

However the implementation was Just Too Complicated, and its specification was too unpredictable.  So during the last major overhaul of the type inference engine, I took most of it out. 

The most promising approach is, I think, Dimitrios and Claudio's QML idea (http://research.microsoft.com/en-us/um/people/crusso/qml/).  It's less ambitious than our earlier schemes, but it is much simpler.

GHC currently implements a kind of half-way house. We have simply not devoted serious attention to the story for impredicative types, yet.  Too busy with type functions and other stuff that has seemed more immediately useful.  So I'm afraid I make no warranty for a sensible, predicable behaviour when you are using impredicativity.

If you care about this, add yourself to the cc list for the ticket
	http://hackage.haskell.org/trac/ghc/ticket/4295
explain why it's important to you, and attach a test case showing the kind of thing you wanted to be able to do.  The more motivating examples, the greater the incentive to fix it.

Simon

|  -----Original Message-----
|  From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-users-
|  bounces at haskell.org] On Behalf Of Wolfgang Jeltsch
|  Sent: 04 November 2011 22:13
|  To: glasgow-haskell-users at haskell.org
|  Subject: problems with impredicativity
|  
|  Hello,
|  
|  this code is accepted by GHC 7.0.4:
|  
|  > {-# LANGUAGE ImpredicativeTypes #-}
|  >
|  > polyId :: (forall a. a) -> a
|  > polyId x = x
|  >
|  > polyIdMap :: [forall a. a] -> [forall a. a]
|  > polyIdMap xs = fmap polyId xs
|  
|  However, this one isn’t:
|  
|  > {-# LANGUAGE ImpredicativeTypes #-}
|  >
|  > polyId :: (forall a. Maybe a) -> Maybe a
|  > polyId x = x
|  >
|  > polyIdMap :: [forall a. Maybe a] -> [forall a. Maybe a]
|  > polyIdMap xs = fmap polyId xs
|  
|  Is there a way to make it accepted?
|  
|  Best wishes,
|  Wolfgang
|  
|  
|  _______________________________________________
|  Glasgow-haskell-users mailing list
|  Glasgow-haskell-users at haskell.org
|  http://www.haskell.org/mailman/listinfo/glasgow-haskell-users