GHC 6.12.1 and impredicative polymorphism
Dan Doel
dan.doel at gmail.com
Fri Nov 13 17:58:54 EST 2009
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).
More information about the Glasgow-haskell-users
mailing list