[Agda] Setω and abstraction

[Dan Doel]

On Wednesday 30 September 2009 6:52:40 am Dan Doel wrote:
> I've been thinking about trying to add a system with universe polymorphism
>  to my PTS evaluator so I can play around with various choices, but I don't
>  think it's 'just another set of axioms,' so I don't know how far I'll get.

So, I did manage to do a bit of this, and I now have a small REPL for type 
checking and normalizing a lambda calculus with a pure type system with 
universe polymorphism. An example session can be found here:

  http://hpaste.org/fastcgi/hpaste.fcgi/view?id=10096#a10096

The type system looks something like:

  0       : Level
  l + 1   : Level forall l : Level
  Type[l] : Type[l + 1] forall l : Level
  Level   : Type[0] (This feels weird to me, but maybe it's okay.)
  (l : Level) -> <expression mentioning l>
          : Type[ω]
  Type[ω] has no type, and is ineligible to be quantified over

At the moment, the type checker would tell you that ω : Level, but I suspect 
that's wrong, since it can't be one of the values quantified over in universe 
polymorphism, or else something bigger would have to exist. It's, therefore, 
also probably better to think of Type[ω] as a wholly distinct universe above 
everything else, and not just part of the Level-indexed family. But the 
notation is convenient. The parser doesn't recognize any syntactic element 
denoting ω at the moment, so you can't really do anything with this anomaly. 
The only way you'll see ω at all is asking the type of a universe-polymorphic 
type (or trying to create a lambda expression that returns a universe-
polymorphic type, which will blow up because nothing is above Type[ω]).

The system is pretty simplistic. There's no logic for dealing with ordering of 
universe levels, or talking about the maximum of two levels; it just blows up 
when it encounters two different level variables (it can make sense of l + n 
and l + m for natural n and m, though). I'll probably make that more robust in 
the future, but even so, you can get something of a feel for what kind of 
capabilities this system would have. You can see in my example session that I 
declare a function that accepts several universe polymorphic functions and 
uses one of them (the one that's supposed to be a type constructor) at two 
different levels.

I also have a capability for assuming variables into the environment with 
certain types, to pretend like inductive types exist. They'll cause errors if 
you ask to see normal forms, but they work for pure type checking. Other than 
that it's raw lambda terms, and those might make it difficult to see certain 
things.

If anyone cares to play with it (although playing with Agda is probably more 
interesting :)), the code is at:

  http://code.haskell.org/~dolio/upts/

I probably won't bother implementing the ω + ω hierarchy. That seems a bit too 
wacky.

-- Dan