[Haskell-cafe] Musings on type systems
wren ng thornton
wren at freegeek.org
Fri Nov 19 21:25:00 EST 2010
On 11/19/10 4:05 PM, Andrew Coppin wrote:
> So what would happen if some crazy person decided to make the kind
> system more like the type system? Or make the type system more like the
> value system? Do we end up with another layer to our cake? Is it
> possible to generalise it to an infinite number of layers?
In addition to the Coq and Agda notion of "universes" you should also
look at Tim Sheard's Omega[1], which takes Haskell and then goes all the
way up.
[1] http://web.cecs.pdx.edu/~sheard/papers/SumSchNotes.ps
--
Live well,
~wren
More information about the Haskell-Cafe
mailing list