Induction principles are propositions
I’ve had a chance to play with parametricity for dependent types, and one exercise is to prove that the extensional behaviour of an induction principle is uniquely determined by the parametricity of the type of the principle — that is, the type of an induction principle is a proposition. Take the standard induction principle for natural numbers for example:
Ind : Set₁
Ind = (P : ℕ → Set)
→ (pz : P zero)
→ (ps : ∀ {n} → P n → P (suc n))
→ (n : ℕ) → P n
Intuitively, since P is parametrically quantified, a function inhabiting Ind can do nothing but use the arguments pz and ps to construct any required P n, and moreover, there is only one way to do that, namely applying ps to pz exactly n times.
We certainly know how to write one such function:
ind : Ind
ind P pz ps zero = pz
ind P pz ps (suc n) = ps (ind P pz ps n)
To prove that Ind is uniquely inhabited, one way is to use its unary parametricity:
Ind-unary-parametricity : Ind → Set₁
Ind-unary-parametricity f =
(P : ℕ → Set) (Q : ∀ {n} → P n → Set)
→ (pz : P zero) (qz : Q pz)
→ (ps : ∀ {n} → P n → P (suc n)) (qz : (∀ {n} {p : P n} → Q p → Q (ps p))
→ (n : ℕ) → Q (f P pz ps n)
Externally, through Bernardy et al’s translation, every program f : Ind induces a program of type Ind-unary-parametricity f, which performs essentially the same computation as f.
I’d like to think that a program cannot peek into parametrically quantified types (like P above), so we can sneak extra stuff into those types, for example some extra proof (like Q above), and the program will have to process the original data and the bundled extra stuff in exactly the same way, not being able to separate them.
As an external observer, we can make a copy of the program that focuses on only the extra stuff, and that’s the induced program.
We can do the translation manually for ind, and can in fact reuse ind to make it clear that it’s the same computation:
ind-parametric : Ind-unary-parametricity ind
ind-parametric P Q pz qz ps qs = ind (Q ∘ ind P pz ps) qz qs
Logically, Q is an additional invariant that we can impose on P-values.
If the invariant holds for pz and is preserved by ps, then it has to hold for any outcome.
Which invariant should we choose?
We know that actually any p : P n can only be ind P pz ps n, so let Q {n} p = (p ≡ ind P pz ps n), and we’re done.
uniqueness :
(f : Ind) → Ind-unary-parametricity f
→ (P : ℕ → Set) (pz : P zero) (ps : ∀ {n} → P n → P (suc n))
→ (n : ℕ) → f P pz ps n ≡ ind P pz ps n
uniqueness f param P pz ps n =
param P (λ {n} p → p ≡ ind P pz ps n) pz refl ps (cong ps) n
What’s more interesting is that essentially the same proof works for the immediate sub-list induction principle discussed in 0034. This induction principle can be implemented using a top-down algorithm or a bottom-up one. 0034 used string diagrams to compare the two algorithms and proved that they have the same extensional behaviour, but the equality proof can actually be done more simply by noting that both algorithms have the same type, which is uniquely inhabited. The proof (for a slightly generalised version of the induction principle) is included in the supplementary Agda file.
Agda file: UniquenessOfInductionPrinciples.agda
