arbitrary rank polymorphism and ghc language pragmas

[richard murphy-3]

Hi All:

I've been working through some details in these papers [1], [2] and
noticed a language pragma configuration that I hope you can confirm.

When using explicit foralls in a data constructor, it appears that GHC
7.4.2 requires Rank2Types in the Language pragma for what the papers
consider rank 1 types.

Here's an example:

data T = TC (forall a b. a -> b -> a)

Am I correct, or is there another extension? The ExplicitForAll does not
appear to support rank 1 types in data constructors.

1. Practical Type Inference for Arbitrary-Rank Types.
2. A Direct Algorithm for Type Inference in the Rank 2 Fragment of the
Second-Order Lambda Calculus.

--
Rick


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Francesco Mazzoli]

At Thu, 05 Jul 2012 11:18:00 -0400,
rickmurphy  wrote:
> data T = TC (forall a b. a -> b -> a)

The type of `TC' will be `(forall a b. a -> b -> a) -> T', a Rank-2
type.

--
Francesco * Often in error, never in doubt

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Twan van Laarhoven]

On 05/07/12 17:18, rickmurphy wrote:

> Hi All:
>
> I've been working through some details in these papers [1], [2] and
> noticed a language pragma configuration that I hope you can confirm.
>
> When using explicit foralls in a data constructor, it appears that GHC
> 7.4.2 requires Rank2Types in the Language pragma for what the papers
> consider rank 1 types.
>
> Here's an example:
>
> data T = TC (forall a b. a -> b -> a)
>
> Am I correct, or is there another extension? The ExplicitForAll does not
> appear to support rank 1 types in data constructors.

There is the PolymorphicComponents extension precisely for this use case.


Twan



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[richard murphy-3]

Thanks Francesco. And I did verify that ExplicitForAll does in fact
allow Rank 1 Types in functions like the following ...

f :: (forall a. a -> a)

--
Rick

On Thu, 2012-07-05 at 16:28 +0100, Francesco Mazzoli wrote:

> At Thu, 05 Jul 2012 11:18:00 -0400,
> rickmurphy  wrote:
> > data T = TC (forall a b. a -> b -> a)
>
> The type of `TC' will be `(forall a b. a -> b -> a) -> T', a Rank-2
> type.
>
> --
> Francesco * Often in error, never in doubt
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe