GHC and Kinds

[Steffen Mazanek]

Hello,

> It means that Kinds are represented by Types.
> 
> Admittedly, Kinds only use a small fragment of what Types can represent,
> namely Arrow, and type constructor applications.  So * is represented by
> a TyConApp with a TyCon that is called typeCon.
> 
> The really annoying thing about Kinds is that there's occasionally a bit
> of sub-kinding.  In particular
> 
> 	error :: forall a. String -> a
> 
> We want to allow 
> 	error "foo" :: Int#

I have subkinding in my calculus as well, but in a completely
different context. For instance, the kind of Either is
+ -> + -> * because Either is covariant in its arguments.
But the kind of Either is also x -> x -> * (x=invariance).
So we have + -> + -> * as the most specific kind of Either.
Note, that the kind arrow in my system is contravariant 
as well. I think, that is a nice analogy to the type
system. 
For example, let tau_1:(x -> *) -> *, tau_2:(+ -> *) -> *.
Then tau_1 is usable whenever tau_2 is in operation.
So from (+ -> *) <: (x -> *) it follows in my system, that
(x -> *) -> * <: (+ -> *) -> *. Unfortunately I have to
decide two contexts of the kind arrow. To understand this,
consider my definition of kinds:

Def.: Kinds are inductively defined as follows:
* is a kind
if kappa1 and kappa2 are kinds, then kappa1 -> kappa2 is a kind
if kappa is a kind, then + -> kappa, - -> kappa, x -> kappa and
alpha -> kappa
alpha is a so-called kind variable, that can be instantiated
by +, - or x (not by arbitrary kinds!). Further on, we have the
convention, that * -> kappa has to be seen as x -> kappa.

What do we mean by the term kind variable?
A type tau may have the kind (alpha->beta->*)->alpha->beta->*. If
one applies this type, e.g., to the arrow type constructor
one gaines (tau (->)): - -> + -> *. So information about variances
is propagated. This allows for subtyping in a convenient manner.

> so the kind of 'a' can't be *, nor # (the kind of unboxed types).  It's
> an "open" kind, written "?"; both * and # are sub-kinds of ?.

I have read about this issue in the sources of the GHC. I try to
understand...

> You should nevertheless be able to encode your kind system in the same
> way as GHC does.

This is a pity, because my kind system allows for a really
nice type inference algorithm, that can deal with higher-kinded
types properly. I hope, that I can transfer it to the GHC.
I will write a short section for the commentary as soon as
I completely understand the GHC kind system.

> But I have been thinking that it's over-kill to use Types for Kinds, and
> leads to no real saving.

I think so, too, because the system from "Typing Haskell
in Haskell" is very easy to understand and extend. Another
advantage is, that it is closer to the Haskell report.

> I may well split the two types in the future.

This would be great.

Thank you for the informations,

Steffen Mazanek