I've been reading the HoTT book and thinking about how it could
influence the design of Typer.
I can't see how to integrate something like the univalence axiom because
it seems problematic from a programming-language point of view (at
least for now).
But the feature that I can see more or less how to provide in Typer is
higher-order inductive types (HIT). These are basically inductive types
annotated with additional constraints in the form of
equality constructors.
E.g.
type ListSet α
| nil
| cons α (ListSet α)
with nomulti: (x ∈ S) -> (S = cons x S)
| noorder: Permutation S₁ S₂ -> (S₁ = S₂)
The idea here is that rather than try to design some representation of
sets which is canonical, we use some convenient representation
(e.g. a list) and then state boldly the additional properties we need
for it to be "canonical".
And by magic, the ListSet is thus made canonical: `nomulti` and
`noorder` are now *new* constructors for the equality type `Eq`.
In order for those equality to make sense, the HIT system imposes that
whenever a piece of code wants to look at a ListSet, it has to
promise/prove that it will obey those additional properties (i.e. that
its return value will not depend on the ordering of elements in the
list or on the number of repetitions of a given element).
HITs can also have additional equality constraints between equality
proofs, i.e. meta-equality proofs, and meta-meta-equality, ...
[ homotopy type theory spends most of its time playing with equality
proofs ], but I'm not very interested in those for now.
I don't want to extend Typer's inductive types with such fanciness:
I already find those inductive types to be "too big" and would rather
decompose them into smaller elements (tags, sums, and products), but I'd
be interested in providing some support for it in Typer.
So, let's start with a particular instance of a HIT: the quotient
types/sets. Let's call `Quotient T R`, the type of elements of type
T where if two elements of x1:T and x2:T are in the relation
R (i.e. there's a proof P : R x1 x2) then we consider them equivalent:
Quotient : (τ : Type) → (τ → τ → Type) → Type;
Qin : τ → Quotient τ R;
Qeq : R x₁ x₂ → Qin{R} x₁ = Qin{R} x₂;
and then the eliminator needs to have a type along the lines of:
Qout : (f : τ → α) → (R x₁ x₂ → f x₁ = f x₂) ≡> (x : Quotient τ R) → α;
where `f` is the function which gets to look at the element `x` and
where the argument of type (R x₁ x₂ → f x₁ = f x₂) is the proof that
this function `f` will treat "equals as equals" (if given two
equivalent inputs, it will return equivalent outputs).
As always, I find it useful to try to represent it via the impredicative
encoding:
Quotient τ R = (α : Type) ≡> (f : τ → α) → (R x₁ x₂ → f x₁ = f x₂) ≡> → α;
Qin x = λα ≡> λ f → λ _ ≡> f x;
Qout x = x;
and interestingly, we see that the argument that proves that `f` is
well-behaved is not used here. Instead it's needed in `Qeq`: in order to
prove `R x₁ x₂ → Qin{R}x₁ = Qin{R}x₂` we can use that proof argument to
argue that the function `Qin{R}x₁` is extensionally equivalent to the
function `Qin{R}x₂`. So we need the functional extensionality axiom in
order to prove this and thus provide an impredicative encoding of
Quotient types.
In practice, such an encoding is rather problematic, as usual, because
it does not allow us to use α at other Type levels of the universe
hierarchy (Type_1, Type_2, ...).
Interestingly, if we assume that `Quotient` exists, we can pretty much
encode any HIT using it. E.g.
type Exp Γ τ
| var (x : String) ((x : τ) ∈ Γ) : Exp Γ τ
| app (Exp Γ (τ₁ → τ₂)) (Exp Γ τ₁) : Exp Γ τ₂
| lam (x : String) (Exp ((x : τ₁) · Γ) τ₂) : Exp Γ (τ₁ → τ₂)
where α-equiv : y ∉ fv e → lam x e = lam y (e[y/x]);
can be encoded using Quotient as:
Exp' : ?G → ?T → Type;
Rexp : Exp' ?Γ ?τ → Exp' ?Γ ?τ → Type;
Exp Γ τ = Quotient (Exp' Γ τ) (Rexp Γ τ);
type Exp' Γ τ
| var' (x : String) ((x : τ) ∈ Γ) : Exp' Γ τ
| app' (Exp Γ (τ₁ → τ₂)) (Exp Γ τ₁) : Exp' Γ τ₂
| lam' (x : String) (Exp ((x : τ₁) · Γ) τ₂) : Exp' Γ (τ₁ → τ₂);
var x P = Qin (var' x P);
app e₁ e₂ = Qin (app' e₁ e₂);
lam x e = Qin (lam' x e);
type Rexp Γ τ x y
| rα-equiv (y ∉ fv e) : Rexp (lam x e) (lam y (subst e x (var y)))
α-equiv x = Qeq (rα-equiv x);
But the termination checker (which here will check the non-negative
occurrence of `Exp` in its definition) needs to handle `Quotient` as
a "positive constructor", and that likely needs to be done in an
ad-hoc way.
So, I think I can add HITs to Typer without really modifying the
inductive types, and instead providing a built-in Quotient type, and
teaching the termination checker about it.
Stefan
