Systems D and DC: A Dependent Haskell Core Specification

Prerequisites. Direct starred prerequisites: Chapter 131. The dependent function and equality rules of chapter 26 supply the remaining prerequisites. No later core chapter depends on this route.

Consider the vector zip whose two arguments are known to have the same length: $$\mathsf{zip}:{\mathrm{\Pi }}^{-}n:\mathsf{Nat}\to {\mathrm{\Pi }}^{-}a:\star \to {\mathrm{\Pi }}^{-}b:\star \to \mathsf{Vec}an\to \mathsf{Vec}bn\to \mathsf{Vec}(a,b)n.$$ Three of its five arguments are marked ${\mathrm{\Pi }}^{-}$: the length $n$ and the two element types are to be erased before the program runs. In chapter 131 that decision was made by a syntactic class — types and coercions were erased, terms were kept. Here $n$ is a natural number, an ordinary run-time value of an ordinary type, and yet it must be erased. The class “type” has stopped coinciding with the class “erasable”.

Nor can erasability be read off the type. The body of $\mathsf{zip}$ matches on a vector whose constructor carries an equality constraint, and the branch for the empty vector must produce a value at type $\mathsf{Vec}(a,b)n$ using the assumption $n=0$. Reusing the mechanism of chapter 131, that assumption is a coercion, and the coercion must also be erased. So a single calculus must classify three different things — what is computed, what is erased, and what is proved — and it must do so while allowing types to contain arbitrary, possibly divergent, terms.

This chapter freezes Systems D and DC of Weirich, Voizard, Azevedo de Amorim and Eisenberg (2017), whose syntax, judgments, typing rules, definitional equality and prop equality are that paper’s Figures 1–9. D is the implicit language: it has no annotations and an undecidable type system, and it is where the soundness argument lives. DC is the annotated language: its type checking is decidable and its types are unique, and it is connected to D by an erasure that forgets exactly the annotations.

System D

Three binders must be distinguished at once. ${\lambda }^{+}$ abstracts a value the body may use; ${\lambda }^{-}$ abstracts a value the body may not use, and whose argument is therefore written $◻$ at the application site; $\mathrm{\Lambda }c$ abstracts a proof of an equality proposition, discharged by the token $\bullet$. The three eliminations are $a{b}^{+}$, $a{◻}^{-}$ and $a[\bullet ]$.

Reduction is call by name and deterministic. The one rule that is not standard is E-AbsTerm, which reduces under an irrelevant abstraction; correspondingly ${\lambda }^{-}x.v$ is a value only when its body is one. The reason is visible in the source language: a Haskell generalization $\mathrm{\Lambda }a.e$ must not delay the evaluation of $e$, because the source program has no abstraction there at all. Since D marks the position of an erased argument rather than deleting it, the reduction rule has to compensate.

Two features of definition 132.3 are worth stating before they are used. The relevance side condition of E-Abs is a condition on the body, not on the type: ${\lambda }^{-}x.a$ is well typed exactly when $x$ does not occur free in $a$, so an irrelevant argument is parametric in the strong sense that the body cannot inspect it. And E-Wff makes propositions homogeneous: $a{\sim }_{A}b$ is well formed only when $a$ and $b$ have the same type $A$. Remark 132.23 records what that choice buys.

Definitional equality and the available set

The judgment is homogeneously typed, and this is the first property to record.

Proof of Lemma 132.6 — Regularity of definitional equality

Proof. Induction on the equality derivation. E-Refl and E-Beta carry the typing of one side as a premise and obtain the other from theorem 132.11. E-Sym and E-Trans are immediate from the induction hypotheses. Each congruence rule reassembles the typing of both sides from the typings supplied by its premises, using the corresponding typing rule. E-Assn reads the proposition $a{\sim }_{A}b$ out of $\mathrm{\Gamma }$; since $\models \mathrm{\Gamma }$, E-Wff was checked when the binding was formed, so both $\mathrm{\Gamma }\models a:A$ and $\mathrm{\Gamma }\models b:A$. E-EqConv moves both typings along an equality of types by E-Conv. E-PiFst and E-PiSnd obtain their conclusions by inverting the typing of the two $\mathrm{\Pi }$-types delivered by the induction hypothesis and applying lemma 132.9 in the second case. ◻

