On Mon, Jun 11, 2012 at 9:58 PM, AntC <span dir="ltr"><<a href="mailto:anthony_clayden@clear.net.nz" target="_blank">anthony_clayden@clear.net.nz</a>></span> wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="im">Simon Peyton-Jones <simonpj <at> <a href="http://microsoft.com" target="_blank">microsoft.com</a>> writes:<br>
<br>
><br>
> There is a little, ill-documented, sub-kind hierarchy in GHC. I'm trying<br>
hard to get rid of it as much as<br>
> possible, and it is much less important than it used to be. It's always been<br>
there, and is nothing to do with polykinds.<br>
><br>
> I've extended the commentary a bit: see "Types" and "Kinds" here<br>
> <a href="http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler" target="_blank">http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler</a><br>
><br>
> The ArgKind thing has gone away following Max's recent unboxed-tuples patch,<br>
so we now only have OpenKind<br>
> (described on the above pages).<br>
<br>
</div>Thank you Simon, Richard, ~d, et al (so much kindness to a stranger!)<br>
<br>
It's not that I have a specific problem (requirement) I'm trying to solve.<br>
It's more that I'm trying to understand how this ladder of<br>
Sorts/Kinds/Types/values hangs together.<br>
<br>
With Phantom types, we've been familiar for many years with uninhabited types,<br>
so why are user-defined (promoted) Kinds/Types different?<br>
<br>
The Singletons stuff shows there are use cases for mapping from uninhabited<br>
types to values -- but it seems to need a lot of machinery (all those shadow<br>
types and values). And indeed TypeRep maps from not-necessarily-inhabited<br>
types to values.<br>
<br>
Is it that we really need to implement type application in the surface<br>
language to get it all to come together? Then we won't need functions applying<br>
to dummy arguments whose only purpose is to carry a Type::Kind.<br>
<br>
To give a tight example:<br>
<br>
data MyNat = Z | S MyNat -- to be promoted<br>
<br>
data ProxyNat (a :: MyNat) = ProxyNat -- :k ProxyNat :: MyNat -> *<br>
<br>
proxyNat :: n -> ProxyNat n -- rejected: Kind mis-match<br>
proxyNat _ = ProxyNat<br>
<br>
The parallel of that with phantom types (and a class constraint for MyNat)<br>
seems unproblematic -- albeit with Kind *.<br>
<br>
Could we have :k (->) :: OpenKind -> * -> * -- why not?</blockquote><div><br></div><div><div>I don't quite understand why you would want arbitrary kinded arguments, but only in negative position. </div></div>
<div><br></div><div>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.)</div>
<div><br></div><div>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.</div>
<div><br></div><div>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 *.</div>
<div><br></div><div>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). </div>
<div><br></div><div>That seems to be a pretty big mess for something that can be solved readily with simpler tools.</div><div><br></div><div>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.</div>
<div><br></div><div>-Edward</div></div>