[Haskell-cafe] Pointfree rank-2 typed function

[Bas van Dijk]

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
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[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

[Bas van Dijk]

On Tue, Nov 24, 2009 at 6:02 PM, Simon Peyton-Jones
<sim...@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.

[Martijn van Steenbergen]

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.

[Simon Peyton-Jones]

| 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/

[Heinrich Apfelmus]

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