GHC 6.12.1 and impredicative polymorphism

[Dan Doel]

On Friday 30 October 2009 5:51:37 am Simon Peyton-Jones wrote:
> 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]!)

This may be a side issue, but...

Someone was asking in #haskell yesterday about what exactly ImpredicativeTypes 
did, as it's a bit difficult to tell at first. I eventually came to the 
conclusion that some of the notation GHC uses may be rather poor.

In a lambda cube/pure type system setting, the difference between an 
impredicative and predicative system are the rules:

   ([], *, *) vs. ([], *, [])

Where the first rule says that, for instance:

  (Pi a:*. a -> a) : *

while the second says:

  (Pi a:*. a -> a) : []

The first is impredicative due to * containing (Pi a:*. a -> a) itself, so the 
expression quantifies over a 'set' containing itself.

But, if we ask GHC the kind of:

  forall a. a -> a

it tells us the answer is *, even without ImpredicativeTypes. But that *looks* 
like a statement that the type system is impredicative already. And in fact, 
we can stick a signature on the identity function like:

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

which appears to allow impredicative instantiation of variables as long as 
they're only used in functions. But, of course, this fails for datatypes 
without the relevant flag. Maybe :: * -> *, but we're not allowed to apply it 
to (forall a. a -> a), even though GHC tells us the latter has type * 
(although, asking the kind of Maybe (forall a. a -> a) does not blow up; only 
trying to use it as a type does).

At some point in the discussion, someone quoted from the boxy paper that in 
HM, quantification ranges over monotypes. Presumably, GHC maintains such a 
distinction internally, which is roughly analogous[1] to tracking the 
difference between * and []. But, when it comes time to display sorts, it 
shows both * and [] as *, which makes it somewhat unclear why Maybe (forall a. 
a) is invalid.

So, to get to the point, whatever implementation is decided upon in the 
future, if predicativity is still around, I think it'd be useful to make that 
predicativity noticeable in the types/kinds/sorts, rather than the current 
situation, which to an observer looks like, "* contains both monotypes and 
polytypes, but quantification over * only really ranges over the monotypes 
(maybe)." I don't know how this would complicate GHC's current kind system, as 
I know it isn't set up like a pure type system, but it might be something to 
think about.

Cheers,
-- Dan

[1] It probably isn't a perfect correspondence. For instance (based on my 
experience implementing rather naive interpreters), in a predicative, lambda 
cube F2, the type:

  forall a. forall b. a -> b

is invalid, because 'forall b. a -> b' has sort [], and so the additional 
quantifier requires the rule ([],[],[]), which gets you to Fomega.

  forall a. (forall b. b) -> a = (forall b. b) -> (forall a. a)

are similarly invalid. But, it feels a bit accidental to me that the Fomega 
rule allows these, so one could probably keep a sort divide between monotypes 
and polytypes while allowing repeated and higher-rank quantification, and also 
not allowing higher-order types (although Haskell has the latter anyway).