Geoffrey Alan Washburn
geoffw at cis.upenn.edu
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 cis.upenn.edu|http://www.cis.upenn.edu/~geoffw/]
More information about the Glasgow-haskell-users