E-Assn is what separates this system from an ordinary intensional type theory: an assumed proposition may be used directly as a definitional equality. That is what makes a GADT branch type check, and it is exactly the feature that forces the available set into the judgment.

Proof of Lemma 132.9 — Substitutivity

Proof. Induction on the typing derivation of $b$, building the equality congruence that matches each typing rule. At E-Var for $x$ the conclusion is the hypothesis; at any other variable, E-Refl. At E-Abs, E-App, E-Pi, E-CAbs and E-CApp the induction hypotheses feed E-AbsCong, E-AppCong, E-PiCong, E-CAbsCong and E-CAppCong, whose available sets are the same $\mathrm{\Delta }$ in every position that carries the equality. The step that fails in a system whose congruence rules add the bound coercion variable to $\mathrm{\Delta }$ is E-CAbs: there the body is compared under $c:\varphi$, and if that comparison had to be carried out in $\mathrm{\Delta },c$ the induction hypothesis, stated for $\mathrm{\Delta }$, would not apply. Because definition 132.5 keeps $\mathrm{\Delta }$ fixed, the induction goes through. ◻

Type soundness for D

Proof of Lemma 132.10 — Inversion for abstraction

Proof. Induction on the typing derivation. The derivation ends either in E-Abs, which gives the four conclusions with $A={\mathrm{\Pi }}^{\rho }x:A_1\to B_1$ and the equality by E-Refl, or in E-Conv, whose premise $\mathrm{\Gamma }\models {\lambda }^{\rho }x.b_0:A^{\prime }$ yields the data by the induction hypothesis and whose equality $A^{\prime }\equiv A$ is composed with the returned one by E-Trans. No other rule has a $\lambda$ as its subject. ◻

Proof of Theorem 132.11 — Preservation

Proof. The mechanism is worth naming: conversion makes inversion deliver a type that is only definitionally equal to the one in hand, so each beta case needs the injectivity of the corresponding type former to recover the domain and codomain. That is why E-PiFst, E-PiSnd, E-CPiFst and E-CPiSnd belong to definition 132.5 rather than being derived afterwards.

E-AppAbs. Let $\mathrm{\Gamma }\models ({\lambda }^{\rho }x.v)a^{\rho }:A$. Inverting the application rule gives $\mathrm{\Gamma }\models {\lambda }^{\rho }x.v:{\mathrm{\Pi }}^{\rho }x:A_0\to B_0$, $\mathrm{\Gamma }\models a:A_0$ and $A=B_0[a/x]$. Lemma 132.10 gives $A_1,B_1$ with $\mathrm{\Gamma };\tilde{\mathrm{\Gamma }}\models {\mathrm{\Pi }}^{\rho }x:A_0\to B_0\equiv {\mathrm{\Pi }}^{\rho }x:A_1\to B_1:\star$ and $\mathrm{\Gamma },x:A_1\models v:B_1$. By E-PiFst, $\mathrm{\Gamma };\tilde{\mathrm{\Gamma }}\models A_0\equiv A_1:\star$, so E-Conv gives $\mathrm{\Gamma }\models a:A_1$ and lemma 132.9 applied to the typing of $v$ gives $\mathrm{\Gamma }\models v[a/x]:B_1[a/x]$. By E-PiSnd with E-Refl on $a$, $\mathrm{\Gamma };\tilde{\mathrm{\Gamma }}\models B_0[a/x]\equiv B_1[a/x]:\star$, and one more E-Conv returns the type $A$.

E-CAppCAbs. The same argument with E-CPiFst and E-CPiSnd in place of E-PiFst and E-PiSnd, and with the substitution $b[\bullet /c]$ replacing $v[a/x]$.

