Kindness of strangers (or strangeness of Kinds)

[Edward Kmett]

On Mon, Jun 11, 2012 at 9:58 PM, AntC <anthony_clayden at clear.net.nz> wrote:

> 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).
>
> Thank you Simon, Richard, ~d, et al (so much kindness to a stranger!)
>
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120611/ecbe6452/attachment.htm>