Simon Peyton-Jones <simonpj <at>
microsoft.com> writes:
>
> There is a little, ill-documented, sub-kind hierarchy in GHC. I'm trying
hard to get rid of it as much as
> possible, and it is much less important than it used to be. It's always been
there, and is nothing to do with polykinds.
>
> I've extended the commentary a bit: see "Types" and "Kinds" here
>
http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler
>
> The ArgKind thing has gone away following Max's recent unboxed-tuples patch,
so we now only have OpenKind
> (described on the above pages).
It's not that I have a specific problem (requirement) I'm trying to solve.
It's more that I'm trying to understand how this ladder of
Sorts/Kinds/Types/values hangs together.
With Phantom types, we've been familiar for many years with uninhabited types,
so why are user-defined (promoted) Kinds/Types different?
The Singletons stuff shows there are use cases for mapping from uninhabited
types to values -- but it seems to need a lot of machinery (all those shadow
types and values). And indeed TypeRep maps from not-necessarily-inhabited
types to values.
Is it that we really need to implement type application in the surface
language to get it all to come together? Then we won't need functions applying
to dummy arguments whose only purpose is to carry a Type::Kind.
To give a tight example:
data MyNat = Z | S MyNat -- to be promoted
data ProxyNat (a :: MyNat) = ProxyNat -- :k ProxyNat :: MyNat -> *
proxyNat :: n -> ProxyNat n -- rejected: Kind mis-match
proxyNat _ = ProxyNat
The parallel of that with phantom types (and a class constraint for MyNat)
seems unproblematic -- albeit with Kind *.
Could we have :k (->) :: OpenKind -> * -> * -- why not?
I don't quite understand why you would want arbitrary kinded arguments, but only in negative position.
Internally its already more like (->) :: OpenKind -> OpenKind -> * at the moment. The changes simply permitted unboxed tuples in argument position, relaxing a previous restriction. OpenKind is just a superkind of * and #, not every kind. Kinds other than * and # just don't have a term level representation. (Well kind Constraint is inhabited by dictionaries for instances after a fashion, but you don't get to manipulate them directly.)
I'm a lot happier with the new plumbing than I was with the crap I've been able to write by hand over the years for natural number types/singletons, and I'm actually pretty happy with the fact that it makes it clearer that there is a distinction between the type level and the term level, and I can't say that I buy the idea of just throwing things open like that.
In particular, the "OpenKind" for all kinds that you seem to be proposing sounds more like letting (->) :: forall (a :: BOX?) (b :: BOX?). a -> b -> * (or (->) :: forall (a :: BOX?). a -> * -> *) than OpenKind, which exists to track where unboxed types can lurk until polymorphism forces it to *.
With the 'more open' OpenKind you propose, it no longer collapses to * when used in a polymorphic fashion, but merely dumbs down to forall (a :: BOX). a, which strikes me as a particularly awkward transition. At the least, you'd need to actually break the 'BOX is the only superkind' rule to provide the quantification that can span over unboxed types and any boxed type, (scribbled as BOX? above).
That seems to be a pretty big mess for something that can be solved readily with simpler tools.
Mind you there is another case for breaking the BOX is the only superkind rule (that is the horrible syntax hack that requires monomorphization of the kinds of the results of type/data families can be cleaned up), but once you have more than one superkind, you start complicating type equality, needing other coercions, so it really shouldn't be done lightly.
-Edward
] 
RSS Feed