Inductive kinds

Simon Peyton-Jones simonpj at
Mon Aug 8 09:37:07 EDT 2005

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?


| -----Original Message-----
| From: glasgow-haskell-users-bounces at
| bounces at] On Behalf Of Geoffrey Alan Washburn
| Sent: 06 August 2005 15:18
| To: glasgow-haskell-users at
| Subject: Inductive kinds
| 	Are there any plans for inductively defined kinds in some future
| version of GHC?
| _______________________________________________
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users at

More information about the Glasgow-haskell-users mailing list