UniversePolymorphism

More flexible handling of universes, for instance some form of universe polymorphism, would be nice. Use cases:

• Sometimes a data type is needed on several levels (both equality on the level of Set and Set1, for instance). Or a function (like composition) may be needed on several levels. These different uses may occur in the same program.
• Sometimes a data type is needed on several levels in the same expression. Example: A deep embedding of a monad, along with the join operation.

    data Monad (a : Set) : Set1 where
      return : a -> Monad a
      _>>=_  : {b : Set} -> Monad b -> (b -> Monad a) -> Monad a

    join : forall {a} -> Monad (Monad a) -> Monad a
    join x = x >>= \y -> y

The type signature of join is not well-typed, since Monad a does not live in Set.

A suggestion for how to solve this problem:

1. Add a typing rule "lift" such that if x : Setn, then x : Set(n + 1).
2. Add a limited form of universe polymorphism, (hopefully) in such a way that every complete program can be translated into ordinary Agda with the lift rule above. Preliminary sketch:
   • Let us (tentatively) introduce a type for universe levels, Level, along with the operation which takes a level to its successor. Then (some) universe polymorphic operations can be written explicitly.
   • However, the resulting system may be too strong, so we restrict it by only allowing a single outermost quantifier for every definition (i.e. higher-rank universe polymorphism is not allowed).
   • Furthermore the user is not allowed to write out this quantifier manually. Instead we infer it. The Monad declaration above is generalised as follows:

         data Monad {i : Level} (a : Set i) : Set (i + 1) where
           return : a -> Monad a
           _>>=_  : {b : Set i} -> Monad b -> (b -> Monad a) -> Monad a 
     

     Basically all uses of Set become Set i, Set1 becomes Set (i + 1), etc.
   • Uses of universe-polymorphic definitions result in certain constraints on the indices. It must be possible to solve these constraints using just the lift typing rule. There may be several possible solutions; we pick the one in which the indices are lowest. (Note: We do not claim that there is a principal solution.) For instance, for the type signature of join we first infer a generalised variant as above:

         forall {i} {a : Set i} -> Monad {?1} (Monad {?2} a) -> Monad {?3} a, 
     

     Here we get some constraints, ?1 ≥ ?2 + 1, ?2 ≥ i and ?3 ≥ i. Furthermore all question marks have to be solved (locally, before proceeding with type checking) with expressions of the form i + k for constant natural numbers k. We get the "lowest" solution ?1 = i + 1, ?2 = i, ?3 = i.
     Another example: For the body of join {i} {a} x we get the generalised right-hand side

         _>>=_ {i = ?1} {a = a} {b = Monad {i = ?2} a}
               x
               (\(y : Monad {i = ?3} a) -> y : Monad {i = ?4} a) 
     

     with the constraints {x ≥ i | i ∈ ?1, ?2, ?3, ?4}, ?1 ≥ ?2 + 1. We get the "lowest" solution ?1 = i + 1, ?2 = ?3 = ?4 = i. (This is a bit simplified since in reality the structure of b would first have to be inferred through unification, etc.)

The system outlined above may perhaps not be strong enough, but at least it solves some problems, is quite simple, and provides a testbed which we can test the limitations of. We should not extend the language without first having well-motivated use cases.

Considering the join operation as more primitive than the bind operation from a category theoretical point of view, I wonder how some intended implementation of

    data Monad {i : Level} (a : Set i) : Set (i + 1) where
      return : a -> Monad a
      _>>=_  : {b : Set i} -> Monad b -> (b -> Monad a) -> Monad a 

might look like. All I can think of at the moment has the signature

    data Monad {i : Level} (a : Set i) : Set (max i c) where
      return : a -> Monad a
      _>>=_  : {b : Set i} -> Monad b -> (b -> Monad a) -> Monad a 

for some constant level c, where max denotes the join in the upper semilattice of universe levels.