Appropriate use of universe polymorphism

Question

I've been working for a couple of weeks on an Agda project, glibly ignoring level polymorphism as much as I can. Unfortunately (or perhaps fortunately) I seem to have reached the point where I need to start understanding it.

Until now I've been using level variables only when they are needed as a second argument to Rel (or third argument to REL). Otherwise I have omitted them, just using Set directly. Now I have some client code that explicitly quantifies over levels a and tries to pass some types of the form Set a to my existing code, which is now insufficiently polymorphic. In the example below, quibble represents the client code, and _[_]×[_]_ and ≈-List are typical of my existing code which just uses Set.

module Temp where

open import Data.List
open import Data.Product
open import Level
open import Relation.Binary

-- Direct product of binary relations.
_[_]×[_]_ : {ℓ₁ ℓ₂ : Level} {A B C D : Set} → A × B → REL A C ℓ₁ → REL B D ℓ₂ → C × D → Set (ℓ₁ ⊔ ℓ₂)
(a , b) [ _R_ ]×[ _S_ ] (c , d) = a R c × b S d

-- Extend a setoid (A, ≈) to List A.
data ≈-List {ℓ : Level} {A : Set} (_≈_ : Rel A ℓ) : Rel (List A) ℓ where
   [] : ≈-List _≈_ [] []
   _∷_ : {x y : A} {xs ys : List A} → (x≈y : x ≈ y) → (xs≈ys : ≈-List _≈_ xs ys) → ≈-List _≈_ (x ∷ xs) (y ∷ ys)

quibble : {a ℓ : Level} {A : Set a} → Rel A ℓ → Rel (List (A × A)) ℓ
quibble _≈_ = ≈-List (λ x y → x [ _≈_ ]×[ _≈_ ] y)

Here, I can extend the inductive definition of ≈-List with an extra level parameter a so that it can take a type argument of type Set a, but then I'm unclear as to how the universes of the input and output relations should change. And then problem spills out to more complex definitions such as _[_]×[_]_ where I'm even less sure how to proceed.

How should I generalise the signatures in the example given, so that quibble compiles? Are there general rules I can follow? I've read this.

Answer 1

I don't think you can generalize it to arbitrary universe levels and still have quibble compile. The product of binary relations can be generalized quite easily: you just have to decorate Sets with one letter for each type A through D:

_[_]×[_]_ : ∀ {a b c d ℓ₁ ℓ₂}
  {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
  A × B → REL A C ℓ₁ → REL B D ℓ₂ → C × D → Set (ℓ₁ ⊔ ℓ₂)
(a , b) [ _R_ ]×[ _S_ ] (c , d) = a R c × b S d

Yes, sadly universe polymorphism usually requires fair amount of boilerplate code. Anyways, the only way to generalize ≈-List is to allow Set a for A. So, you start with:

data ≈-List {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) : Rel (List A) a where

But here's the problem: what's the type of the _∷_ constructor? The type of x (and y, xs, ys) is A : Set a, type of x≈y is x ≈ y : Rel A ℓ = A → A → Set ℓ. This implies that type of the constructor should be Set (max a ℓ), or in standard library notation Set (a ⊔ ℓ).

So yes, if we generalize ≈-List to work with A : Set a, we have to declare its type as Rel (List A) (a ⊔ ℓ). You could make it Rel (List A) ℓ by not having x, y, xs and ys - but I suppose that's not an option. And that's a dead end: either use Sets (because zero ⊔ ℓ = ℓ) or change quibble.

---

quibble might not be salvagable, but let me give you one tip that's nice to know when you deal with universe polymorphism. Sometimes you have a type A : Set a and something that requires type Set (a ⊔ b). Now, surely a ≤ a ⊔ b, so by going from Set a to Set (a ⊔ b) cannot cause any contradictions (in the usual Set : Set sense). And of course, the standard library has a tool for this. In the Level module, there's a data type called Lift, let's look at its definition:

record Lift {a ℓ} (A : Set a) : Set (a ⊔ ℓ) where
  constructor lift
  field lower : A

Notice that is has only one field of type A (which is in Set a) and Lift A itself has a type Set (a ⊔ ℓ). So, if you have x : A : Set a, you can move to higher level via lift: lift a : Lift A : Set (a ⊔ ℓ) and vice versa: if you have something in Lift A, you can lower it back using... erm.. lower: x : Lift A : Set (a ⊔ ℓ) and lower x : A : Set a.

---

I did a quick search through pile of my code snippets and it came up with this example: how to implement safe head on Vectors with just the dependent eliminator. Here's the dependent eliminator (also known as induction principle) for vectors:

Vec-ind : ∀ {a p} {A : Set a} (P : ∀ n → Vec A n → Set p)
  (∷-case : ∀ {n} x xs → P n xs → P (suc n) (x ∷ xs))
  ([]-case : P 0 []) →
  ∀ n (v : Vec A n) → P n v
Vec-ind P ∷-case []-case ._ [] = []-case
Vec-ind P ∷-case []-case ._ (x ∷ xs)
  = ∷-case x xs (Vec-ind P ∷-case []-case _ xs)

Since we have to deal with empty vector, we'll use type level function that returns A for non-empty vectors and ⊤ for empty ones:

Head : ∀ {a} → ℕ → Set a → Set a
Head 0       A = ⊤
Head (suc n) A = A

But here's the problem: we ought to return Set a, but ⊤ : Set. So we Lift it:

Head 0       A = Lift ⊤
Head (suc n) A = A

And then we can write:

head : ∀ {n a} {A : Set a} → Vec A (suc n) → A
head {A = A} = Vec-ind (λ n xs → Head n A) (λ x _ _ → x) (lift tt) _