Inductive kinds

[Geoffrey Alan Washburn]

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 at cis.upenn.edu|http://www.cis.upenn.edu/~geoffw/]