If we want to go the built-in quotient type route, it might be good looking at the compatible extension of Coq logic by Pierre Courtieu that allow for quotient type that have a normalization function.
I think the original paper is : Normalized Types by Pierre Courtieu
It's a fairly elegant approach, but from a programming-language perspective I don't really like its computational behavior, because it calls the canonicalization function every time you do a `case` on such an object.
Also, in the case of α-equivalence of λ terms, such a canonicalization function seems rather non-trivial (you can't use deb-indices encoded as strings because it doesn't behave correctly, you can't use deb-levels because the canonicalization function can't know how many vars are in the surrounding context, so I guess it would have to allocate var names deterministically, which seems to imply you have to traverse the whole term to canonicalize it, which means that the cost of every `case` ends up being not constant-time but of time proportional to the size of the term).
Stefan
The good think is that in this paper most of the proofs of this extended CIC calculus are done by translating terms of this new extension into terms of the plain CIC. But typer has macros. So instead of adding built-in quotient type, we could do like Racket and add built-in facilities to defined new language with the help of macros. So you could defined Typer Core without quotient, and Typer (the user language) with the quotient type but in fact this is just a translation to the Typer Core kernel.
That would be a powerful demonstration of the capabilities of Typer's macros. Simple kernel and yet powerful quotient type.
On 2017-12-13 11:07 PM, Stefan Monnier wrote:
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 _______________________________________________ Typer mailing list Typer@iro.umontreal.ca https://webmail.iro.umontreal.ca/mailman/listinfo/typer
Typer mailing list Typer@iro.umontreal.ca https://webmail.iro.umontreal.ca/mailman/listinfo/typer