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.
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 decorateSet
s with one letter for each typeA
throughD
:Yes, sadly universe polymorphism usually requires fair amount of boilerplate code. Anyways, the only way to generalize
≈-List
is to allowSet a
forA
. So, you start with:But here's the problem: what's the type of the
_∷_
constructor? The type ofx
(andy
,xs
,ys
) isA : Set a
, type ofx≈y
isx ≈ y : Rel A ℓ = A → A → Set ℓ
. This implies that type of the constructor should beSet (max a ℓ)
, or in standard library notationSet (a ⊔ ℓ)
.So yes, if we generalize
≈-List
to work withA : Set a
, we have to declare its type asRel (List A) (a ⊔ ℓ)
. You could make itRel (List A) ℓ
by not havingx
,y
,xs
andys
- but I suppose that's not an option. And that's a dead end: either useSet
s (becausezero ⊔ ℓ = ℓ
) or changequibble
.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 typeA : Set a
and something that requires typeSet (a ⊔ b)
. Now, surelya ≤ a ⊔ b
, so by going fromSet a
toSet (a ⊔ b)
cannot cause any contradictions (in the usualSet : Set
sense). And of course, the standard library has a tool for this. In theLevel
module, there's a data type calledLift
, let's look at its definition:Notice that is has only one field of type
A
(which is inSet a
) andLift A
itself has a typeSet (a ⊔ ℓ)
. So, if you havex : A : Set a
, you can move to higher level vialift
:lift a : Lift A : Set (a ⊔ ℓ)
and vice versa: if you have something inLift A
, you can lower it back using... erm..lower
:x : Lift A : Set (a ⊔ ℓ)
andlower 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
onVec
tors with just the dependent eliminator. Here's the dependent eliminator (also known as induction principle) for vectors: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:But here's the problem: we ought to return
Set a
, but⊤ : Set
. So weLift
it:And then we can write: