Dependently typed program transformations
This post is jointly written with my assistant Shu-Ting Hsu.
When writing Agda programs, applying different pattern matching strategies to the same function leads to different program structures corresponding to different ways of performing case analyses.
One common situation that arises when working with an indexed data type is that a beginner may analyse the indices first but end up with a more complex program, and then they are usually taught that it can be more straightforward to analyse the data.
For example, consider this definition of _≤_ (which is a renamed version of _≤′_ from the standard library),
data _≤_ : ℕ → ℕ → Set where
base : m ≡ n → m ≤ n
step : m ≤ n → m ≤ suc n
and suppose that we want to weaken suc m ≤ n (that is, m < n) to m ≤ n:
wk : (m n : ℕ) → suc m ≤ n → m ≤ n
wk m .(suc m) (base refl) = step (base refl)
wk m .(suc n) (step {n} m<n) = step (wk m n m<n)
This definition performs a case analysis on the proof of suc m ≤ n.
To emphasise that the pattern matching on the second argument is not performed by the programmer but forced by unification, we use dot patterns explicitly (and therefore need to bind n explicitly in the step constructor in the second clause).
A beginner might be unfamiliar with the idea of induction on proofs though, and write the following version that analyses the indices m and n first:
wk' : (m n : ℕ) → suc m ≤ n → m ≤ n
wk' zero zero m<n = base refl
wk' zero (suc .zero) (base refl) = step (base refl)
wk' zero (suc n) (step m<n) = step (wk' zero n m<n)
wk' (suc m) zero (base ())
wk' (suc m) (suc .(suc m)) (base refl) = step (base refl)
wk' (suc m) (suc n) (step m<n) = step (wk' (suc m) n m<n)
Here wk' is finished with six cases, and is more complex than wk.
In all the cases except the first one, the shapes of m and n determine the constructor of suc m ≤ n, but we still need to match the proof with that constructor explicitly — note the absence of dots before the base and step patterns.
The first case is more interesting because the right-hand side is something we didn’t see in wk.
Alternatively, we could complete the clause by matching m<n : suc zero ≤ zero with base () and make wk' less different from wk, but we will keep the base refl definition to help with our discussion below (and it’s actually natural for a beginner to fill in base refl upon seeing the goal type zero ≤ zero).
So wk' performs two layers of pattern matching on the indices and then the data, whereas wk performs only one layer of pattern matching on the data directly.
What is the connection between wk and wk'?
We suspect that wk' can be transformed into wk step by step, and carry out an experiment.
Transforming wk' to wk, take 1
Our first step is to fully expand the two layers of case analyses in every clause.
For wk', only the first clause still needs to be expanded:
wk₁ : (m n : ℕ) → suc m ≤ n → m ≤ n
wk₁ zero zero (base _) = base refl
wk₁ zero (suc .zero) (base refl) = step (base refl)
wk₁ zero (suc n) (step m<n) = step (wk₁ zero n m<n)
wk₁ (suc m) zero (base ())
wk₁ (suc m) (suc .(suc m)) (base refl) = step (base refl)
wk₁ (suc m) (suc n) (step m<n) = step (wk₁ (suc m) n m<n)
Next, we reorder the clauses so that the clauses with the same patterns for the proof of suc m ≤ n are grouped together, to indicate that the case analysis on the indexed data suc m ≤ n is now performed first (although the case tree generated by Agda won’t reflect that):
wk₂ : (m n : ℕ) → suc m ≤ n → m ≤ n
wk₂ zero zero (base _) = base refl
wk₂ zero (suc .zero) (base refl) = step (base refl)
wk₂ (suc m) zero (base ())
wk₂ (suc m) (suc .(suc m)) (base refl) = step (base refl)
wk₂ zero (suc n) (step m<n) = step (wk₂ zero n m<n)
wk₂ (suc m) (suc n) (step m<n) = step (wk₂ (suc m) n m<n)
In the step clauses, the results on the right-hand sides are actually essentially the same: the difference is only in the first arguments of the recursive calls, but what they both do is copying the first argument, regardless of whether that’s zero or suc m.
The two clauses can therefore be merged into a single one:
wk₃ : (m n : ℕ) → suc m ≤ n → m ≤ n
wk₃ zero zero (base _) = base refl
wk₃ zero (suc .zero) (base refl) = step (base refl)
wk₃ (suc m) zero (base ())
wk₃ (suc m) (suc .(suc m)) (base refl) = step (base refl)
wk₃ m (suc n) (step m<n) = step (wk₃ m n m<n)
The first four base clauses do not admit the same simplification.
The second and fourth clauses look mergeable because they share the same result, but the first and third clauses do not.
The third clause is an impossible branch, but its empty domain makes its result extensionally irrelevant, so the mismatch may not be problematic; on the other hand, if we insist on rewriting it into the same form syntactically, there doesn’t seem to be a way of doing that.
The first clause presents a more problematic mismatch, since base refl and step (base refl) have visibly different constructor forms.
It appears that we’re stuck.
Basic analyses
It turns out that we can make more progress if we first translate pattern-matching programs into the corresponding eliminators, as in Goguen, McBride, and McKinna’s Eliminating dependent pattern matching.
For example, the eliminator for _≤_ is
elim-≤ : (P : (m n : ℕ) → m ≤ n → Set)
→ ({m n : ℕ} {m≡n : m ≡ n} → P m n (base m≡n))
→ ({m n : ℕ} {m≤n : m ≤ n} → P m n m≤n → P m (suc n) (step m≤n))
→ (m n : ℕ) (m≤n : m ≤ n) → P m n m≤n
elim-≤ P pb ps m .m (base refl) = pb
elim-≤ P pb ps m .(suc _) (step m≤n) = ps (elim-≤ P pb ps m _ m≤n)
Actually, instead of translating directly to eliminators, Goguen et al chose to introduce an intermediate language of basic analysis; pattern-matching programs are translated to basic analyses, which can be defined in terms of eliminators. These basic analysis operators can be thought of as a semantics of Epigram. For example, Section 2 of Conor’s Epigram: Practical programming with dependent types gave this standard example:
plus x y ⇐ rec x {
plus x y ⇐ case x {
plus zero y ⇒ y
plus (suc x) y ⇒ suc (plus x y) } }
There are two things to observe here: (i) Conor chose to separate recursion and case analysis; (ii) the target to be recursed over or analysed (x in the example above) may be part of a larger input (x and y above).
By contrast, eliminators mix recursion and case analysis, and assume that the proof and its indices are the only things in the input — for example, elim-≤ ends with (m n : ℕ) (m≤n : m ≤ n) → P m n m≤n instead of a general dependent function type (δ : Δ) → T δ.
The rest of this section explains in more detail what basic analysis operators are and how to define them from eliminators.
Basic case-analysis operators
We’ll look at case analysis first.
The following case-≤ operator is the same as elim-≤ except that the induction hypothesis in the step method is dropped, so the case-≤ operator only performs a case analysis on a proof of m ≤ n.
case-≤ : (P : ∀ m n → m ≤ n → Set)
→ ((m n : ℕ) (m≡n : m ≡ n) → P m n (base m≡n))
→ ((m n : ℕ) (m≤n : m ≤ n) → P m (suc n) (step m≤n))
→ (m n : ℕ) (m≤n : m ≤ n) → P m n m≤n
case-≤ P pb ps = elim-≤ P
(λ {m₀ n₀ m₀≡n₀} → pb m₀ n₀ m₀≡n₀)
(λ {m₀ n₀ m₀≤n₀} _ → ps m₀ n₀ m₀≤n₀)
Like elim-≤, the type of case-≤ ends with (m n : ℕ) (m≤n : m ≤ n) → P m n m≤n, but we want to change that to a general dependent function type (δ : Δ) → T δ:
basic-case-≤ : (Δ : Set) (T : Δ → Set) (t : Δ → Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] (m ≤ n))
→ ((δ : Δ) (m n : ℕ) (m≡n : m ≡ n) → (m , n , base m≡n) ≡ t δ → T δ)
→ ((δ : Δ) (m n : ℕ) (m≤n : m ≤ n) → (m , suc n , step m≤n) ≡ t δ → T δ)
→ (δ : Δ) → T δ
basic-case-≤ Δ T t m₁ m₂ δ =
let (m , n , m≤n) = t δ
in case-≤ (λ m n m≤n → (δ : Δ) → (m , n , m≤n) ≡ t δ → T δ)
(λ m n m≡n δ → m₁ δ m n m≡n)
(λ m n m≤n δ → m₂ δ m n m≤n)
m n m≤n δ refl
This is the basic analysis derived from case-≤, hence the name basic-case-≤.
The first two arguments of basic-case-≤ specify what Δ and T are.
The next argument t extracts the proof and its indices from an input δ : Δ to be analysed.
In the two methods, we add equality constraints stating that the extracted proof and its indices are specialised to base and step between the input δ : Δ and the output T δ.
So when we use basic-case-≤ to write a function (δ : Δ) → T δ that analyses t δ, we split the programming problem into two cases; in each case, we still write a function from δ : Δ to T δ but can assume an additional equality constraint that t δ has a more specialised form.
The derivation of basic-case-≤ from case-≤ is actually a general construction given by Goguen et al (which derives basic analysis operators from ‘elimination operators’), but we won’t go into the details here.
Basic recursion operators
Now, we move on to recursion. For case analysis, the methods add constraints on the immediate constructor shape of the proof being analysed. For recursion, the methods should be able to make recursive calls on structurally smaller proofs (or data). Goguen et al chose to define strong induction principles: the methods are supplied with an additional argument for making recursive calls on all the smaller proofs, not only for the immediate predecessor.
To represent these recursive calls, we first introduce an iterated tuple type Below-≤ P m n m≤n which, for a predicate P on the proofs, states that P holds for all the proofs structurally smaller than the given proof m≤n:
Below-≤ : (P : ∀ m n → m ≤ n → Set) → ∀ m n → m ≤ n → Set
Below-≤ P m .m (base refl) = ⊤
Below-≤ P m .(suc _) (step m≤n) = Below-≤ P m _ m≤n × P m _ m≤n
In the base case, there is no smaller proof, so the tuple is trivial.
In the step case, the proof contains a predecessor proof m≤n, so the tuple contains both the recursive information below that predecessor and the result of P for the predecessor itself.
Then we can define the type of the recursion operator, where we use Below-≤ as the type of the induction hypotheses:
rec-≤ : (P : ∀ m n → m ≤ n → Set)
→ (∀ m n → (m≤n : m ≤ n) → Below-≤ P m n m≤n → P m n m≤n)
→ ∀ m n → (m≤n : m ≤ n) → P m n m≤n
The operational intuition of strong induction is to never forget previous results and accumulate them in a tuple instead, which is used as the strengthened induction hypotheses.
A clean way of implementing rec-≤ is to write a function constructing such tuples first:
below-≤ : (P : ∀ m n → m ≤ n → Set)
→ (p : ∀ m n → (m≤n : m ≤ n) → Below-≤ P m n m≤n → P m n m≤n)
→ ∀ m n → (m≤n : m ≤ n) → Below-≤ P m n m≤n
below-≤ P p m .m (base refl) = tt
below-≤ P p m .(suc _) (step m≤n) = let b = below-≤ P p m _ m≤n
in (b , p m _ m≤n b)
The type of below-≤ is the same as that of rec-≤ except that the result type is the Below tuple type.
In the base case, there are no smaller proofs, so the tuple is just tt.
In the step case, we first build the tuple b below m≤n recursively (which are the strengthened hypotheses), and then extend the tuple with the result for m≤n itself, obtained by applying the method p to b (the strengthened induction hypotheses).
Then all it takes to get from below-≤ to rec-≤ is a final application of p:
rec-≤ : (P : ∀ m n → m ≤ n → Set)
→ (∀ m n → (m≤n : m ≤ n) → Below-≤ P m n m≤n → P m n m≤n)
→ ∀ m n → (m≤n : m ≤ n) → P m n m≤n
rec-≤ P p m n m≤n = p m n m≤n (below-≤ P p m n m≤n)
Same as case-≤, we want rec-≤ to end with a general dependent function type (δ : Δ) → T δ, so we apply Goguen et al’s general construction to rec-≤ and get
basic-rec-≤ : (Δ : Set) (T : Δ → Set) (t : (δ : Δ) → Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] (m ≤ n))
→ ((δ : Δ) (m n : ℕ) (m≤n : m ≤ n) → (b : Below-≤ (λ m' n' m≤n' → (δ : Δ) → (m' , n' , m≤n') ≡ t δ → T δ) m n m≤n) → (m , n , m≤n) ≡ t δ → T δ)
→ (δ : Δ) → T δ
basic-rec-≤ Δ T t p δ =
let (m , n , m≤n) = t δ
in rec-≤ (λ m' n' m≤n' → (δ : Δ) → (m' , n' , m≤n') ≡ t δ → T δ)
(λ m n m≤n b δ → p δ m n m≤n b)
m n m≤n δ refl
When we use basic-rec-≤ to write a function (δ : Δ) → T δ that recurses on t δ, first we specify Δ, T, and t, and then we write a function with the same input and output but extended with additional arguments.
The first three additional arguments m, n, and m≤n can be thought of as the results of pattern-matching t δ with a tuple because there is an equality constraint (m , n , m≤n) ≡ t δ near the end.
Then we get a Below-≤ argument that allows us to make recursive calls as long as the m≤n proof gets structurally smaller.
Such a recursive call can change the input δ as needed (to something larger or even unrelated), but the m≤n part of δ should get smaller for the recursive call to be legitimate.
So the Below-≤ argument contains functions of type (δ : Δ) → (m' , n' , m≤n') ≡ t δ → T δ for all (m' , n' , m≤n') that are smaller than (m , n , m≤n).
Deriving basic analysis operators from other eliminators
In the next section we will see concrete examples of translating pattern-matching programs to basic analysis, namely wk and wk₁ (which is close to wk').
Before moving forward to the translation, we need to apply the above techniques to another datatype ℕPair = ℕ × ℕ, since wk₁’s first pattern-matching target is its pair of natural-number arguments.
The eliminator we start with matches both natural numbers with zero or suc, and allows recursion whenever one or both numbers get structurally smaller:
elim-ℕPair : (P : ℕ × ℕ → Set)
→ P (zero , zero)
→ ({n : ℕ} → P (zero , n) → P (zero , suc n))
→ ({m : ℕ} → P (m , zero) → P (suc m , zero))
→ ({m n : ℕ} → P (m , n) → P (suc m , n) → P (m , suc n) → P (suc m , suc n))
→ ((m , n) : ℕ × ℕ) → P (m , n)
elim-ℕPair p pz psₙ psₘ ps (zero , zero) = pz
elim-ℕPair p pz psₙ psₘ ps (zero , suc n) = psₙ (elim-ℕPair p pz psₙ psₘ ps (zero , n))
elim-ℕPair p pz psₙ psₘ ps (suc m , zero ) = psₘ (elim-ℕPair p pz psₙ psₘ ps (m , zero))
elim-ℕPair p pz psₙ psₘ ps (suc m , suc n) = ps (elim-ℕPair p pz psₙ psₘ ps (m , n)) (elim-ℕPair p pz psₙ psₘ ps (suc m , n)) (elim-ℕPair p pz psₙ psₘ ps (m , suc n))
In the last case, it allows recursive access to the three smaller pairs: (m , n), (suc m , n), and (m , suc n).
Next, we split elim-ℕPair into two operators, case-ℕPair for case analysis,
case-ℕPair : (P : ℕ × ℕ → Set)
→ P (zero , zero)
→ ((n : ℕ) → P (zero , suc n))
→ ((m : ℕ) → P (suc m , zero))
→ ((m n : ℕ) → P (suc m , suc n))
→ (m n : ℕ) → P (m , n)
case-ℕPair P pz pn pm ps zero zero = pz
case-ℕPair P pz pn pm ps zero (suc n) = pn n
case-ℕPair P pz pn pm ps (suc m) zero = pm m
case-ℕPair P pz pn pm ps (suc m) (suc n) = ps m n
and rec-ℕPair for recursive call, following the same recipe as above:
Below-ℕPair : (P : ℕ × ℕ → Set) → ℕ → ℕ → Set
Below-ℕPair P zero zero = ⊤
Below-ℕPair P zero (suc n) = Below-ℕPair P zero n × P (zero , n)
Below-ℕPair P (suc m) zero = Below-ℕPair P m zero × P (m , zero)
Below-ℕPair P (suc m) (suc n) = (Below-ℕPair P m n × P (m , n))
× (Below-ℕPair P (suc m) n × P (suc m , n))
× (Below-ℕPair P m (suc n) × P (m , suc n))
below-ℕPair : (P : ℕ × ℕ → Set)
→ (p : (m n : ℕ) → Below-ℕPair P m n → P (m , n))
→ (m n : ℕ) → Below-ℕPair P m n
below-ℕPair P p zero zero = tt
below-ℕPair P p zero (suc n) = let b = below-ℕPair P p zero n
in (b , p zero n b)
below-ℕPair P p (suc m) zero = let b = below-ℕPair P p m zero
in (b , p m zero b)
below-ℕPair P p (suc m) (suc n) = let b = below-ℕPair P p m n
bₙ = below-ℕPair P p (suc m) n
bₘ = below-ℕPair P p m (suc n)
in ((b , p m n b) ,
(bₙ , p (suc m) n bₙ) ,
(bₘ , p m (suc n) bₘ))
rec-ℕPair : (P : ℕ × ℕ → Set)
→ ((m n : ℕ) → Below-ℕPair P m n → P (m , n))
→ (m n : ℕ) → P (m , n)
rec-ℕPair P p m n = p m n (below-ℕPair P p m n)
(Shin noted in a group meeting that the top-down problem-splitting strategy of elim-ℕPair leads to overlapping sub-problems, and there is an opportunity to derive a bottom-up rec-ℕPair to avoid solving the same sub-problems repeatedly, in the same spirit as our binomial tabulation papers.)
Finally, we apply the basic analysis construction on case-ℕPair and rec-ℕPair, respectively:
basic-case-ℕPair : (Δ : Set) (T : Δ → Set) (t : Δ → ℕ × ℕ)
→ ((δ : Δ) → (zero , zero) ≡ t δ → T δ)
→ ((δ : Δ) (n : ℕ) → (zero , suc n) ≡ t δ → T δ)
→ ((δ : Δ) (m : ℕ) → (suc m , zero) ≡ t δ → T δ)
→ ((δ : Δ) (m n : ℕ) → (suc m , suc n) ≡ t δ → T δ)
→ (δ : Δ) → T δ
basic-case-ℕPair Δ T t p₁ p₂ p₃ p₄ δ = let (m , n) = t δ in case-ℕPair (λ (m , n) → (δ : Δ) → (m , n) ≡ t δ → T δ) p₁ (λ n δ → p₂ δ n) (λ m δ → p₃ δ m) (λ m n δ → p₄ δ m n) m n δ refl
basic-rec-ℕPair : (Δ : Set) (T : Δ → Set) (t : (δ : Δ) → ℕ × ℕ)
→ ((δ : Δ) (m n : ℕ) → (b : Below-ℕPair (λ (m , n) → (δ : Δ) → (m , n) ≡ t δ → T δ) m n) → (m , n) ≡ t δ → T δ)
→ (δ : Δ) → T δ
basic-rec-ℕPair Δ T t p δ = let (m , n) = t δ in rec-ℕPair (λ (m , n) → (δ : Δ) → (m , n) ≡ t δ → T δ) (λ m n b δ → p δ m n b) m n δ refl
Remark.
There are more than one ways of performing pattern matching on pairs of natural numbers.
For example, the following alternative eliminator also matches both numbers with zero or suc, but allows recursion only when both numbers are structurally smaller:
elim-ℕPair' : (P : ℕ × ℕ → Set)
→ P (zero , zero)
→ ((n : ℕ) → P (zero , suc n))
→ ((m : ℕ) → P (suc m , zero))
→ ((m n : ℕ) → P (m , n) → P (suc m , suc n))
→ ((m , n) : ℕ × ℕ) → P (m , n)
elim-ℕPair' p pz psₙ psₘ ps (zero , zero ) = pz
elim-ℕPair' p pz psₙ psₘ ps (zero , suc n) = psₙ n
elim-ℕPair' p pz psₙ psₘ ps (suc m , zero ) = psₘ m
elim-ℕPair' p pz psₙ psₘ ps (suc m , suc n) = ps m n (elim-ℕPair' p pz psₙ psₘ ps (m , n))
This corresponds more closely to the recursion performed on (m , n) : ℕPair such that m ≤' n where
data _≤'_ : ℕ → ℕ → Set where
base : zero ≤' n
step : m ≤' n → suc m ≤' suc n
The same can be said for natural numbers — for example, here is a possible alternative eliminator (that have two base cases for 0 and 1):
elim-ℕ' : (P : ℕ → Set)
→ P zero
→ P (suc zero)
→ ((n : ℕ) → P n → P (suc (suc n)))
→ (n : ℕ) → P n
elim-ℕ' P p₀ p₁ ps zero = p₀
elim-ℕ' P p₀ p₁ ps (suc zero) = p₁
elim-ℕ' P p₀ p₁ ps (suc (suc n)) = ps n (elim-ℕ' P p₀ p₁ ps n)
This emphasises the importance of having a general mechanism of deriving basic analysis operators from eliminators: one may want to derive a fixed set of basic analysis operators from a datatype definition, but the above examples of alternative eliminators show that the programmer can choose among different eliminators —and even craft their own— to derive the basic analyses they need. (End of remark.)
Summary
Basic analysis is a higher-level language than eliminators. It separates case analysis from recursion, so constructor inspection and recursive calls are handled by distinct basic analysis operators. These operators are also generalised for arbitrary input contexts and output types, and introduce assumptions about some targeted data (extracted from the inputs) into the contexts. A basic case-analysis operator introduces, for each constructor branch, an equality constraint stating that the targeted data should start with that constructor (as well as arguments of that constructor). A basic recursion operator introduces recursive calls that can be made on inputs where the targeted data become structurally smaller.
Translation to basic analyses
We now illustrate the translation to basic analyses using wk:
wk : (m n : ℕ) → suc m ≤ n → m ≤ n
wk m .(suc m) (base refl) = step (base refl)
wk m .(suc n) (step {n} m<n) = step (wk m n m<n)
The function takes three inputs: m : ℕ, n : ℕ, and m<n : suc m ≤ n.
In the Agda definition, case analysis is more discernible, but the first step of the translation is to invoke a basic recursion operator.
In this case, the target on which the function recurses is m<n, so we use basic-rec-≤:
wk : (m n : ℕ) → suc m ≤ n → m ≤ n
wk m n m<n = basic-rec-≤ (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] suc m ≤ n) (λ (m , n , _ ) → m ≤ n) (λ (m , n , m<n) → (suc m , n , m<n))
(λ { (m , n , m<n) .(suc m) .n .m<n b refl → {! !} })
(m , n , m<n)
In the translation, we package the three inputs into a triple (m , n , m<n) : Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] suc m ≤ n (whose type is given as the first argument to basic-rec-≤) and pass the triple into the operator as the last argument.
The output type of the function is specified by the second argument λ (m , n , _ ) → m ≤ n.
The third argument specifies the target on which to perform recursion, which belongs to the indexed datatype _≤_, so the extraction function returns the _≤_ data along with its surrounding indices: (suc m , n , m<n).
What remains is the method; its inputs, after some simplification, are the original three plus a Below-value b, which makes recursive calls available.
All the inputs —including b— are then passed to the next basic analysis operator, which should be basic-case-≤ applied to m<n and its type indices.
This splits the function we’re defining into the two constructor cases of _≤_ (base and step):
wk : (m n : ℕ) → suc m ≤ n → m ≤ n
wk m n m<n =
let P : (m n : ℕ) → m ≤ n → Set
P = λ Dm Dn Dm<n → ((m , n , m<n) : Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] suc m ≤ n) → (Dm , Dn , Dm<n) ≡ (suc m , n , m<n) → m ≤ n
in basic-rec-≤ (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] suc m ≤ n) (λ (m , n , _) → m ≤ n) (λ (m , n , m<n) → (suc m , n , m<n))
(λ { (m , n , m<n) .(suc m) .n .m<n b refl →
basic-case-≤ (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] Σ[ m<n ∈ suc m ≤ n ] Below-≤ P (suc m) n m<n) (λ (m , n , _) → m ≤ n) (λ (m , n , m<n , _) → (suc m , n , m<n))
(λ { (m , n , m<n , b) m₀ n₀ m₀≡n₀ r₀ → {! m ≤ n ⊣ r₀ : (m₀ , n₀ , base m₀≡n₀) ≡ (suc m , n , m<n); … !} })
(λ { (m , n , m<n , b) m₀ n₀ m₀≤n₀ r₀ → {! m ≤ n ⊣ r₀ : (m₀ , suc n₀ , step m₀≤n₀) ≡ (suc m , n , m<n); … !} })
(m , n , m<n , b) })
(m , n , m<n)
We can see the variable r₀ in both methods; however, as shown in the two holes above, r₀ represents different equality constraints in the two methods, restricting m<n to base or step cases; the arguments of the constructors mentioned by the constraints are also introduced as fresh variables, all given names with suffix ₀.
In order to specialise the inputs and correspondingly the output type, we match r₀ with refl.
This invokes unification and allows us to specialise the inputs m, n, and m<n according to the equality constraints:
wk : (m n : ℕ) → suc m ≤ n → m ≤ n
wk m n m<n =
let P : (m n : ℕ) → m ≤ n → Set
P = λ Dm Dn Dm<n → ((m , n , m<n) : Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] suc m ≤ n) → (Dm , Dn , Dm<n) ≡ (suc m , n , m<n) → m ≤ n
in basic-rec-≤ (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] suc m ≤ n) (λ (m , n , _) → m ≤ n) (λ (m , n , m<n) → (suc m , n , m<n))
(λ { (m , n , m<n) .(suc m) .n .m<n b refl →
basic-case-≤ (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] Σ[ m<n ∈ suc m ≤ n ] Below-≤ P (suc m) n m<n) (λ (m , n , _) → m ≤ n) (λ (m , n , m<n , _) → (suc m , n , m<n))
(λ {(m , n , base m≡n , b) .(suc m) .n .m≡n refl → {! !} })
(λ {(m , suc n , step m≤n , b) .(suc m) .n .m≤n refl → {! !} })
(m , n , m<n , b) })
(m , n , m<n)
In the first method, (m , n , m<n) is specialised to (m , n , base m≡n), and in the second method, it is specialised to (m , suc n , step m≤n) — this is the same specialisation that occurs when we perform case-splitting on m<n in the pattern-matching version of wk!
In general:
Given a pattern-matching program, Agda performs unification internally to determine which constructor branches are possible and how the variables in those branches should be specialised.
In a basic-analysis program, the corresponding constraints are represented explicitly by equality arguments such as r₀, and matching them with refl invokes the same unification process — so these equality arguments represent the unification constraints solved by Agda.
We illustrate this using two versions of the function that returns the first element of a non-empty vector.
Consider the pattern-matching definition head,
head : ∀ n → Vec A (suc n) → A
head n (x ∷ xs) = x
and the corresponding basic-analysis definition head':
head' : ∀ n → Vec A (suc n) → A
head' {A} n xs =
let P : ∀ n → Vec A n → Set
P = λ Dn Dxs → ((n , xs) : Σ[ n ∈ ℕ ] Vec A (suc n)) → (Dn , Dxs) ≡ (suc n , xs) → A
in basic-rec-Vec (Σ[ n ∈ ℕ ] Vec A (suc n)) (λ _ → A) (λ (n , xs) → (suc n , xs))
(λ { (n , xs) .(suc n) .xs b refl →
basic-case-Vec (Σ[ n ∈ ℕ ] Σ[ xs ∈ Vec A (suc n) ] Below-Vec P (suc n) xs) (λ (n , _) → A) (λ (n , xs , _) → (suc n , xs))
(λ { (n , xs , b) () })
(λ { (n , (x ∷ xs) , b) .n .x .xs refl → x })
(n , xs , b) })
(n , xs)
Comparing head and head', the [] case appears in head' and is closed by matching the unification constraint introduced by basic-rec-Vec with the absurd pattern (), whereas it does not appear in head since [] does not match the required type Vec A (suc n).
This illustrates what happens implicitly during pattern matching in Agda: unification determines which branches are possible, and branches where unification succeeds negatively are omitted.
On the other hand, in basic-analysis definitions, the unification constraints are explicit, so unification must be triggered manually by matching them with refl, specialising the inputs and constructor arguments.
Back to the translation of wk, after the unification, we complete the two branches.
In the base case, using the same strategy as in the pattern-matching version, we match m≡n so that the goal can be fulfilled directly with step (base refl):
wk : (m n : ℕ) → suc m ≤ n → m ≤ n
wk m n m<n =
let P : (m n : ℕ) → m ≤ n → Set
P = λ Dm Dn Dm<n → ((m , n , m<n) : Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] suc m ≤ n) → (Dm , Dn , Dm<n) ≡ (suc m , n , m<n) → m ≤ n
in basic-rec-≤ (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] suc m ≤ n) (λ (m , n , _) → m ≤ n) (λ (m , n , m<n) → (suc m , n , m<n))
(λ { (m , n , m<n) .(suc m) .n .m<n b refl →
basic-case-≤ (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] Σ[ m<n ∈ suc m ≤ n ] Below-≤ P (suc m) n m<n) (λ (m , n , _) → m ≤ n) (λ (m , n , m<n , _) → (suc m , n , m<n))
(λ { (m , n , base refl , b) .(suc m) .n .refl refl → step (base refl) })
(λ { (m , suc n , step m≤n , b) .(suc m) .n .m≤n refl → {! !} })
(m , n , m<n , b) })
(m , n , m<n)
In the step case, unification changes the goal to m ≤ suc n.
At the same time, because the analysed proof is a step constructor, the corresponding Below value is also expanded according to the step case in the definition of Below-≤.
Thus, b has the form (_ , b'): the first component contains the recursive calls for smaller proofs, while b' is the recursive call that we can make on the immediate predecessor proof m≤n.
To actually make the recursive call, we write b' (m , n , m≤n) refl, where the final argument is an equality proof confirming that the supplied input m≤n is the one allowed by b', which is again m≤n, so refl suffices.
The recursive call produces a proof of m ≤ n; applying step then yields the required proof of m ≤ suc n:
wk : (m n : ℕ) → suc m ≤ n → m ≤ n
wk m n m<n =
let P : (m n : ℕ) → m ≤ n → Set
P = λ Dm Dn Dm<n → ((m , n , m<n) : Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] suc m ≤ n) → (Dm , Dn , Dm<n) ≡ (suc m , n , m<n) → m ≤ n
in basic-rec-≤ (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] suc m ≤ n) (λ (m , n , _) → m ≤ n) (λ (m , n , m<n) → (suc m , n , m<n))
(λ { (m , n , m<n) .(suc m) .n .m<n b refl →
basic-case-≤ (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] Σ[ m<n ∈ suc m ≤ n ] Below-≤ P (suc m) n m<n) (λ (m , n , _) → m ≤ n) (λ (m , n , m<n , _) → (suc m , n , m<n))
(λ { (m , n , base refl , b) .(suc m) .n .refl refl → step (base refl) })
(λ { (m , suc n , step m≤n , b) .(suc m) .n .m≤n refl → let (_ , b') = b in step (b' (m , n , m≤n) refl) })
(m , n , m<n , b) })
(m , n , m<n)
This completes the basic-analysis definition of wk.
Summary
The translation to basic analysis for a recursive function follows a general rule: basic recursion operators are applied as the outermost layers, so that the required Below arguments are introduced before any case analysis takes place.
These Below arguments are then passed to the subsequent basic case-analysis operators, which split the targeted data into constructor cases, allowing us to break these arguments into tuples of recursive calls that we can actually make.
Within each branch generated by a basic case-analysis, the unification constraints are made explicit and can be matched with refl to specialise the inputs and local constructor arguments.
Laws on basic analyses
Below we will return to the unfinished transformation from wk' to wk, this time translating them to basic analyses first.
Before that, let us formulate some laws on basic analyses used in the transformation.
(From wk₂ to wk₃) we tried to remove the redundant case analyses, which succeeded for the step branches but failed for the base branches.
This removal may be formulated as an equational law (informally in Epigram syntax):
lhs ⇒ rhs
= lhs ⇐ case x {
x₀ ⇒ rhs[x₀/x]
x₁ ⇒ rhs[x₁/x] }
Initially lhs contains an input x, and the result is rhs (which may refer to x).
Equivalently, we can perform a redundant case analysis on x, specialising x to, for example, x₀ or x₁; in both branches we still want to give rhs as the result, which, however, needs to be specialised correspondingly to rhs[x₀/x] and rhs[x₁/x].
Interestingly, when the law is reformulated in terms of basic case-analyses, it becomes conceptually cleaner and easy to justify (although the form gets more ugly, and we’ll skip writing it formally): since basic case-analyses merely introduce equality constraints in the methods while leaving the original input and output unchanged, we can simply copy rhs into the methods of a redundant basic case-analysis while ignoring the constraints.
Another law we need (for going from wk₁ to wk₂) is the case-swapping law:
case x {
x₀ ⇒ case y { y₀ ⇒ rhs₀
y₁ ⇒ rhs₁ }
x₁ ⇒ case y { y₀ ⇒ rhs₂
y₁ ⇒ rhs₃ } }
= case y {
y₀ ⇒ case x { x₀ ⇒ rhs₀
x₁ ⇒ rhs₂ }
y₁ ⇒ case x { x₀ ⇒ rhs₁
x₁ ⇒ rhs₃ } }
This law allows us to swap two nested layers of case analyses, and correspondingly the middle two branches rhs₁ and rhs₂ (while rhs₀ and rhs₃ stay where they are).
Again it is conceptually easier (but syntactically messier) to justify this law in terms of basic case-analyses: each layer of basic case-analysis introduces an equality constraint; it doesn’t matter in which order we introduce the constraints, so it’s okay to swap the layers.
Incidentally, the separation of case analysis and recursion helps us to formulate these laws — for eliminators it’s harder to imagine what the laws would look like.
Transforming wk' to wk, take 2: translating to basic analyses
Now we’re ready to try to transform the basic-analysis version of wk' to that of wk.
If we want to be thorough, we should start from wk' and translate it to basic analyses, but for brevity let’s skip to wk₁ (copied here for easy reference):
wk₁ : (m n : ℕ) → suc m ≤ n → m ≤ n
wk₁ zero zero (base _) = base refl
wk₁ zero (suc .zero) (base refl) = step (base refl)
wk₁ zero (suc n) (step m<n) = step (wk₁ zero n m<n)
wk₁ (suc m) zero (base ())
wk₁ (suc m) (suc .(suc m)) (base refl) = step (base refl)
wk₁ (suc m) (suc n) (step m<n) = step (wk₁ (suc m) n m<n)
wk₁ only slightly expands wk' to two full layers of pattern matching, analysing both the pair of natural numbers m and n and the proof of suc m ≤ n.
Translation of wk₁ applies basic-rec-ℕPair and basic-case-ℕPair (the first layer), and then inserts basic-case-≤ (the second layer) into each of the four branches:
wk₁ : (m n : ℕ) → suc m ≤ n → m ≤ n
wk₁ m n m<n =
let P = λ (Dm , Dn) → ((m , n , m<n) : Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] suc m ≤ n) → (Dm , Dn) ≡ (suc m , n) → m ≤ n
in basic-rec-ℕPair (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] suc m ≤ n) (λ (m , n , _) → m ≤ n) (λ (m , n , _) → (suc m , n))
(λ { (m , n , m<n) .(suc m) .n b refl →
basic-case-ℕPair (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] Σ[ m<n ∈ suc m ≤ n ] Below-ℕPair P (suc m) n) (λ (m , n , _) → m ≤ n) (λ (m , n , _) → (m , n))
(λ { (.zero , .zero , m<n , b) refl →
basic-case-≤ (suc zero ≤ zero × Below-ℕPair P (suc zero) zero) (λ _ → zero ≤ zero) (λ (m<n , _) → (suc zero , zero , m<n))
(λ { (.(base _) , b) m₀ n₀ _ refl → base refl })
(λ { (m<n , b) m₀ n₀ m₀≤n₀ () })
(m<n , b) })
(λ { (.zero , .(suc nₚ) , m<n , b) nₚ refl →
basic-case-≤ (Σ[ nₚ ∈ ℕ ] suc zero ≤ suc nₚ × Below-ℕPair P (suc zero) (suc nₚ)) (λ (nₚ , _) → zero ≤ suc nₚ) (λ (nₚ , m<n , _) → (suc zero , suc nₚ , m<n))
(λ { (.zero , .(base refl) , b) m₀ n₀ refl refl → step (base refl) })
(λ { (nₚ , .(step m₀≤n₀) , b) m₀ n₀ m₀≤n₀ refl → let ((_ , b') , _) = b in step (b' (zero , nₚ , m₀≤n₀) refl) })
(nₚ , m<n , b) })
(λ { (.(suc mₚ) , .zero , m<n , b) mₚ refl →
basic-case-≤ (Σ[ mₚ ∈ ℕ ] suc (suc mₚ) ≤ zero × Below-ℕPair P (suc (suc mₚ)) zero) (λ (mₚ , _) → suc mₚ ≤ zero) (λ (mₚ , m<n , _) → (suc (suc mₚ) , zero , m<n))
(λ { (mₚ , base () , b) m₀ n₀ m₀≡n₀ refl })
(λ { (mₚ , m<n , b) m₀ n₀ m₀≤n₀ () })
(mₚ , m<n , b) })
(λ { (.(suc mₚ) , .(suc nₚ) , m<n , b) mₚ nₚ refl →
basic-case-≤ (Σ[ mₚ ∈ ℕ ] Σ[ nₚ ∈ ℕ ] suc (suc mₚ) ≤ suc nₚ × Below-ℕPair P (suc (suc mₚ)) (suc nₚ)) (λ (mₚ , nₚ , _) → suc mₚ ≤ suc nₚ) (λ (mₚ , nₚ , m<n , _) → (suc (suc mₚ) , suc nₚ , m<n))
(λ { (mₚ , .(suc mₚ) , .(base refl) , b) m₀ n₀ refl refl → step (base refl) })
(λ { (mₚ , nₚ , .(step m₀≤n₀) , b) m₀ n₀ m₀≤n₀ refl → let ((_ , b') , _) = b in step (b' (suc mₚ , nₚ , m₀≤n₀) refl) })
(mₚ , nₚ , m<n , b) })
(m , n , m<n , b)})
(m , n , m<n)
Different from the Agda version, this definition ends up with eight branches instead of six: We are allowed to omit the second and the sixth branches in the Agda version because index unification succeeds negatively, whereas in the basic-analysis version we need to prove negative success explicitly (by matching the manifested unification constraint with the absurd pattern).
Next, to evolve into wk₂, we need to switch the order of applying basic-case-ℕPair and basic-case-≤ (ignoring the outermost basic-rec-ℕPair for now), so we try to use the case-swapping law.
However, looking closer at the inner layer basic-case-≤, we see that the law cannot be applied because the four invocations of basic-case-≤ are not in the same form: the methods look rather different, and even the result types T δ and the extracted data t δ are different — that is, the four basic-case-≤ do case analysis on different ≤-proofs.
The reason is that, before invoking basic-case-≤, the unification constraints generated by basic-case-ℕPair have already been solved, specialising the input to different shapes:
wk₁ : (m n : ℕ) → suc m ≤ n → m ≤ n
wk₁ m n m<n =
...
basic-case-ℕPair ...
(λ { (.zero , .zero , m<n , b) refl → basic-case-≤ ... (λ _ → zero ≤ zero) (λ (m<n , _) → (suc zero , zero , m<n)) ... })
(λ { (.zero , .(suc nₚ) , m<n , b) nₚ refl → basic-case-≤ ... (λ (nₚ , _) → zero ≤ suc nₚ) (λ (nₚ , m<n , _) → (suc zero , suc nₚ , m<n)) ... })
(λ { (.(suc mₚ) , .zero , m<n , b) mₚ refl → basic-case-≤ ... (λ (mₚ , _) → suc mₚ ≤ zero) (λ (mₚ , m<n , _) → (suc (suc mₚ) , zero , m<n)) ... })
(λ { (.(suc mₚ) , .(suc nₚ) , m<n , b) mₚ nₚ refl → basic-case-≤ ... (λ (mₚ , nₚ , _) → suc mₚ ≤ suc nₚ) (λ (mₚ , nₚ , m<n , _) → (suc (suc mₚ) , suc nₚ , m<n)) ... })
...
Think back to how we justified the case-swapping law: the law holds when we gather constraints generated at both the outer and inner layers, and then the constraints can be dealt with in any order, whereas here the translation chooses to solve the outer constraints eagerly and kills the possibility of swapping.
So we should delay solving the outer constraints; instead, we keep them as input to the inner basic-case-≤:
wk₁．₄ : (m n : ℕ) → suc m ≤ n → m ≤ n
wk₁．₄ m n m<n =
let P = λ (Dm , Dn) → ((m , n , m<n) : Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] suc m ≤ n) → (Dm , Dn) ≡ (suc m , n) → m ≤ n
in basic-rec-ℕPair (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] suc m ≤ n) (λ (m , n , _) → m ≤ n) (λ (m , n , _) → (suc m , n))
(λ { (m , n , m<n) .(suc m) .n b refl →
basic-case-ℕPair (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] suc m ≤ n × Below-ℕPair P (suc m) n) (λ (m , n , _) → m ≤ n) (λ (m , n , _) → (m , n))
(λ { (m , n , m<n , b) r →
basic-case-≤ (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] suc m ≤ n × Below-ℕPair P (suc m) n × (zero , zero) ≡ (m , n)) (λ (m , n , _) → m ≤ n) (λ (m , n , m<n , _) → (suc m , n , m<n))
(λ { (m , n , m<n , b , refl) m₀ n₀ m₀≡n₀ refl → base refl })
(λ { (m , n , m<n , b , refl) m₀ n₀ m₀≤n₀ () })
(m , n , m<n , b , r) })
(λ { (m , n , m<n , b) nₚ r →
basic-case-≤ (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] suc m ≤ n × Below-ℕPair P (suc m) n × Σ[ nₚ ∈ ℕ ] (zero , suc nₚ) ≡ (m , n)) (λ (m , n , _) → m ≤ n) (λ (m , n , m<n , _) → (suc m , n , m<n))
(λ { (m , n , m<n , b , nₚ , refl) m₀ n₀ refl refl → step (base refl) })
(λ { (m , n , m<n , b , nₚ , refl) m₀ n₀ m₀≤n₀ refl → let ((_ , b') , _) = b in step (b' (zero , nₚ , m₀≤n₀) refl) })
(m , n , m<n , b , nₚ , r) })
(λ { (m , n , m<n , b) mₚ r →
basic-case-≤ (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] suc m ≤ n × Below-ℕPair P (suc m) n × Σ[ mₚ ∈ ℕ ] (suc mₚ , zero) ≡ (m , n)) (λ (m , n , _) → m ≤ n) (λ (m , n , m<n , _) → (suc m , n , m<n))
(λ { (m , n , m<n , b , mₚ , refl) m₀ n₀ () refl })
(λ { (m , n , m<n , b , mₚ , refl) m₀ n₀ m₀≤n₀ () })
(m , n , m<n , b , mₚ , r)})
(λ { (m , n , m<n , b) mₚ nₚ r →
basic-case-≤ (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] suc m ≤ n × Below-ℕPair P (suc m) n × Σ[ mₚ ∈ ℕ ] Σ[ nₚ ∈ ℕ ] (suc mₚ , suc nₚ) ≡ (m , n)) (λ (m , n , _) → m ≤ n) (λ (m , n , m<n , _) → (suc m , n , m<n))
(λ { (m , n , m<n , b , mₚ , nₚ , refl) m₀ n₀ refl refl → step (base refl) })
(λ { (m , n , m<n , b , mₚ , nₚ , refl) m₀ n₀ m₀≤n₀ refl → let ((_ , b') , _) = b in step (b' (suc mₚ , nₚ , m₀≤n₀) refl) })
(m , n , m<n , b , mₚ , nₚ , r) })
(m , n , m<n , b) })
(m , n , m<n)
In each branch of wk₁．₄, the unification constraint introduced by basic-case-ℕPair, together with all the related arguments (which are originally unified away before basic-case-≤ is applied), is left unsolved and passed into the inner case-analysis layer.
As a result, all of the four basic-case-≤ applications now have a uniform form: they perform case analysis on the same ≤-proof suc m ≤ n with the general result type m ≤ n:
wk₁．₄ : (m n : ℕ) → suc m ≤ n → m ≤ n
wk₁．₄ m n m<n =
...
basic-case-ℕPair ...
(λ { (m , n , m<n , b) r →
basic-case-≤ ... (λ (m , n , _) → m ≤ n) (λ (m , n , m<n , _) → (suc m , n , m<n)) ...})
(λ { (m , n , m<n , b) nₚ r →
basic-case-≤ ... (λ (m , n , _) → m ≤ n) (λ (m , n , m<n , _) → (suc m , n , m<n)) ...})
(λ { (m , n , m<n , b) mₚ r →
basic-case-≤ ... (λ (m , n , _) → m ≤ n) (λ (m , n , m<n , _) → (suc m , n , m<n)) ...})
(λ { (m , n , m<n , b) mₚ nₚ r →
basic-case-≤ ... (λ (m , n , _) → m ≤ n) (λ (m , n , m<n , _) → (suc m , n , m<n)) ...})
...
Now that we have reached the form required for applying the case-swapping law, we can swap the order of basic-case-ℕPair and basic-case-≤:
wk₁．₅ : (m n : ℕ) → suc m ≤ n → m ≤ n
wk₁．₅ m n m<n =
let P = λ (Dm , Dn) → ((m , n , m<n) : Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] suc m ≤ n) → (Dm , Dn) ≡ (suc m , n) → m ≤ n
in basic-rec-ℕPair (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] suc m ≤ n) (λ (m , n , _) → m ≤ n) (λ (m , n , _) → (suc m , n))
(λ { (m , n , m<n) .(suc m) .n b refl →
basic-case-≤ (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] suc m ≤ n × Below-ℕPair P (suc m) n) (λ (m , n , _) → m ≤ n) (λ (m , n , m<n , _) → (suc m , n , m<n))
(λ { (m , n , m<n , b) m₀ n₀ m₀≡n₀ r₀ →
basic-case-ℕPair (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] Σ[ m<n ∈ suc m ≤ n ] Below-ℕPair P (suc m) n × Σ[ m₀ ∈ ℕ ] Σ[ n₀ ∈ ℕ ] Σ[ m₀≡n₀ ∈ m₀ ≡ n₀ ] (m₀ , n₀ , base m₀≡n₀) ≡ (suc m , n , m<n)) (λ (m , n , _) → m ≤ n) (λ (m , n , _) → (m , n))
(λ {(m , n , m<n , b , m₀ , n₀ , m₀≡n₀ , refl) refl → base refl})
(λ {(m , n , m<n , b , m₀ , n₀ , refl , refl) nₚ refl → step (base refl)})
(λ {(m , n , m<n , b , m₀ , n₀ , () , refl) mₚ refl})
(λ {(m , n , m<n , b , m₀ , n₀ , refl , refl) mₚ nₚ refl → step (base refl)})
(m , n , m<n , b , m₀ , n₀ , m₀≡n₀ , r₀)})
(λ { (m , n , m<n , b) m₀ n₀ m₀≤n₀ r₀ →
basic-case-ℕPair (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] Σ[ m<n ∈ suc m ≤ n ] Below-ℕPair P (suc m) n × Σ[ m₀ ∈ ℕ ] Σ[ n₀ ∈ ℕ ] Σ[ m₀≤n₀ ∈ m₀ ≤ n₀ ] (m₀ , suc n₀ , step m₀≤n₀) ≡ (suc m , n , m<n)) (λ (m , n , _) → m ≤ n) (λ (m , n , _) → (m , n))
(λ { (m , n , m<n , b , m₀ , n₀ , m₀≤n₀ , () ) refl })
(λ { (m , n , m<n , b , m₀ , n₀ , m₀≤n₀ , refl) nₚ refl → let ((_ , b') , _) = b in step (b' (zero , nₚ , m₀≤n₀) refl) })
(λ { (m , n , m<n , b , m₀ , n₀ , m₀≤n₀ , () ) mₚ refl })
(λ { (m , n , m<n , b , m₀ , n₀ , m₀≤n₀ , refl) mₚ nₚ refl → let ((_ , b') , _) = b in step (b' (suc mₚ , nₚ , m₀≤n₀) refl) })
(m , n , m<n , b , m₀ , n₀ , m₀≤n₀ , r₀) })
(m , n , m<n , b)})
(m , n , m<n)
At this point, we can individually rewrite the methods of the first and the second basic-case-ℕPair applications, so that within each application the methods become the same, allowing us to remove the base-case-≤ using the redundant-case-analysis law.
Like in our initial experiment, the methods in the second application of basic-case-ℕPair are more obviously the same, modulo substitution; unlike in the initial experiment, in this basic-analysis version we can make the methods exactly the same by choosing to solve the first unification constraint (generated by basic-case-≤) but not the second (generated by basic-case-ℕPair):
basic-case-ℕPair ...
(λ {(m , n , m<n , b , m₀ , n₀ , m₀≤n₀ , refl) r → let ((_ , b') , _) = b in step (b' (m , n₀ , m₀≤n₀) refl)})
(λ {(m , n , m<n , b , m₀ , n₀ , m₀≤n₀ , refl) nₚ r → let ((_ , b') , _) = b in step (b' (m , n₀ , m₀≤n₀) refl)})
(λ {(m , n , m<n , b , m₀ , n₀ , m₀≤n₀ , refl) mₚ r → let ((_ , b') , _) = b in step (b' (m , n₀ , m₀≤n₀) refl)})
(λ {(m , n , m<n , b , m₀ , n₀ , m₀≤n₀ , refl) mₚ nₚ r → let ((_ , b') , _) = b in step (b' (m , n₀ , m₀≤n₀) refl)})
...
The methods in the first application of basic-base-ℕPair correspond to where we got stuck in the initial experiment.
But here, using the same trick of selectively solving unification constraints, we can rewrite the methods to the same form too:
basic-case-ℕPair ...
(λ {(m , n , m<n , b , m₀ , n₀ , refl , refl) r → step (base refl)})
(λ {(m , n , m<n , b , m₀ , n₀ , refl , refl) nₚ r → step (base refl)})
(λ {(m , n , m<n , b , m₀ , n₀ , refl , refl) mₚ r → step (base refl)})
(λ {(m , n , m<n , b , m₀ , n₀ , refl , refl) mₚ nₚ r → step (base refl)})
...
Then we can remove these two basic-case-ℕPair applications using the redundant-case-analysis law, and almost reach the basic-analysis version of wk.
It’s only ‘almost’, because we haven’t transformed the outermost basic-rec-ℕ-Pair to basic-rec-≤; this requires law(s) that we won’t formulate this time, although we suspect that it’s about switching to use a different but related termination measure.
We can now explain the transformation from wk' to wk more precisely:
-
Whereas (Agda’s) dependent pattern matching implicitly includes a unification step, the basic-analysis translation lets us make the unification step explicit and separate from case analysis. This is crucial for completing the transformations from
wk'towk, because we can then control where unification takes place, which allows the programs to be rewritten to required forms. -
In our initial experiment with pattern-matching definitions, the merging of redundant cases in the
stepbranches succeeds only accidentally: Since Agda allows us to omit the impossible branches, we only see the two survivingstepclauses, and these can be merged after reordering. In the basic-analysis version, the omitted branches reappear as branches closed by contradiction, and further transformations are required to make all the branches the same.
Transforming wk' to wk, take 3: Fording
The direction looks promising, but a serious drawback is that the laws hold at the level of basic-analysis operators, not directly at the surface level of pattern-matching programs, so the laws can only be applied to translated programs, which are rather tedious though.
In particular, the delayed-constraint transformation (that got us to wk₁．₄) requires exposing unification constraints, which are implicit in pattern-matching programs.
However, if we think a bit more, the way in which basic analyses expose constraints can be thought of as some kind of Fording, which we should be able to perform on pattern-matching programs directly!
Let’s go back to wk₃ (where we got stuck in the initial experiment):
wk₃ : (m n : ℕ) → suc m ≤ n → m ≤ n
wk₃ zero zero (base _) = base refl
wk₃ zero (suc .zero) (base refl) = step (base refl)
wk₃ (suc m) zero (base ())
wk₃ (suc m) (suc .(suc m)) (base refl) = step (base refl)
wk₃ m (suc n) (step m<n) = step (wk₃ m n m<n)
Instead of matching and specialising m and n, we can introduce ‘Ford variables’ m' and n' and constraints that they are equal to m and n respectively, and then match and specialise m' and n' instead — this corresponds to how basic analyses keep the original input and output, and introduce constraints on the input (as well as new variables mentioned by the constraints):
wk₄ : (m n : ℕ) → suc m ≤ n → (m' n' : ℕ) → m' ≡ m → n' ≡ n → m ≤ n
wk₄ m n (base _) zero zero refl refl = base refl
wk₄ m n (base refl) zero (suc .zero) refl refl = step (base refl)
wk₄ m n (base ()) (suc m') zero refl refl
wk₄ m n (base refl) (suc m') (suc .(suc m')) refl refl = step (base refl)
wk₄ m n (step m<n) m' (suc n') refl refl = step (wk₄ _ _ m<n m' n' refl refl)
Even though I haven’t thought it through, I believe this Ford transformation always inserts refl as the proofs of the new constraints, which trigger unification.
Then (maybe assuming axiom K) we can ‘unmatch’ proofs as needed, thereby delaying unification.
For example, by ‘unmatching’ the two constraint arguments, we can make the first four clauses uniform except for the redundant case analysis on m' and n':
wk₅ : (m n : ℕ) → suc m ≤ n → (m' n' : ℕ) → m' ≡ m → n' ≡ n → m ≤ n
wk₅ m n (base refl) zero zero meq neq = step (base refl)
wk₅ m n (base refl) zero (suc n') meq neq = step (base refl)
wk₅ m n (base refl) (suc m') zero meq neq = step (base refl)
wk₅ m n (base refl) (suc m') (suc n') meq neq = step (base refl)
wk₅ m n (step m<n) m' (suc n') refl refl = step (wk₅ _ _ m<n m' n' refl refl)
And now we can remove the redundant case analysis:
wk₆ : (m n : ℕ) → suc m ≤ n → (m' n' : ℕ) → m' ≡ m → n' ≡ n → m ≤ n
wk₆ m n (base refl) m' n' meq neq = step (base refl)
wk₆ m n (step m<n) m' (suc n') refl refl = step (wk₆ _ _ m<n m' n' refl refl)
Interestingly, after removing the redundant case analysis, we can rematch the constraint proofs with refl,
wk₇ : (m n : ℕ) → suc m ≤ n → (m' n' : ℕ) → m' ≡ m → n' ≡ n → m ≤ n
wk₇ m n (base refl) m' n' refl refl = step (base refl)
wk₇ m n (step m<n) m' (suc n') refl refl = step (wk₇ _ _ m<n m' n' refl refl)
so that we can un-Ford the program and reach wk:
wk : (m n : ℕ) → suc m ≤ n → m ≤ n
wk m n (base refl) = step (base refl)
wk m (suc n) (step m<n) = step (wk m n m<n)
So actually there’s no need to go through the translation to basic analyses, which is a relief!
A more complete story
To put the post into context:
In Shin’s JFP pearl on top-down vs bottom-up sublist computation, he gave an equational specification (3.1) and a derivation of a function which he called upgrade; subsequently I expressed Shin’s specification (3.1) in a dependent type and reimplemented (and simultaneously verified) the function, which I called retabulate in the short story paper.
Shu-Ting and I were intrigued by how different the two solutions look.
After Shu-Ting’s numerous experiments, gradually we suspected that the first solution can be systematically transformed into the second, and a key step is switching from a two-level analysis on indices and then indexed data to a direct analysis on indexed data, as illustrated by the wk example.
The original example looks more like the following (which is still a simplified version; the complete code is included in the attached Agda file):
up : ∀ k → BTree A n (suc k) → 2 ≤ n → suc (suc k) ≤ n → BTree (Vec A (suc (suc k))) n (suc (suc k))
up k (tipN x) l₁ l₂ = ⊥-elim (n≮n (suc k) (≤′⇒≤ l₂))
up k (node (tip0 x) (tipN y)) l₁ l₂ = tipN (x ∷ y ∷ [])
up k (node (tip0 x) (node u u')) l₁ l₂ = node (mapB (λ q → x ∷ q ∷ []) (node u u')) (up zero (node u u') (s≤′s (bounded u')) (s≤′s (bounded u')))
up k (node (tipN x) u) l₁ l₂ = ⊥-elim (n≮n (suc k) (≤′⇒≤ l₂))
up k (node (node t t') (tipN x)) (step l₁) l₂ = tipN (unTip (up _ (node t t') l₁ (base refl)) ∷ʳ x)
up k (node (node t t') (node u u')) (base refl) l₂ = ⊥-elim (n≮0 (≤-pred (≤-pred (≤′⇒≤ l₂))))
up k (node (node t t') (node u u')) (step l₁) (base refl) = ⊥-elim (unbounded u')
up k (node (node t t') (node u u')) (step l₁) (step l₂) = node (zipBW _∷ʳ_ (up _ (node t t') l₁ (≤⇒≤′ (<⇒≤ (≤′⇒≤ l₂)))) (node u u')) (up _ (node u u') l₁ l₂)
This up function is a dependently typed reimplementation of Shin’s upgrade function.
Roughly speaking, up transforms a tree to another by performing pattern matching on the input tree; the trees have indexed types that express shape constraints, and on the indices there are some more constraints, which are conditions assumed by Shin’s specification (3.1).
Upon closer inspection, Shin’s derivation starts with analyses on the indices and the constraints/conditions.
If up used the same case analysis strategy, with the arguments rearranged in the order in which they are analysed, it would look like
up' : 2 ≤ n → ∀ k → suc (suc k) ≤ n → BTree A n (suc k) → BTree (Vec A (suc (suc k))) n (suc (suc k))
up' (base refl) k (base refl) (node (tip0 x) (tipN y)) = tipN (x ∷ y ∷ [])
up' (base refl) k (step l₂) t with step (base ()) ← l₂
up' (step l₁) k (base refl) (node (tip0 x) (tipN y)) with step (base ()) ← l₁
up' (step l₁) .(suc _) (base refl) (node (node t t') (tipN x)) = tipN (unTip (up' l₁ _ (base refl) (node t t')) ∷ʳ x)
up' (step l₁) .(suc _) (base refl) (node (node t t') (node u u')) = ⊥-elim (unbounded u')
up' (step l₁) zero (step l₂) (tipN x) = ⊥-elim (n≮0 (≤′⇒≤ l₂))
up' (step l₁) zero (step l₂) (node (tip0 x) u) = node (mapB (λ q → x ∷ q ∷ []) u) (up' l₁ zero l₂ u)
up' (step l₁) (suc k) (step l₂) (tipN x) = ⊥-elim (n≮n (suc (suc k)) (≤′⇒≤ (step l₂)))
up' (step l₁) (suc k) (step l₂) (node t u) = node (zipBW _∷ʳ_ (up' l₁ k (≤⇒≤′ (≤-pred (≤′⇒≤ (step l₂)))) t) u) (up' l₁ (suc k) l₂ u)
We believe that up and up' are related by the simple transformations described in this post.
A more complete story involves more transformations:
Shin started with an equational specification, which, as a type, looks like
2 ≤ n → ∀ k → suc (suc k) ≤ n → ∀ t → ch k xs ≡ t → ⋯
The involved functions can be replaced by inductively defined relations, for example
2 ≤ n → ∀ k → suc (suc k) ≤ n → ∀ t → Ch k xs t → ⋯
where the equation involving ch is replaced by a relation Ch whose inhabitants are execution traces of ch.
The output tree t is a simplified representation of those traces, so Ch looks like an algebraic ornamentation of BTree, which brings us closer to up'.
Our hunch is that by applying a somewhat long series of transformations we may be able to get from Shin’s equational proof to the retabulate function on trees; each of the transformations may not be surprising, but the overall effect would be.
Alas, this means that if we want to write a paper, we’ll need to cover quite a few transformations to make the paper interesting enough, but the workload seems too much.
It might be worth a try if we could find more convincing examples, but examples also turned out to be difficult to conceive.
So this is where we have to stop, write things up, and hope that suitable examples and follow-up ideas will show up some day.
On the other hand, this was a nice opportunity for us to start studying the underlying mechanisms that make dependently typed programming practical (compared with, for example, programming directly in Martin-Löf type theory). We read Goguen et al’s Eliminating dependent pattern matching and followed the reference to Conor’s Elimination with a motive, which was probably where the basic analysis idea was first published (although we actually like Goguen et al’s succinct presentation more). In these translations and our final version of transformations, Fording has been shown to be a technique that’s more important than it looks, but with the advent of homotopy type theory it’s less clear how harmless Fording is. Even though I’m not eager to embrace the full generality of homotopy type theory, it’s still important to be aware of the big picture, so I think at some point I’ll need to read the sequel Eliminating dependent pattern matching without K as well as Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory by Cockx et al. Also written by Cockx et al (who have revised all the papers for JFP — very impressive) is Elaborating dependent (co)pattern matching: No pattern left behind, but I’m less sure about this one about (Agda’s) case trees because I’ve found Epigram’s approach to be clearer (without having to rely on argument reordering to try to express case analysis strategies, for example) and more general/extensible, as explained in The view from the left.
Agda file: BasicAnalysis.agda