E-Axiom. E-Fam types $F$ at the $A$ recorded in ${\mathrm{\Sigma }}_0$, and well-formedness of ${\mathrm{\Sigma }}_0$ gives $\varnothing \models a:A$; weakening moves it to $\mathrm{\Gamma }$.

For one-step reduction, E-Prim is the three cases above, and E-AbsTerm, E-AppLeft and E-CAppLeft rebuild the typing derivation from the induction hypothesis using E-Abs, E-App or E-IApp, and E-CApp respectively. In E-AbsTerm the side condition $x\notin \mathrm{fv}(a)$ is preserved, because reduction does not introduce free variables. ◻

Consistency

The soundness argument now has three steps: equality with an empty available set implies joinability; parallel reduction is confluent; and joinable types are consistent. The middle step is a substantial rewriting theorem and is imported exactly.

This is Theorem 4.6 of Weirich, Voizard, Azevedo de Amorim, and Eisenberg (2017). It is imported for their parallel reduction, defined for the syntax of definition 132.1 with the signature ${\mathrm{\Sigma }}_0$ treated opaquely. What it supplies here is exactly the diamond property; every use of it below is through theorem 132.16. No other property of parallel reduction is assumed, and nothing in this chapter reproves it.

Proof of Theorem 132.15 — Equality implies joinability

Proof. Induction on the equality derivation. The available set is empty, so E-Assn cannot fire — this is the one place where the restriction of definition 132.5 does the work, and it is why the theorem is stated with $\varnothing$. E-Refl gives $a{\Rightarrow }^{\ast }a$. E-Beta gives $a_1\Rightarrow a_2$, since every primitive reduction is a parallel reduction step. E-Sym is symmetry of $\iff$. E-Trans needs theorem 132.14: from $a{\Rightarrow }^{\ast }{d}_1$, $a_1{\Rightarrow }^{\ast }{d}_1$, $a_1{\Rightarrow }^{\ast }{d}_2$, $b{\Rightarrow }^{\ast }{d}_2$, confluence gives a common reduct of $d_1$ and $d_2$, hence of $a$ and $b$. Every congruence rule is handled by joining the components and reassembling, because parallel reduction is a congruence. E-PiFst, E-PiSnd, E-CPiFst and E-CPiSnd are handled by observing that a common reduct of two $\mathrm{\Pi }$-types is a $\mathrm{\Pi }$-type whose components are common reducts of the components, again by theorem 132.14. ◻

Proof of Theorem 132.16 — Joinability implies consistency

Proof. Parallel reduction does not change the head form of $\star$, ${\mathrm{\Pi }}^{\rho }x:A\to B$ or $\mathrm{\forall }c:\varphi .A$: no reduction rule has one of these as a redex, and the congruence clauses rebuild the same head. So if $A{\Rightarrow }^{\ast }b$ and $B{\Rightarrow }^{\ast }b$ and both $A$ and $B$ are in head form, both heads equal the head of $b$. ◻

Proof of Theorem 132.19 — Progress

Proof. Induction on the typing derivation. E-Star, E-Pi and E-CPi give values. E-Var cannot occur, since $a$ has no free term variable. E-Fam gives an E-Axiom step. E-Conv passes to its premise.

E-Abs. If $\rho =+$ the term is a value. If $\rho =-$, the induction hypothesis applies to the body in $\mathrm{\Gamma },x:A$; the extra binding is a term variable that does not occur free in the body, by the side condition of E-Abs, so the hypothesis of the theorem is preserved. Either the body is a value, and then ${\lambda }^{-}x.a$ is one, or the body steps, and E-AbsTerm lifts the step.

E-App and E-IApp. Apply the induction hypothesis to the function. If it steps, E-AppLeft lifts the step. If it is a value $v$ of type ${\mathrm{\Pi }}^{\rho }x:A_0\to B_0$, then corollary 132.17 applies: by lemma 132.10 and the value grammar, $v$ is one of ${\lambda }^{\rho }x.b$, $\star$, a $\mathrm{\Pi }$-type, a $\mathrm{\forall }$-type or $\mathrm{\Lambda }c.b$. A closed value of the last four shapes has type $\star$ or a $\mathrm{\forall }$-type, and $\mathrm{\Gamma };\varnothing \models$ that type $\equiv {\mathrm{\Pi }}^{\rho }x:A_0\to B_0$ would identify two different head forms, contradicting corollary 132.17. The available set is empty because $\mathrm{\Gamma }$ has no coercion assumption. Hence $v={\lambda }^{\rho }x.b$ and E-AppAbs applies.

