[Agda] Reflection with terms in different universes

[Jannis Limperg]

Dear all,

I'm trying and failing to write a reflective simplification tactic
involving terms at different universe levels. (Jesper: Here's yet
another argument for cumulativity.) For a simple example, consider
the following definitions of magmas and their morphisms:

\begin{code}
open import Agda.Primitive using (lsuc ; _⊔_)

record Magma l : Set (lsuc l) where
field
Carrier : Set l
eq : Carrier → Carrier → Set l
plus : Carrier → Carrier → Carrier

open Magma

record _⇒_ {l} (M : Magma l) {l′} (N : Magma l′) : Set (l ⊔ l′) where
field
arr : Carrier M → Carrier N
resp : ∀ {x y}
→ eq M x y → eq N (arr x) (arr y)
plus : ∀ {x y}
→ eq N (plus N (arr x) (arr y)) (arr (plus M x y))

open _⇒_
\end{code}

The tactic should simplify magma expressions. Of course, with magmas
there's not much to simplify (the actual problem involves categories and
functors), but one goal I'd like to have proven for me is this:

\begin{code}
postulate
goal : ∀ {l} {M : Magma l} {l′} {N : Magma l′} (f : M ⇒ N) x y
→ eq N (plus N (arr f x) (arr f y)) (arr f (plus M x y))
\end{code}

To get a reflective tactic that solves this sort of goal, I'd usually
define a language of terms and an interpretation function:

\begin{code}
data Tm {l} : Magma l → Set (lsuc l) where
var : ∀ {M} (x : Carrier M) → Tm M
_+_ : ∀ {M} (x y : Tm M) → Tm M
hom : {M N : Magma l} → M ⇒ N → Tm M → Tm N

⟩_⟧ : ∀ {l} {M : Magma l} → Tm M → Carrier M
⟩ var x ⟧ = x
⟩_⟧ {M = M} (x + y) = plus M ⟩ x ⟧ ⟩ y ⟧
⟩ hom f x ⟧ = arr f ⟩ x ⟧
\end{code}

But here's the rub: In a `Tm {l} M`, *all* magmas must be at level `l`.
Consequently, there is no `Tm M` corresponding to the goal above, which
contains two magmas, `M` and `N`, at different levels. So the question
is: How do I write a reflective tactic that can deal with this sort of
problem?

Here are my previous attempts at a solution, which you can probably
skip:

One idea was to replace the magmas with placeholders (say, natural
numbers) during reflection. But then the interpretation function needs
to substitute the actual magmas for the placeholders, so it needs a
mapping from natural numbers to magmas at different levels, which seems
to run into the same problem.

Another idea involves lifting all the magmas up to the maximum of their
levels during reflection. The tactic would then yield an equation that
corresponds to the goal, only with all magmas replaced by lifted ones.
Perhaps I could then reflectively generate a proof that this equation
over lifted magmas implies the goal; this proof should be entirely
syntax-directed. This approach seems promising, but before going on a
wild adventure, I wanted to ask if someone had dealt with this sort of
thing before.

Thanks for your time,
Jannis

[Roman]

Post by Jannis Limperg
One idea was to replace the magmas with placeholders (say, natural

numbers) during reflection.

when I needed to evaluate types of the following form:

data Type n : Set where
Var : Fin n -> Type n
_⇒_ : Type n -> Type n -> Type n

to regular Agda types. The idea is that you generate an implicit
product vector for levels using

_^_ : ∀ {α} -> Set α -> ℕ -> Set α
A ^ 0 = Lift ⊤
A ^ suc n = A × A ^ n

and supply a universe for each of these levels:

Sets : ∀ {n} -> (αs : Level ^ n) -> Set blah-blah
Sets {0} _ = ⊤
Sets {suc _} (α , αs) = Set α × Sets αs

The interpretation function then is

⟦_⟧ᵗˡ : ∀ {n} σ -> Level ^ n -> Level
⟦ Var i ⟧ᵗˡ αs = lookup i αs
⟦ σ ⇒ τ ⟧ᵗˡ αs = ⟦ σ ⟧ᵗˡ αs ⊔ ⟦ τ ⟧ᵗˡ αs

⟦_⟧ᵗ : ∀ {n} {αs : Level ^ n} σ -> Sets αs -> Set (⟦ σ ⟧ᵗˡ αs)
⟦ Var i ⟧ᵗ As = Lookup i As
⟦ σ ⇒ τ ⟧ᵗ As = ⟦ σ ⟧ᵗ As -> ⟦ τ ⟧ᵗ As

Then when you need to construct a term rather than a type, you make
those implicit `{αs : Level ^ n} {As : Sets αs}` and Agda will
perfectly unify them with, say, ∀ {l} {M : Magma l} {l′} {N : Magma
l′} from your example.

For example, for me it was

⟦_⟧ : ∀ {n Γ σ} {αs : Level ^ n} {As : Sets αs} -> Γ ⊢ σ -> ⟦ Γ ⟧ᶜ
As -> ⟦ σ ⟧ᵗ As

The `Sets` machinery can be found at [1].
The example interpretation can be found at [2].

[1] https://github.com/effectfully/STLC/blob/master/src/STLC/Lib/Sets.agda
[2] https://github.com/effectfully/STLC/blob/master/src/STLC/Semantics/Eval.agda

[Roman]

Post by Jannis Limperg
Another idea involves lifting all the magmas up to the maximum of their

levels during reflection.

I have a blog post about doing a similar thing:
http://effectfully.blogspot.com/2016/07/cumu.html

Applied to your case it looks like this:
https://gist.github.com/effectfully/9ebd95e43c3a562e233e779269e3f241

I'd start from the placeholders approach, though.

[Jannis Limperg]

Thank you very much, Roman! I expected the number of workable approaches
to this problem to be closer to zero than two, so your detailed answers
are much appreciated.

Cheers,
Jannis