Re: [Haskell-cafe] Musings on type systems

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