E-CApp. The same argument, with the $\mathrm{\forall }$ head form, gives $v=\mathrm{\Lambda }c.b$ and an E-CAppCAbs step. ◻

System DC

D is not a checker: E-Conv has an undecidable premise, and E-App guesses the type of an abstraction’s argument. DC reifies the derivation.

Three changes carry the whole difference. An-Abs checks relevance against the erasure of the body, because the annotation $A$ may legitimately mention $x$; An-App needs no separate irrelevant rule, because the argument is present in both cases; and An-Conv replaces the undecidable equality premise by a proof $\gamma$ that the checker only has to verify.

This is Lemma 5.6 of Weirich, Voizard, Azevedo de Amorim, and Eisenberg (2017). Three weaker alternatives were available — requiring $A=B$, requiring $A$ and $B$ to be $\alpha$-equivalent, or requiring nothing — and the reason for this one is compositionality: with $A=B$, the congruence rule for application would have to insert a coercion around one side to make the two dependent result types agree, and would no longer be symmetric in its two premises.

Proof of Lemma 132.25 — Decidability and uniqueness

Proof. Uniqueness is by induction on $a$: every rule of definition 132.21 is determined by the outermost form of its subject, and each reads its result type off the subject’s annotations — An-Abs from $A$ and the body’s unique type, An-App by substituting the actual argument, An-Conv from the coercion’s right-hand side, An-CApp by substituting the supplied proof. Since there is no rule whose subject is arbitrary, no conversion rule applies silently. Decidability follows: the syntax-directed reading of the rules is a terminating recursion on $a$, whose only non-structural obligation is checking a coercion, and definition 132.22 is likewise syntax directed on $\gamma$, with An-Beta requiring only one primitive reduction step of an erased term and a syntactic comparison. ◻

Erasure and annotation

The clause $|a{b}^{-}|=|a|{◻}^{-}$ is the one that answers the opening obstruction: the argument disappears, the application site does not. The clause $|a▸\gamma |=|a|$ deletes every equality proof, exactly as in chapter 131.

Proof of Lemma 132.27 — Erasure and annotation

Proof of the first half. Induction on the DC typing derivation, rule by rule. An-Star, An-Var, An-Fam, An-Pi and An-CPi erase to the identically named D rules. An-Abs erases to E-Abs: its side condition is stated on $|a|$, which is exactly the side condition of E-Abs at the erased body. An-App at $\rho =+$ erases to E-App; at $\rho =-$ it erases to E-IApp, whose premise $\mathrm{\Gamma }\models a:A$ is supplied by the induction hypothesis applied to the actual argument that DC carries and D deletes. An-CAbs erases to E-CAbs. An-CApp erases to E-CApp, its coercion premise becoming the equality premise by the erasure of the coercion judgment. An-Conv erases to E-Conv, because the erasure of $a▸\gamma$ is $|a|$ and the coercion becomes a definitional equality. The second half is Lemma 5.5 of the frozen source; its proof constructs annotations by recursion on the D derivation and is not reproduced here. ◻

The steps that erase to an equality are exactly those that only move an annotation or a cast; the pattern is the same as theorem 131.35 of chapter 131, and it is what licenses the following reading of the two languages.

Proof of Corollary 132.29 — Annotations do not change behaviour

Proof. Both erase to the same D term, and by lemma 132.28 every DC step of either projects to a step or to nothing in D. Since D reduction is deterministic, the two erased reduction sequences coincide. ◻

That is the practical content of the pair D/DC. In the $\mathsf{zip}$ of the opening, a type inferencer may produce the empty-vector branch with the proof $c_1$ or with the proof $c_2$; the two annotated programs are different DC terms, they erase to the same D term, and corollary 132.29 says the choice is invisible at run time.

