Inductive kinds

Geoffrey Alan Washburn geoffw at
Mon Aug 8 09:50:05 EDT 2005

Simon Peyton-Jones wrote:

 > You mean something like 'datakind' in Tim Sheard's Omega?

 > 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 

[Geoff Washburn|geoffw at|]

More information about the Glasgow-haskell-users mailing list