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
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/put... 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@haskell.org [mailto:haskell-cafe-bounces@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
On Tue, Nov 24, 2009 at 6:02 PM, 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/put...
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
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/put...
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.
| 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/
Simon Peyton-Jones wrote:
| 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.
I tried to use impredicative polymorphism once to create polymorphic values inside a monad, similar to the following (silly) example foo :: IO (∀a. a -> a) foo = do ref <- newIORef id -- ref :: IO (∀a. a -> a) readIORef ref (Fortunately, it turned out that this was not what I needed anyway.) Generally, it seems to me that all polymorphically typed EDSLs require impredicative polymorphism. After all, they are usually embedded with some kind of functor F (= Expr, IO, Parser, ...) and polymorphically typed means that you want types like F (∀a. a :~> a) and so on. Of course, we don't have (m)any examples of polymorphically typed DSLs yet, but it would be handy to have support for impredicativity in GHC if someone stumbles upon a useful one. Regards, apfelmus -- http://apfelmus.nfshost.com
participants (4)
-
Bas van Dijk -
Heinrich Apfelmus -
Martijn van Steenbergen -
Simon Peyton-Jones