‘Induction principles are propositions’ revisited
The binomial tabulation story turns out to be difficult to publish, and Shin and I are about to rewrite the first half about dependently typed programming into a functional pearl for JFP (in the short and traditional format that everyone expects). One revelation in the story was that two implementations of an induction principle may be proved to be extensionally equal using parametricity, which was briefly described in 0036. After some discussion with Zhixuan, I think there’s a more accurate perspective, which will be described below (in terms of the induction principle on natural numbers) as well as go into the pearl (in terms of the immediate sublist induction principle), but there are problems that we cannot resolve too. I’m keeping a record of the problems here, and maybe someone will be able to shed light on them.
The first thing Zhixuan pointed out was that the computation rules were a defining part of an induction principle too. For example, in addition to
IndType : Set₁
IndType = (P : ℕ → Set) (pz : P zero) (ps : ∀ {n} → P n → P (suc n))
→ (n : ℕ) → P n
which is only the type of the standard induction principle of natural numbers, we should also specify the computation rules
Comp : IndType → Set₁
Comp f = (P : ℕ → Set) (pz : P zero) (ps : ∀ {n} → P n → P (suc n))
→ f P pz ps zero ≡ pz
× (∀ {n} → f P pz ps (suc n) ≡ ps (f P pz ps n))
which complete the definition of the induction principle:
Ind : Set₁
Ind = Σ IndType Comp
We can then prove that Ind is a proposition even when ℕ : Set, zero : ℕ, and suc : ℕ → ℕ are declared as (module) parameters about which we know nothing except their types (as opposed to an inductive type and its two constructors).
The essential part of the proof is
uniqueness : (f g : IndType) → Comp f → Comp g
→ (P : ℕ → Set) (pz : P zero) (ps : ∀ {n} → P n → P (suc n))
→ (n : ℕ) → f P pz ps n ≡ g P pz ps n
uniqueness f g f-comp g-comp P pz ps =
f (λ n → f P pz ps n ≡ g P pz ps n)
(begin
f P pz ps zero
≡⟨ proj₁ (f-comp P pz ps) ⟩
pz
≡⟨ proj₁ (g-comp P pz ps) ⟨
g P pz ps zero
∎)
(λ {n} eq →
begin
f P pz ps (suc n)
≡⟨ proj₂ (f-comp P pz ps) ⟩
ps (f P pz ps n)
≡⟨ cong ps eq ⟩
ps (g P pz ps n)
≡⟨ proj₂ (g-comp P pz ps) ⟨
g P pz ps (suc n)
∎)
This can then be straightforwardly extended to (i j : Ind) → i ≡ j if we have function extensionality and know that ℕ is an h-set.
Therefore, by including Comp in Ind, we characterise the notion uniquely and make the definition nice and tight.
In relation to the above, which is standard knowledge, the revelation in the binomial tabulation story can be described as follows: one of f and g can be assumed to satisfy unary parametricity instead of the computation rules, and we’ll still have a proof.
Concretely, define unary parametricity by
Param : IndType → Set₁
Param g =
{P : ℕ → Set} (Q : ∀ {n} → P n → Set)
{pz : P zero} (qz : Q pz)
{ps : ∀ {n} → P n → P (suc n)} (qs : ∀ {n} {p : P n} → Q p → Q (ps p))
{n : ℕ} → Q (g P pz ps n)
and we can prove
uniqueness' : (f g : IndType) → Comp f → Param g
→ (P : ℕ → Set) (pz : P zero) (ps : {n : ℕ} → P n → P (suc n))
→ (n : ℕ) → f P pz ps n ≡ g P pz ps n
uniqueness' f g f-comp g-param P pz ps n =
g-param (λ {n} p → f P pz ps n ≡ p)
(proj₁ (f-comp P pz ps))
(λ { refl → proj₂ (f-comp P pz ps) })
This is useful when f is the standard implementation of the induction principle, which satisfies the computation rules even judgementally, and g is a non-standard one which cannot be easily proved to satisfy the computation rules (in the case of binomial tabulation, Shin needed to write an entire paper to prove that).
By contrast, proving parametricity is mechanical if not automatic, so we get to avoid a potentially difficult proof of the computation rules.
Note that the second and third arguments of g-param are essentially just f-comp.
This is no coincidence:
The invariant we use, namely λ {n} p → f P pz ps n ≡ p, states that any p : P n (constructed within g) can only be the result computed by f P pz ps n.
This invariant should hold for pz : P zero, that is, f P pz ps zero should compute to pz; it should also be preserved by ps, that is, whenever f P pz ps n computes to p : P n, f P pz ps (suc n) should compute to ps p — or equivalently, f P pz ps (suc n) computes to ps (f P pz ps n).
These together say that f P pz ps computes its results using pz and ps, and are exactly the computation rules of f P pz ps.
Also note that parametricity plays a crucial role: in a language where quantification over Set is not necessarily parametric, g P pz ps may for example be able to match P against a specific type family, and then use known operations other than pz and ps for that specific type family, which, unlike pz and ps, may not preserve the invariant.
Zhixuan suggested an alternative two-part proof: first derive the computation rules from parametricity,
Param→Comp : (g : IndType) → Param g → Comp g
and then just invoke uniqueness since both f and g satisfy the computation rules now.
This looked plausible to me — intuitively, parametricity seems to imply that g P pz ps can only apply ps to pz exactly n times if it wants to produce something of type P n.
But this intuition is based on the assumption that ℕ is an inductive type with zero and suc as its constructors, so that, for example, ∀ {n} → suc n ≢ n — otherwise suc could well be id, and there would be no restriction on how many times ps is applied.
Zhixuan’s proof of Param→Comp actually goes through uniqueness' and hence assumes that the computation rules have been established, albeit for another induction function, and I don’t feel comfortable calling it a derivation of the computation rules from parametricity.
In any case, uniqueness' is more fundamental, and I’ll just use uniqueness' in the JFP pearl.
On the other hand, I still wonder whether we can obtain the computation rules from some weaker assumptions and parametricity, rather than inheriting them from another induction function.
However, we prove uniqueness' by invoking parametricity with the invariant ‘p is equal to the result of an induction function’, which we cannot even state if there’s no induction function yet.
I tried to define the induction function as a relation instead, but that relation would still be inductively defined, and programming with that relation may still be argued to be assuming (some more generic notion of) induction.
And, without induction on natural numbers, it doesn’t seem possible to derive the computation rules from that relation (or I think equivalently, turn that relation into a function).
In any case, as long as we’re using a variant of the invariant, we’d need to prove the computation rules to finish invoking parametricity.
In the end I suspect that we have to assume something no weaker than the computation rules — that is, it might be possible to prove something like
(P : IndType → Set₁)
→ ((f : IndType) → Param f → P f → Comp f)
→ (f : IndType) → P f → Comp f
but I have no idea how to prove it, internally or externally (Zhixuan surmises that this is independent of MLTT/Agda), even if we change the antecedent (f : IndType) → Param f → P f → Comp f to something more intensional to allow more analysis.
Maybe an expert in parametricity would have some ideas, but I’m definitely not that person.
Agda file: InductionPropositional.agda
