>>>>> Samuel E Moelius, wrote (on Wed, 06 Aug 2003 at 15:35):
> On Wednesday, August 6, 2003, at 06:15 AM, C T McBride wrote:
>> This is why most sensible dependent type theories have a hierarchy of
>> universes behind the scenes. You can think of * in Haskell as the lowest
>> universe, inhabited by types.
> Why wouldn't terms be the lowest universe?
A universe is a type of types/set-like-things, modulo a pile of
subtleties. (The first of which is that it is actually a type of
codes for types.)
I think the term "universe", which afaik was introduced into type
theory by Martin-Lof, was chosen for its use in the foundations of
category theory in dealing with questions of "size"
(smallness/largeness).
Peter Hancock
_______________________________________________
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe
