Intrinsic typing and proof economy: Complex indices
Over the past few months, I worked with Shin to extract and update a part of the short story on binomial tabulation as a more ordinary pearl for JFP, and just submitted it. The original short story has been uploaded to arXiv, where I expect it to stay forever. Writing the short story was more like an experiment; I’m still very happy with the outcome (and go back to read and enjoy it myself from time to time), but as a test for whether my taste matches that of the general PL community, I now believe the result is negative. It is more important to produce stuff that advances science though, rather than stuff that’s optimised to leave good impressions on people in a limited amount of time.
I started to ponder how to explain the kind of ‘proof economy’ that intrinsic typing can achieve in 0040.
There I compared a few versions of vector append with different amounts of proof effort, and saw that the usual proof-free version (append₀) corresponds to a version (append₁) that handles a proof explicitly but in a simple way.
What I think should be done is formalise such correspondence, so that it is clear what kind of proof is/can be hidden.
More specifically, I want to compare (data) types that differ in only one feature, and then state how to convert programs from one type to the other, so as to explain how that feature affects how we write programs (and proofs).
A simplest example is the technique of converting a complex target index in an inductive family, for example the final ‘suc n’ in
data Vec (A : Set) : ℕ → Set where
[] : Vec A zero
_∷_ : A → Vec A n → Vec A (suc n)
to a variable constrained by an equality, as in
data Vec' (A : Set) : ℕ → Set where
[] : Vec' A zero
cons : A → Vec' A n → suc n ≡ r → Vec' A r
Intuitively, wherever we write x ∷ xs with Vec we write cons x xs refl with Vec', dealing with the equality proof explicitly in the latter case.
The technique/conversion can also be applied backwards and interpreted as saying that what we gain by using the complex target index in Vec is the ability to omit the refl in cons.
Note that the conversion is only applied to cons (and not to nil), so the difference between the data types is as localised as possible.
Hopefully such conversions will compose, so that when we use multiple features we can deduce what the combined effect is.
For example, apply the technique to both cons and nil to get
data Vec'' (A : Set) : ℕ → Set where
nil : zero ≡ r → Vec'' A r
cons : A → Vec'' A n → suc n ≡ r → Vec'' A r
and we’ll know that we’re exposing equality proofs in both constructors.
When it comes to differences between data types, one thinks of ornaments.
(Indeed, there are ornaments from Vec to Vec'' and vice versa.)
Moreover, ornamental isomorphisms do capture the idea of proof economy to some extent — for example, the isomorphism Vec A n ≅ Σ[ xs ∈ List A ] length xs ≡ n can be interpreted as saying that a vector has the same content as a pair of a list and a proof about its length (so manipulating the vector can be thought of as manipulating the pair simultaneously).
In a similar vein, we could easily prove that Vec A n ≅ Vec'' A n, and inspecting the two-way conversions in the isomorphism will show that we’re adding or removing refl.
But that’s not the full story.
The isomorphism seems to suggest that Vec and Vec'' are the same, but in fact they behave differently in practice, and we ought to capture that in a theory.
For example, when we write a function like
f : Vec A (g m) → ⋯
f [] = ?
f (x ∷ xs) = ?
where the index g m in the type of the input vector is complex, the case splitting would fail because g m cannot be unified with zero or suc n.
Switching to Vec'' delays unification and allows case splitting:
f'' : Vec'' A (g m) → ⋯
f'' (nil eq) = {! ⋯ ⊣ eq : zero ≡ g m !}
f'' (cons x xs eq) = {! ⋯ ⊣ x : A; xs : Vec'' A n; eq : suc n ≡ g m !}
The isomorphism doesn’t capture this difference. To see the difference, ultimately one would need to compare the two data types within the theory of dependent pattern matching, but that theory is rather complex. Instead, I hope that I can do the comparison in terms of elimination rules.
It turns out that, in the more basic setting with only elimination rules, it’s fine to use the ordinary Vec.
Recall that the elimination rule of Vec is
Vec-elim : {A : Set} (P : ∀ {n} → Vec A n → Set)
→ P []
→ (∀ x {n} (xs : Vec A n) → P xs → P (x ∷ xs))
→ ∀ {n} (xs : Vec A n) → P xs
In the type of f we want to quantify over all indices of the form g m.
To do that with Vec-elim, which lets us quantify over any n, we should restrict n to the form g m in the motive P.
That is, using the elimination rule we should aim for this equivalent type
∀ {A n} → Vec A n → ∀ {m} → n ≡ g m → ⋯
--------------------
and set the underlined part as the motive.
Apply this function to refl, and we get back to the original type of f:
f : Vec A (g m) → ⋯
f {A} xs₀ =
Vec-elim (λ {n} xs → ∀ {m} → n ≡ g m → Vec A (h m))
(λ eq → {! ⋯ ⊣ eq : zero ≡ g m !})
(λ x xs ih eq → {! ⋯ ⊣ x : A
; xs : Vec A n
; ih : ∀ {m} → n ≡ g m → ⋯
; eq : suc n ≡ g m !})
xs₀
refl
The holes correspond to those we get after doing case splitting in the definition of f''.
In fact for the second hole the Vec-elim version may be preferable because an inductive call can be made by proving n ≡ g m for some m, whereas in the f'' version we cannot apply f'' to xs before we somehow unify n with some g m, which is a stricter requirement than exhibiting a proof of n ≡ g m.
That is, the transformation from a complex index to a variable with an equality constraint should be applied outside the data type definition for maximum flexibility; whether the transformation is applied inside the data type definition doesn’t seem important.
Hm, that doesn’t work as I expected.
I wanted to explain how the index transformation affects the usability of Vec and Vec'', but actually the transformation isn’t inherently tied to data types, and can —or should— be applied elsewhere, and even to type families, not just inductive families.
I think the example does show that the familiar Agda data type definitions and dependent pattern matching already help to hide a lot of equality proofs.
I’ve never really dug into the translation from dependent pattern matching definitions to eliminators (with or without K), but I think I have a vague impression that equality types are crucially involved (and therefore having the K axiom or not leads to different treatments).
It’ll probably be worthwhile to (seriously) study the translation and explain it more explicitly in terms of proof economy, but I suspect there won’t be much new stuff to develop.
Hopefully, by going through a few more examples that I’ve already had in mind and will write about, I’ll be able to find new things to say.
