simonpj at microsoft.com
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 haskell.org
| 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
More information about the Glasgow-haskell-users