[Haskell-cafe] Musings on type systems

[wren ng thornton]

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