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?
AntC
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
