[Haskell-cafe] type universes (was Re: MPTC inheritance

[wren ng thornton]

Larry Evans wrote:
> Except that a kind sounds like a universe at level 2 or 3.
> IOW, I guess haskell types are at level 1, and kines at level 2?
> Then I guess values would be at level 0?

Exactly.

> Is there some version of haskell that has more levels in its
> type universe.  If not, it there some reason for that
> limitation?

The language you're looking for is called Omega:

     http://web.cecs.pdx.edu/~sheard/Omega/index.html
     http://code.google.com/p/omega/
     http://web.cecs.pdx.edu/~sheard/

And as the name implies, the levels go all the way to the top.


> Is there some reference explaining the relationship
> of haskell types to nuprl type universes?


That one I can't help with :)

-- 
Live well,
~wren