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|[EMAIL PROTECTED]|http://www.cis.upenn.edu/~geoffw/]
_______________________________________________
Glasgow-haskell-users mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
