Simon Peyton-Jones wrote:
You mean something like 'datakind' in Tim Sheard's Omega?
Essentially.
Nothing is imminent. What I'd like to do, though, is to use data *types* at the type level, rather than reproduce the data-type declaration stuff at the kind level. Thus
data Nat = S Nat | Z
data Foo :: Nat -> * where Nil :: Foo Z Cons :: Int -> Foo n -> Foo (S n)
My dependent-type friends tell me that the paradoxes of "* has kind *" can be dealt with, but I don't understand the details yet. But as I say, nothing is very imminent.
why do you ask?
I have been looking at program extraction in Coq and was realizing that they probably do not need to do as much erasure, for the purposes of proof irrelevance, in their Haskell module now that GHC supports GADTs. With the addition of datakinds or some similar mechanism like you sketch above, it would be possible to achieve an even closer correspondence. -- [Geoff Washburn|geoffw@cis.upenn.edu|http://www.cis.upenn.edu/~geoffw/]