Limits and seminar

The frozen source is Weirich, Voizard, Azevedo de Amorim and Eisenberg (2017), together with its Coq development. Every rule displayed above is theirs, and the theorem statements retain their exact hypotheses: theorem 132.15 holds only for the empty available set; theorem 132.19 holds only for contexts without coercion assumptions and without free term variables; lemma 132.24 relates the types of the two sides only up to a derivable equality. Theorem 132.14 is imported, not reproved.

Four boundaries are worth stating plainly. First, nothing here is a theorem about GHC. D and DC have no primitive datatypes, no pattern matching, no type classes and no roles; the vector examples are encodings, and the compiler’s front end is not modelled. Second, corollary 132.17 is not logical consistency, and example 132.4 shows why: every type is inhabited. Third, the signature ${\mathrm{\Sigma }}_0$ is treated opaquely, so the results hold for any well-formed signature but say nothing about a particular set of recursive definitions beyond its well-formedness. Fourth, D’s type system is undecidable, so lemma 132.25 is a statement about DC only; the implicit language is a specification and an inspiration for inference, not an algorithm.

The relation to chapter 131 is one of replacement, not extension. FC keeps a syntactic separation of types from terms and erases the former; DC conflates them and erases whatever is marked $\rho =-$. A coercion is explicit in both, and both admit an erasure theorem, but no FC theorem transfers to DC by that resemblance: FC’s consistency is a condition on top-level axioms, whereas D’s is a proved property of definitional equality with an empty available set.

[4]

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 132.6, then complete exercise 132.9.

Exercise 132.6¶

★★☆ Encode the two-constructor vector type of the opening as a Scott-encoded D term, give the type of the cons constructor including its equality constraint, and type the empty-vector branch of $\mathsf{zip}$, naming the use of E-Assn and the available set at that point.

Referenced from 3 locations

• Systems D and DC: A Dependent Haskell Core Specification

Exercise 132.7¶

★★★ The impossible branches of $\mathsf{zip}$ are discharged by a contradiction between $n\sim 0$ and $n\sim \mathsf{Succ}m$. Write the D derivation that takes those two assumptions to an equality of two constructor applications with different heads, and then explain why corollary 132.17 does not apply to it. State precisely what has to be true of the context for the branch to be unreachable.

Referenced from 2 locations

• Systems D and DC: A Dependent Haskell Core Specification

Exercise 132.8¶

★★★ Consider three candidate variants of E-CPiCong: the printed rule; the rule that adds $c$ to $\mathrm{\Delta }$; and the rule that requires ${\varphi }_1={\varphi }_2$ syntactically. For each, say whether theorem 132.15, lemma 132.9 and theorem 132.19 survive, giving either a proof sketch of the surviving case or a counterexample.

Referenced from 2 locations

• Systems D and DC: A Dependent Haskell Core Specification

Exercise 132.9 — Practical: relevance and erasure checker¶

★★★ Practical project.dc-relevance-erasure Complete project dc-relevance-erasure. Implement, for a finite fragment of D and DC, (i) the DC typing rules An-Star, An-Var, An-Abs, An-App, An-CAbs, An-CApp and An-Conv, (ii) the annotation erasure of definition 132.26, (iii) the D one-step reduction of definition 132.2 including E-AbsTerm, and (iv) the head-form consistency test of definition 132.12. The invariant the implementation must maintain is that a term accepted by the DC checker erases to a term accepted by the D checker at the erased type, so that lemma 132.27 holds on every accepted input. The named cases print

irrelevant-use: rejected
erased-application: ok
two-annotations-one-erasure: ok
reduce-under-irrelevant: value
int-bool: inconsistent

The checker is independent evidence for the finite fragment; it does not prove theorem 132.11, theorem 132.19, does not decide D typing, and does not implement the coercion language of definition 132.22 beyond An-Refl, An-Assn and An-Beta.

Referenced from 3 locations

• Systems D and DC: A Dependent Haskell Core Specification