RE: [Haskell-cafe] Pointfree rank-2 typed function
| Are there workarounds for uses of impredicative types, or do we lose the | ability to express certain programs as a result? There's usually a workaround. I include the msg I sent below. Simon -Original Message- From: Simon Peyton-Jones Sent: 30 October 2009 09:52 To: GHC users Cc: Dimitrios Vytiniotis Subject: GHC 6.12.1 and impredicative polymorphism Friends One more update about GHC 6.12, concerning impredicative polymorphism. GHC has had an experimental implementation of impredicative polymorphism for a year or two now (flag -XImpredicativePolymorphism). But a) The implementation is ridiculously complicated, and the complexity is pervasive (in the type checker) rather than localized. I'm very unhappy about this, especially as we add more stuff to the type checker for type families. b) The specification (type system) is well-defined [1], but is also pretty complicated, and it's just too hard to predict which programs will typecheck and which will not. So it's time for a re-think. I propose to deprecate it in 6.12, and remove it altogether in 6.14. We may by then have something else to put in its place. (There is no lack of candidates [2,3,4]!) Fortunately, I don't think a lot of people use the feature in anger. Please yell if you *are* using impredicative polymorphism for something serious. But if you are, we need to think of a workaround. The current situation seems unsustainable. Simon [1] http://research.microsoft.com/en-us/um/people/simonpj/papers/boxy/ [2] http://research.microsoft.com/en-us/um/people/crusso/qml/ [3] http://research.microsoft.com/en-us/um/people/daan/pubs.html [4] http://gallium.inria.fr/~remy/mlf/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] Pointfree rank-2 typed function
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-boun...@haskell.org
[mailto:haskell-cafe-boun...@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@haskell.org
| http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Pointfree rank-2 typed function
On Tue, Nov 24, 2009 at 6:02 PM, Simon Peyton-Jones simo...@microsoft.com wrote: 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*. Ok nice because I'm very used to refactor code like: 'f x = g x' to 'f = g' for all f and g. Thanks, Bas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Pointfree rank-2 typed function
Simon Peyton-Jones wrote: 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*. Are there workarounds for uses of impredicative types, or do we lose the ability to express certain programs as a result? Thanks, Martijn. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
