# Universe Polymorphism

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`

.

**endo**-functors, i.e.,

`Monad a`

shoud be “the same kind of thing” as `a`

.
A suggestion for how to solve this problem:

- Add a typing rule "lift" such that if
`x : Set`

_{n}, then`x : Set`

_{(n + 1)}. - 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.)

- Let us (tentatively) introduce a type for universe levels,

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.