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 _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
