[Agda] Universe polymorphism

[Darin Morrison]

On Sat, Sep 26, 2009 at 3:28 PM, Peter Hancock <hancock at spamcop.net> wrote:

> Personally, I think that universes are hairy enough that they are best
> programmed explicitly, as Set-indexed families of Sets/Functors/Whatever.
> That is, they should be internal universes of Set = Set0.  I haven't
> ever felt the need for Set2, though Set1 is very convenient.
> I don't think Agda should provide automation for weird towers of
> universes over Set0.

If you code everything from scratch, or almost from scratch, then you
can probably get away with the explicit approach.  However, if you
make heavy use of the standard library, the need for some sort of
automation is painfully apparent.  There's already some bits and
pieces of duplicated modules for Set and Set1 creeping into the
library.

Take a look at Data.Product1 to see how out of hand things can get:

http://www.cs.nott.ac.uk/~nad/listings/lib-0.2/Data.Product1.html

The situation gets much, much worse if you need to use something more
complicated like the equational reasoning modules at higher universes
than they are already defined for.  Now instead of a few data
structures, you have huge chunks of code that need to be duplicated.

Maybe there is a way to continue using the explicit approach but make
it less cumbersome for large scale developments by finding some sort
of clever syntactic sugar...

--
Darin