Inductive kinds

[Simon Peyton-Jones]

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?

Simon


| -----Original Message-----
| From: glasgow-haskell-users-bounces at haskell.org
[mailto:glasgow-haskell-users-
| bounces at haskell.org] On Behalf Of Geoffrey Alan Washburn
| Sent: 06 August 2005 15:18
| To: glasgow-haskell-users at haskell.org
| 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 haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users