# 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

join x = x >>= \y -> y
```
The type signature of `join` is not well-typed, since `Monad a` does not live in `Set`.
Comment (Wolfram): However, this example is artificial at least because monads should be endo-functors, i.e., `Monad a` shoud be “the same kind of thing” as `a`.

A suggestion for how to solve this problem:

1. Add a typing rule "lift" such that if `x : Set``n`, 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.