[Haskell-cafe] Pointfree rank-2 typed function

[Simon Peyton-Jones]

It used to be, because GHC used to implement so-called "deep skolemisation".  See Section 4.6.2 of
http://research.microsoft.com/en-us/um/people/simonpj/papers/higher-rank/putting.pdf

Deep skolemisation was an unfortunate casualty of the push to add impredicative polymoprhism.  However, as I mentioned in an earlier email, I'm currently planning to take impredicative polymorphism *out*, which means that deep skolemisation might come back *in*. 

Simon

| -----Original Message-----
| From: haskell-cafe-bounces at haskell.org [mailto:haskell-cafe-bounces at haskell.org] On
| Behalf Of Bas van Dijk
| Sent: 24 November 2009 13:34
| To: Haskell Cafe
| Subject: [Haskell-cafe] Pointfree rank-2 typed function
| 
| Hello,
| 
| Given this program:
| 
| ------------------------------------------------------------
| {-# LANGUAGE Rank2Types #-}
| 
| newtype Region s a = Region a
| 
| unRegion :: forall a s. Region s a -> a
| unRegion (Region x) = x
| 
| runRegionPointfull :: forall a. (forall s. Region s a) -> a
| runRegionPointfull r = unRegion r
| ------------------------------------------------------------
| 
| Is it possible to write the rank-2 typed function 'runRegionPointfull'
| in pointfree style?
| 
| Unfortunately the following doesn't typecheck:
| 
| runRegionPointfree :: forall a. (forall s. Region s a) -> a
| runRegionPointfree = unRegion
| 
| Couldn't match expected type `forall s. Region s a'
|            against inferred type `Region s a1'
|     In the expression: unRegion
|     In the definition of `runRegionPointfree':
|         runRegionPointfree = unRegion
| 
| Why can't the typechecker match `forall s. Region s a' and `Region s a1'?
| 
| Thanks,
| 
| Bas
| _______________________________________________
| Haskell-Cafe mailing list
| Haskell-Cafe at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell-cafe