Chapter 131Optional

Explicit Equality Evidence and System FC

Prerequisites. Direct starred prerequisites: none. System F, higher kinds, existential abstraction and the dependent equality rules supply the mathematical prerequisites; no compiler or Haskell knowledge is assumed. No later core chapter depends on this route.

A source language may declare a data type whose constructors constrain the type index they return. The standard example is an expression type with three constructors, $\begin{aligned} Zero & : Exp Int, & Succ & : Exp Int \to Exp Int, \\ Pair & : Exp b \to Exp c \to Exp (b, c), \end{aligned}$ together with an evaluator whose declared type is $eval : Exp a \to a$ . In the $Zero$ branch the evaluator must return the literal $0$ , and $0$ has type $Int$ , not $a$ .

Try to type that branch in System F extended by algebraic data types with existential components and higher kinds — write $F_{A}$ for that language. The branch body must be given the result type $a$ , so the only possible leaf is $\frac{0 : Int \in Γ}{Γ ⊢ 0 : a} FA - Const .$ The premise of FA-Const is $0 : a \in Γ$ . The displayed tree is therefore not a derivation. No other rule repairs it: in $F_{A}$ type equality is syntactic identity of types, the type variable $a$ is not the type constant $Int$ , and there is no rule whose conclusion changes the type of a term. The branch cannot be typed at all.

The information the branch is missing is not a value. It is the fact, established by the pattern match, that in this branch $a$ and $Int$ may be interchanged. System $F C (X)$ records that fact as a first-class object of the type language, and every place where the fact is used is marked in the term. This chapter freezes the calculus $F C (X)$ of Sulzmann, Chakravarty, Peyton Jones and Donnelly (2007), whose syntax, typing rules, kinding rules and operational semantics are its Figures 1–4, audits its rules for regularity, proves substitution, preservation, progress, consistency and erasure at their exact hypotheses, and elaborates the GADT source fragment into it.

The frozen $F C (X)$ signature

Definition 131.1 — Symbol classes and raw syntax ¶

Fix disjoint countable sets of type variables $a, b, c, c o$ , term variables $x, f$ , coercion constants $C$ , value type constructors $T$ , type functions $S^{n}$ of declared arity $n$ , and data constructors $K$ . Sorts, kinds, types-and-coercions, terms, patterns and environments are generated by $\begin{aligned} δ & ::= TY ∣ CO, \\ κ, ι & ::= ⋆ ∣ κ_{1} \to κ_{2} ∣ σ_{1} \sim σ_{2}, \\ d & ::= a ∣ T, & g & ::= c o ∣ C, \\ φ, ρ, σ, τ, υ, γ & ::= a ∣ C ∣ T ∣ φ_{1} φ_{2} ∣ S^{n} φ^{n} ∣ \forall a : κ . φ \\ ∣ sym γ ∣ γ_{1} \circ γ_{2} ∣ γ @ φ ∣ left γ ∣ right γ \\ ∣ γ_{1} \sim γ_{2} ∣ leftc γ ∣ rightc γ ∣ γ_{1} ▸ γ_{2}, \\ u & ::= x ∣ K, \\ e & ::= u ∣ Λ a : κ . e ∣ e φ ∣ λ x : σ . e ∣ e_{1} e_{2} \\ ∣ let x : σ = e_{1} in e_{2} \\ ∣ case e_{1} of \overset{―}{p \to e_{2}} ∣ e ▸ γ, \\ p & ::= K \overset{―}{b : κ} \overset{―}{x : σ}, \\ Γ & ::= ϵ ∣ Γ, u : σ ∣ Γ, d : κ ∣ Γ, g : κ ∣ Γ, S^{n} : κ . \end{aligned}$ The metavariables $ρ, σ, τ, υ$ are used where only a regular type can stand and $γ$ where only a coercion can stand; the distinction is enforced by the kinding rules, not by the grammar. Write $κ \Rightarrow σ$ for $\forall_: κ . σ$ when the bound variable does not occur in $σ$ , and $\overset{―}{φ^{n}}$ for a sequence $φ_{1} \dots φ_{n}$ . A type function symbol $S^{n}$ occurs only in the saturated form $S^{n} φ^{n}$ .

Referenced from 6 locations

Explicit Equality Evidence and System FC

The language has no type-level lambda, so equality of regular types is syntactic identity up to renaming of bound variables. Every departure from that identity must be carried by an explicit coercion.

Definition 131.2 — Kind well-formedness ¶

The judgment $Γ ⊢_{k} κ : δ$ is generated by

Γ ⊢_{k} ⋆ : TY

Star

Γ ⊢_{k} κ_{1} : TY

Γ ⊢_{k} κ_{2} : TY

Γ ⊢_{k} κ_{1} \to κ_{2} : TY

FunK

Γ ⊢_{TY} σ_{1} : κ

Γ ⊢_{TY} σ_{2} : κ

Γ ⊢_{k} σ_{1} \sim σ_{2} : CO

EqTy

Γ ⊢_{k} γ_{1} : CO

Γ ⊢_{k} γ_{2} : CO

Γ ⊢_{k} γ_{1} \sim γ_{2} : CO

EqCo

Referenced from 6 locations

Explicit Equality Evidence and System FC

EqTy requires the two sides of an equality kind to have one kind. That single premise is what makes the coercion judgment below a statement about comparable objects, and section 131.4 shows that four of the printed coercion rules fail to preserve it.

Definition 131.3 — Type kinding ¶

d : κ \in Γ

Γ ⊢_{k} κ : TY

Γ ⊢_{TY} d : κ

TyVar

Γ ⊢_{TY} σ_{1} : κ_{1} \to κ_{2}

Γ ⊢_{TY} σ_{2} : κ_{1}

Γ ⊢_{TY} σ_{1} σ_{2} : κ_{2}

TyApp

S^{n} : κ^{n} \to ι \in Γ

Γ ⊢_{TY} σ_{i} : κ_{i} (1 \leq i \leq n)

Γ ⊢_{TY} S^{n} σ^{n} : ι

TySCon

Γ, a : κ ⊢_{TY} σ : ⋆

Γ ⊢_{k} κ : δ

a \notin fv (Γ)

Γ ⊢_{TY} \forall a : κ . σ : ⋆

TyAll

Referenced from 5 locations

Explicit Equality Evidence and System FC

Two consequences are needed constantly and are proved once.

Lemma 131.4 — Kind uniqueness ¶

If $Γ ⊢_{TY} σ : κ$ and $Γ ⊢_{TY} σ : κ^{'}$ then $κ = κ^{'}$ .

Referenced from 7 locations

Explicit Equality Evidence and System FC

Proof of Lemma 131.4 — Kind uniqueness

Proof. The four rules of definition 131.3 have pairwise distinct subjects: an atom, an application $σ_{1} σ_{2}$ , a saturated type-function application, and a quantified type. So the last rule of both derivations is the same, and we induct on $σ$ . For TyVar the kind is read off the unique binding of $d$ in $Γ$ . For TySCon it is the result kind $ι$ of the unique declaration of $S^{n}$ . For TyAll it is $⋆$ . For TyApp the induction hypothesis gives one kind $κ_{1} \to κ_{2}$ for $σ_{1}$ ; an arrow kind determines $κ_{2}$ . ◻

Lemma 131.5 — Weakening ¶

Let $Γ^{'}$ extend $Γ$ by bindings whose subjects do not occur in $Γ$ . Then each of $Γ ⊢_{k} κ : δ$ , $Γ ⊢_{TY} σ : κ$ , $Γ ⊢_{CO} γ : κ$ and $Γ ⊢_{e} e : σ$ implies the same judgment under $Γ^{'}$ .

Referenced from 6 locations

Explicit Equality Evidence and System FC

Proof of Lemma 131.5 — Weakening

Proof. Every rule of definition 131.2, definition 131.3, definition 131.6, definition 131.7 either has no environment premise, or looks a binding up in $Γ$ , or extends the environment by one fresh binding. Lookups survive the extension because $Γ$ is a sub-environment of $Γ^{'}$ ; binder rules survive after renaming the bound variable away from the finitely many subjects of $Γ^{'}$ . A structural induction on the derivation, replacing $Γ$ by $Γ^{'}$ at each node, gives the four statements simultaneously. ◻

Definition 131.6 — Coercion kinding ¶

d : κ \in Γ

Γ ⊢_{k} κ : TY

Γ ⊢_{CO} d : d \sim d

CoRefl

g : σ \sim τ \in Γ

Γ ⊢_{CO} g : σ \sim τ

CoVar

Γ ⊢_{CO} γ : σ \sim τ

Γ ⊢_{CO} sym γ : τ \sim σ

Sym

Γ ⊢_{CO} γ_{1} : σ_{1} \sim σ_{2}

Γ ⊢_{CO} γ_{2} : σ_{2} \sim σ_{3}

Γ ⊢_{CO} γ_{1} \circ γ_{2} : σ_{1} \sim σ_{3}

Trans

Γ, a : κ ⊢_{CO} γ : σ \sim τ

Γ ⊢_{k} κ : TY

a \notin fv (Γ)

Γ ⊢_{CO} \forall a : κ . γ : \forall a : κ . σ \sim \forall a : κ . τ

CoAllT

Γ ⊢_{CO} γ : \forall a : κ . σ \sim \forall b : κ . τ

Γ ⊢_{TY} υ : κ

Γ ⊢_{CO} γ @ υ : σ [υ / a] \sim τ [υ / b]

CoInstT

Γ ⊢_{CO} γ_{1} : σ_{1} \sim τ_{1}

Γ ⊢_{CO} γ_{2} : σ_{2} \sim τ_{2}

Γ ⊢_{TY} σ_{1} σ_{2} : κ

Γ ⊢_{CO} γ_{1} γ_{2} : σ_{1} σ_{2} \sim τ_{1} τ_{2}

Comp

Γ ⊢_{CO} γ_{i} : σ_{i} \sim τ_{i} (1 \leq i \leq n)

Γ ⊢_{TY} S^{n} σ^{n} : κ

Γ ⊢_{CO} S^{n} γ^{n} : S^{n} σ^{n} \sim S^{n} τ^{n}

SComp

Γ ⊢_{CO} γ : σ_{1} σ_{2} \sim τ_{1} τ_{2}

Γ ⊢_{CO} left γ : σ_{1} \sim τ_{1}

Left

Γ ⊢_{CO} γ : σ_{1} σ_{2} \sim τ_{1} τ_{2}

Γ ⊢_{CO} right γ : σ_{2} \sim τ_{2}

Right

Γ ⊢_{CO} γ : κ_{1} \sim κ_{2}

Γ ⊢_{CO} γ^{'} : σ_{1} \sim σ_{2}

Γ ⊢_{k} κ_{1} : CO

Γ ⊢_{CO} γ \Rightarrow γ^{'} : κ_{1} \Rightarrow σ_{1} \sim κ_{2} \Rightarrow σ_{2}

CompC

Γ ⊢_{CO} γ : κ_{1} \Rightarrow σ_{1} \sim κ_{2} \Rightarrow σ_{2}

Γ ⊢_{CO} leftc γ : κ_{1} \sim κ_{2}

LeftC

Γ ⊢_{CO} γ : κ_{1} \Rightarrow σ_{1} \sim κ_{2} \Rightarrow σ_{2}

Γ ⊢_{CO} rightc γ : σ_{1} \sim σ_{2}

RightC

Γ ⊢_{CO} γ_{1} : σ_{1} \sim τ_{1}

Γ ⊢_{CO} γ_{2} : σ_{2} \sim τ_{2}

Γ ⊢_{CO} γ_{1} \sim γ_{2} : (σ_{1} \sim σ_{2}) \sim (τ_{1} \sim τ_{2})

EqCoerce

Γ ⊢_{CO} γ_{1} : κ

Γ ⊢_{CO} γ_{2} : κ \sim κ^{'}

Γ ⊢_{CO} γ_{1} ▸ γ_{2} : κ^{'}

CastC

The rule named EqCoerce is the rule printed as $(\sim)$ in the source.

Referenced from 8 locations

Explicit Equality Evidence and System FC

Two features of definition 131.6 deserve to be noticed before any of it is used. First, CoRefl witnesses reflexivity of an atom by the atom itself: the coercion $Int$ has kind $Int \sim Int$ . Lemma 131.11 extends that to every well-kinded type. Second, Left and Right apply to ordinary application $φ_{1} φ_{2}$ and not to $S^{n} φ^{n}$ ; the saturation requirement of definition 131.1 is what keeps the two apart, and remark 131.14 shows what decomposing a type function would cost.

Definition 131.7 — Term typing and patterns ¶

u : σ \in Γ

Γ ⊢_{e} u : σ

Var

Γ ⊢_{TY} σ_{x} : ⋆

Γ, x : σ_{x} ⊢_{e} e : σ

Γ ⊢_{e} λ x : σ_{x} . e : σ_{x} \to σ

Abs

Γ ⊢_{e} e_{1} : σ_{2} \to σ_{1}

Γ ⊢_{e} e_{2} : σ_{2}

Γ ⊢_{e} e_{1} e_{2} : σ_{1}

App

Γ ⊢_{e} e_{1} : σ_{1}

Γ, x : σ_{1} ⊢_{e} e_{2} : σ_{2}

Γ ⊢_{e} let x : σ_{1} = e_{1} in e_{2} : σ_{2}

Let

Γ, a : κ ⊢_{e} e : σ

Γ ⊢_{k} κ : δ

a \notin fv (Γ)

Γ ⊢_{e} Λ a : κ . e : \forall a : κ . σ

AbsT

Γ ⊢_{e} e : \forall a : κ . σ

Γ ⊢_{k} κ : δ

Γ ⊢_{δ} φ : κ

Γ ⊢_{e} e φ : σ [φ / a]

AppT

Γ ⊢_{e} e : σ

Γ ⊢_{CO} γ : σ \sim τ

Γ ⊢_{e} e ▸ γ : τ

Cast

Γ ⊢_{e} e : σ

Γ ⊢_{p} p_{j} \to e_{j} : σ \to τ (1 \leq j \leq m)

Γ ⊢_{e} case e of \overset{―}{p \to e} : τ

Case

K : \forall \overset{―}{a : κ} . \forall \overset{―}{b : ι} . \overset{―}{σ} \to T \overset{―}{a} \in Γ

θ = \overset{―}{[υ / a]}

Γ, \overset{―}{b : θ (ι)}, \overset{―}{x : θ (σ)} ⊢_{e} e : τ

Γ ⊢_{p} K \overset{―}{b : θ (ι)} \overset{―}{x : θ (σ)} \to e : T \overset{―}{υ} \to τ

Alt

In AppT the metavariable $δ$ is $TY$ when $κ$ is a type kind and $CO$ when $κ$ is an equality kind, so one rule covers both type application and coercion application. A binder $b : ι$ of a data constructor is existential when $ι$ is a type kind and a coercion binder when $ι$ is an equality kind.

Referenced from 4 locations

Explicit Equality Evidence and System FC

Definition 131.8 — Declarations and programs ¶

A program is $pgm ::= \overset{―}{decl}; e$ with $\begin{aligned} decl & ::= data T : κ where \overset{―}{K : \forall \overset{―}{a : κ} . \forall \overset{―}{b : ι} . \overset{―}{σ} \to T \overset{―}{a}} \\ ∣ type S^{n} : κ^{n} \to ι ∣ axiom C : σ_{1} \sim σ_{2} . \end{aligned}$ Declaration checking uses

Γ ⊢_{k} κ : TY

Γ, T : κ ⊢_{TY} σ_{K} : ⋆ for each K

Γ ⊢ (data T : κ where \overset{―}{K : σ_{K}}) : (T : κ, \overset{―}{K : σ_{K}})

Data

Γ ⊢_{k} κ_{i} : TY

Γ ⊢_{k} ι : TY

Γ ⊢ (type S^{n} : κ^{n} \to ι) : (S^{n} : κ^{n} \to ι)

Type

Γ ⊢_{k} κ : CO

Γ ⊢ (axiom C : κ) : (C : κ)

Coerce

A program $\overset{―}{decl}; e$ is well typed at $σ$ when the declarations extend the initial environment $Γ_{0}$ to $Γ$ and $Γ ⊢_{e} e : σ$ . An environment produced this way is a top-level environment: it binds only $T$ , $S^{n}$ , $K$ and $C$ , and no type variable, coercion variable or term variable.

Referenced from 3 locations

Explicit Equality Evidence and System FC

Remark 131.9 — One corrected premise in Data ¶

The printed declaration rule checks $Γ ⊢_{TY} σ : ⋆$ in $Γ$ . A constructor type mentions the type constructor it builds — $Zero : \forall a : ⋆ . \forall c o : a \sim Int . Exp a$ mentions $Exp$ — so that premise is never derivable for a recursive declaration. Data above checks the constructor types in $Γ, T : κ$ . Nothing else in the calculus changes, and every later proof uses the corrected rule.

Referenced from 3 locations

Explicit Equality Evidence and System FC

Example 131.10 — The evaluator that F_A could not type ¶

Declare $data Exp : ⋆ \to ⋆ where \begin{aligned} Zero : \forall a : ⋆ . (a \sim Int) \Rightarrow Exp a, \\ Succ : \forall a : ⋆ . (a \sim Int) \Rightarrow Exp Int \to Exp a . \end{aligned}$ The $Zero$ branch that had no $F_{A}$ derivation now has one. In the alternative $Zero (c o : a \sim Int)$ the pattern binds $c o$ , so CoVar gives $Γ ⊢_{CO} c o : a \sim Int$ , Sym gives $Γ ⊢_{CO} sym c o : Int \sim a$ , and Cast gives $\frac{\begin{matrix} Γ ⊢_{e} 0 : Int \\ \frac{\frac{c o : a \sim Int \in Γ}{Γ ⊢_{CO} c o : a \sim Int} CoVar}{Γ ⊢_{CO} sym c o : Int \sim a} Sym \end{matrix}}{Γ ⊢_{e} 0 ▸ sym c o : a} Cast .$ The whole evaluator is $eval = Λ a : ⋆ . λ e : Exp a . case e of {\begin{cases} Zero (c o : a \sim Int) \to 0 ▸ sym c o \\ Succ (c o : a \sim Int) (e^{'} : Exp Int) \\ \to (eval Int e^{'} + 1) ▸ sym c o . \end{cases}$ The evidence appears twice in the term and nowhere in the run-time behaviour: theorem 131.35 shows that both casts vanish.

Referenced from 6 locations

Explicit Equality Evidence and System FC

Exercise 131.1 ¶

★☆☆ Write the derivation of $Γ ⊢_{e} (eval Int e^{'} + 1) ▸ sym c o : a$ in the $Succ$ branch of example 131.10, naming the rule at every node. Then say which single premise fails if $sym$ is deleted.

Referenced from 2 locations

Explicit Equality Evidence and System FC

Constructing and decomposing evidence

Reflexivity is stated for atoms only. The first thing to prove is that it holds for every well-kinded type, and that the witness is the type itself. The coercion language contains no separate reflexivity constant, so the two clauses below must be proved together: the quantifier case $κ \Rightarrow σ$ needs reflexivity of the equality kind $κ$ , which CoAllT cannot supply.

Lemma 131.11 — Reflexivity ¶

If $Γ ⊢_{TY} φ : κ$ then $Γ ⊢_{CO} φ : φ \sim φ$ .
If $Γ ⊢_{k} κ : CO$ then $Γ ⊢_{CO} κ : κ \sim κ$ .

Referenced from 6 locations

Explicit Equality Evidence and System FC

Proof of Lemma 131.11 — Reflexivity

Proof. Simultaneous induction on the two derivations.

Clause 1. TyVar: CoRefl applies to the same premises and gives $Γ ⊢_{CO} d : d \sim d$ . TyApp $φ = σ_{1} σ_{2}$ : the induction hypothesis gives $Γ ⊢_{CO} σ_{i} : σ_{i} \sim σ_{i}$ , and Comp, whose third premise is the kinding of $σ_{1} σ_{2}$ already in hand, gives $Γ ⊢_{CO} σ_{1} σ_{2} : σ_{1} σ_{2} \sim σ_{1} σ_{2}$ . TySCon: the same with SComp. TyAll $φ = \forall a : κ . σ$ : split on the sort of $κ$ . If $Γ ⊢_{k} κ : TY$ , the induction hypothesis in $Γ, a : κ$ and CoAllT give $Γ ⊢_{CO} \forall a : κ . σ : \forall a : κ . σ \sim \forall a : κ . σ$ . If $Γ ⊢_{k} κ : CO$ , then $a \notin fv (σ)$ and $φ = κ \Rightarrow σ$ ; clause 2 gives $Γ ⊢_{CO} κ : κ \sim κ$ , clause 1 for $σ$ gives $Γ ⊢_{CO} σ : σ \sim σ$ , and CompC gives $Γ ⊢_{CO} κ \Rightarrow σ : κ \Rightarrow σ \sim κ \Rightarrow σ$ .

Clause 2. EqTy $κ = σ_{1} \sim σ_{2}$ : clause 1 gives $Γ ⊢_{CO} σ_{i} : σ_{i} \sim σ_{i}$ , and EqCoerce gives $Γ ⊢_{CO} σ_{1} \sim σ_{2} : (σ_{1} \sim σ_{2}) \sim (σ_{1} \sim σ_{2})$ . EqCo: the same with the induction hypothesis of clause 2 on the two component kinds. ◻

The reflexivity witness is the mechanism behind the whole calculus: to lift a coercion $γ$ through a type $φ$ , replace one CoRefl leaf of the reflexivity derivation of $φ$ by $γ$ .

Theorem 131.12 — Lifting ¶

Let $a \notin fv (Γ)$ and $Γ ⊢_{CO} γ : σ_{1} \sim σ_{2}$ with $Γ ⊢_{TY} σ_{1} : κ^{'}$ and $Γ ⊢_{TY} σ_{2} : κ^{'}$ .

If $Γ, a : κ^{'} ⊢_{TY} φ : κ$ then $Γ ⊢_{CO} φ [γ / a] : φ [σ_{1} / a] \sim φ [σ_{2} / a]$ .
If $Γ, a : κ^{'} ⊢_{k} κ : CO$ then $Γ ⊢_{CO} κ [γ / a] : κ [σ_{1} / a] \sim κ [σ_{2} / a]$ .

Referenced from 7 locations

Explicit Equality Evidence and System FC

Proof of Theorem 131.12 — Lifting

Proof. The obstruction is that $γ$ has one fixed kind while $φ$ may place $a$ under applications, type functions and quantifiers. The decisive move is to run the reflexivity proof of lemma 131.11 on $φ$ and change exactly the leaves at which $a$ is reached; the invariant is that after processing a subterm $ψ$ , the constructed coercion has kind $ψ [σ_{1} / a] \sim ψ [σ_{2} / a]$ . Formally we induct simultaneously on the two kinding derivations.

Clause 1. TyVar with $d = a$ : then $κ = κ^{'}$ , $φ [γ / a] = γ$ and $φ [σ_{i} / a] = σ_{i}$ , so the conclusion is the hypothesis on $γ$ . TyVar with $d \neq a$ : the substitution leaves $d$ unchanged and lemma 131.11 gives $Γ ⊢_{CO} d : d \sim d$ . TyApp $φ = φ_{1} φ_{2}$ : the induction hypothesis gives $Γ ⊢_{CO} φ_{j} [γ / a] : φ_{j} [σ_{1} / a] \sim φ_{j} [σ_{2} / a]$ for $j = 1, 2$ . Lemma 131.18 gives $Γ ⊢_{TY} (φ_{1} φ_{2}) [σ_{1} / a] : κ$ , which is the third premise of Comp; that rule then gives the required coercion, because substitution commutes with application. TySCon: identical with SComp. TyAll $φ = \forall b : ι . ψ$ , where $b$ is chosen outside $fv (γ) \cup fv (σ_{1}) \cup fv (σ_{2}) \cup fv (Γ) \cup {a}$ . If $Γ ⊢_{k} ι : TY$ , weaken $γ$ to $Γ, b : ι$ by lemma 131.5, apply the induction hypothesis to $ψ$ there, and conclude by CoAllT. If $Γ ⊢_{k} ι : CO$ , then $φ = ι \Rightarrow ψ$ with $b \notin fv (ψ)$ ; clause 2 applied to $ι$ and clause 1 applied to $ψ$ feed CompC.

Clause 2. EqTy $κ = υ_{1} \sim υ_{2}$ : clause 1 gives coercions $υ_{j} [γ / a]$ of kind $υ_{j} [σ_{1} / a] \sim υ_{j} [σ_{2} / a]$ , and EqCoerce assembles $υ_{1} [γ / a] \sim υ_{2} [γ / a]$ at exactly the required kind. EqCo: the same with clause 2 on the two component kinds. ◻

Clause 2 is what makes the constructor-push rule of section 131.5 type-correct, and it is the reason the coercion language contains the forms $γ_{1} \sim γ_{2}$ and $γ_{1} ▸ γ_{2}$ at all.

Example 131.13 — Lifting through a data type and a quantifier ¶

Let $Γ ⊢_{CO} γ : σ_{1} \sim σ_{2}$ with both sides of kind $⋆$ , and let $Tree : ⋆ \to ⋆$ . Taking $φ = Tree a$ , theorem 131.12 produces the coercion $Tree γ$ of kind $Tree σ_{1} \sim Tree σ_{2}$ : the head is the reflexivity witness $Tree$ supplied by CoRefl, and the argument is $γ$ . Taking $φ = \forall b : ⋆ . a \to Int$ gives $Γ ⊢_{CO} \forall b : ⋆ . γ \to Int : \forall b : ⋆ . σ_{1} \to Int \sim \forall b : ⋆ . σ_{2} \to Int,$ where $γ \to Int$ abbreviates $(\to) γ Int$ , an instance of Comp whose head is the reflexivity witness $(\to)$ .

Referenced from 2 locations

Explicit Equality Evidence and System FC

Decomposition runs the other way. From $Γ ⊢_{CO} γ : Tree σ_{1} \sim Tree σ_{2}$ , Right extracts $Γ ⊢_{CO} right γ : σ_{1} \sim σ_{2}$ . Decomposition is the step that the elaboration of section 131.8 cannot do without, and it is also the step whose soundness depends on a property of the type language rather than of the coercion language.

Remark 131.14 — Why type functions are saturated ¶

Suppose $S^{1}$ were allowed to appear unapplied, so that $S^{1} σ$ counted as an ordinary application. With the two axioms $C_{1} : S^{1} Int \sim Bool$ and $C_{2} : S^{1} Bool \sim Bool$ the coercion $C_{1} \circ sym C_{2}$ has kind $S^{1} Int \sim S^{1} Bool$ , and Right would produce a coercion of kind $Int \sim Bool$ . Both axioms are individually harmless — they say only that a type function takes the value $Bool$ at two arguments — so the failure is caused by decomposition, not by the axioms. Keeping $S^{n} φ^{n}$ syntactically distinct from $φ_{1} φ_{2}$ removes the Right step: the premise of Right does not match $S^{1} Int \sim S^{1} Bool$ . The same restriction stops a partial type-function application from instantiating a type variable, so a variable of higher kind ranges over injective constructors only.

Referenced from 3 locations

Explicit Equality Evidence and System FC

Exercise 131.2 ¶

★☆☆ Let $Γ ⊢_{CO} γ : σ_{1} \sim σ_{2}$ . Build, node by node, the coercion of kind $(σ_{1} \sim Int) \Rightarrow Tree σ_{1} \sim (σ_{2} \sim Int) \Rightarrow Tree σ_{2}$ that theorem 131.12 constructs for $φ = (a \sim Int) \Rightarrow Tree a$ , naming the rule used at each node. (Half a page; both clauses of the theorem occur.)

Referenced from 2 locations

Explicit Equality Evidence and System FC

Exercise 131.3 ¶

★★☆ Give a well-formed top-level environment containing two axioms about one type function $S^{1}$ of kind $⋆ \to ⋆$ from which a coercion of kind $Int \sim Bool$ is derivable once Right is allowed to decompose $S^{1}$ -applications. Then check that your environment still satisfies definition 131.29 when Right keeps its printed restriction.

Referenced from 2 locations

Explicit Equality Evidence and System FC

Type functions and axioms

A type function is declared without an interpretation and given one, case by case, by equality axioms. This is the second extension of System F, and it is the one that adds power beyond GADTs.

Example 131.15 — A type family and the cast it licenses ¶

Declare $type {Elem}^{1} : ⋆ \to ⋆$ and $axiom ebs : {Elem}^{1} BitSet \sim Char$ . The declaration Coerce is applicable because EqTy holds: both sides have kind $⋆$ . Now compute the type of a character used where an element of a $BitSet$ is expected. With $Γ ⊢_{e} c : Char$ , $\begin{aligned} Γ ⊢_{CO} ebs : {Elem}^{1} BitSet \sim Char & \overset{C o V a r}{=} axiom, \\ Γ ⊢_{CO} sym ebs : Char \sim {Elem}^{1} BitSet & \overset{S y m}{=} from the line above, \\ Γ ⊢_{e} c ▸ sym ebs : {Elem}^{1} BitSet & \overset{C a s t}{=} from the two lines above . \end{aligned}$ A parametric axiom quantifies on each side separately, $axiom el : (\forall e : ⋆ . {Elem}^{1} [e]) \sim (\forall e : ⋆ . e)$ , and is used at a type by CoInstT: $Γ ⊢_{CO} el @ Int : {Elem}^{1} [Int] \sim Int$ . A single quantifier over an equality, $\forall a : ⋆ . ({Elem}^{1} [a] \sim a)$ , is not a type of definition 131.1 at all: TyAll requires its body to have kind $⋆$ , and an equality kind is not $⋆$ .

Referenced from 2 locations

Explicit Equality Evidence and System FC

Exercise 131.4 ¶

★☆☆ A source declaration $newtype T = MkT (T \to T)$ is translated by a single axiom. State it, check that Coerce accepts it, and write the two casts that convert between $T$ and $T \to T$ .

Referenced from 2 locations

Explicit Equality Evidence and System FC

Regularity, and four missing side conditions

Everything proved so far used the coercion rules in the forward direction. The metatheory needs them in the backward direction as well: from $Γ ⊢_{CO} γ : κ$ one wants to know that $κ$ is a well-formed equality kind, so that the two types it relates are comparable. That property fails for the printed rules.

Proposition 131.16 — Failure of regularity for the printed decomposition rules ¶

There is an environment $Γ$ and a coercion $γ$ with $Γ ⊢_{CO} γ : σ \sim τ$ derivable from definition 131.6 for which $Γ ⊢_{k} σ \sim τ : CO$ is not derivable.

Referenced from 3 locations

Explicit Equality Evidence and System FC

Proof of Proposition 131.16 — Failure of regularity for the printed decomposition rules

Proof. Let $F : ⋆ \to ⋆$ and $G : (⋆ \to ⋆) \to ⋆$ be value type constructors and $Maybe : ⋆ \to ⋆$ . Put $Γ = F : ⋆ \to ⋆, G : (⋆ \to ⋆) \to ⋆, Maybe : ⋆ \to ⋆, Int : ⋆, g : F Int \sim G Maybe .$ The binding of $g$ is well formed: TyApp gives $Γ ⊢_{TY} F Int : ⋆$ and $Γ ⊢_{TY} G Maybe : ⋆$ , so EqTy applies with the common kind $⋆$ . By CoVar and then Left, $Γ ⊢_{CO} left g : F \sim G$ . But $Γ ⊢_{k} F \sim G : CO$ would need, by EqTy, one kind for both $F$ and $G$ ; by lemma 131.4 their kinds are $⋆ \to ⋆$ and $(⋆ \to ⋆) \to ⋆$ , which are distinct. So the conclusion of Left is not a well-formed equality kind. ◻

Nothing about consistency repairs this. Consistency is required only of the top-level environment, whereas $g$ is a coercion variable of the kind a pattern match introduces, and the calculus deliberately admits locally false equality assumptions. The same computation with EqCoerce in place of Left produces an ill-formed kind from two perfectly good coercions whose left-hand sides have different kinds.

Convention 131.17 — The audited rule set ¶

Write $F C^{r} (X)$ for the calculus of definition 131.1, definition 131.2, definition 131.3, definition 131.6, definition 131.7, definition 131.8 with four rules given extra premises and one rule given one:

Γ ⊢_{CO} γ : σ_{1} σ_{2} \sim τ_{1} τ_{2}

Γ ⊢_{TY} σ_{2} : κ_{1}

Γ ⊢_{TY} τ_{2} : κ_{1}

Γ ⊢_{CO} left γ : σ_{1} \sim τ_{1}

Left^r

Γ ⊢_{CO} γ : σ_{1} σ_{2} \sim τ_{1} τ_{2}

Γ ⊢_{TY} σ_{2} : κ_{1}

Γ ⊢_{TY} τ_{2} : κ_{1}

Γ ⊢_{CO} right γ : σ_{2} \sim τ_{2}

Right^r

Γ ⊢_{CO} γ_{1} : σ_{1} \sim τ_{1}

Γ ⊢_{CO} γ_{2} : σ_{2} \sim τ_{2}

Γ ⊢_{k} σ_{1} \sim σ_{2} : CO

Γ ⊢_{CO} γ_{1} \sim γ_{2} : (σ_{1} \sim σ_{2}) \sim (τ_{1} \sim τ_{2})

EqCoerce^r

Γ, a : κ ⊢_{CO} γ : σ \sim τ

Γ, a : κ ⊢_{TY} σ : ⋆

Γ ⊢_{k} κ : TY

a \notin fv (Γ)

Γ ⊢_{CO} \forall a : κ . γ : \forall a : κ . σ \sim \forall a : κ . τ

CoAllT^r

Γ ⊢_{CO} γ : κ_{1} \sim κ_{2}

Γ ⊢_{CO} γ^{'} : σ_{1} \sim σ_{2}

Γ ⊢_{TY} σ_{1} : ⋆

Γ ⊢_{k} κ_{1} : CO

Γ ⊢_{CO} γ \Rightarrow γ^{'} : κ_{1} \Rightarrow σ_{1} \sim κ_{2} \Rightarrow σ_{2}

CompC^r

Every other rule is unchanged. All statements from here on are about $F C^{r} (X)$ . Lemma 131.11, Theorem 131.12 were proved without using Left, Right, EqCoerce, and their uses of CoAllT and CompC discharge the extra premises from the reflexivity hypotheses, so both results hold verbatim in $F C^{r} (X)$ .

Referenced from 4 locations

Explicit Equality Evidence and System FC

Lemma 131.18 — Kinding substitution ¶

Let $a \notin fv (Γ)$ and $Γ ⊢_{TY} υ : κ^{'}$ . If $Γ, a : κ^{'}, Γ^{'} ⊢_{TY} σ : κ$ then $Γ, Γ^{'} [υ / a] ⊢_{TY} σ [υ / a] : κ [υ / a]$ , and correspondingly for $⊢_{k}$ and $⊢_{CO}$ .

Referenced from 6 locations

Explicit Equality Evidence and System FC

Proof of Lemma 131.18 — Kinding substitution

Proof. Induction on the derivation. TyVar at $a$ returns $υ$ , which has kind $κ^{'} = κ^{'} [υ / a]$ because $a \notin fv (κ^{'})$ ; TyVar at another atom is unchanged, except that its kind is substituted, and lemma 131.5 moves the judgment into the substituted environment. TyApp, TySCon and TyAll commute with substitution, the last after renaming its bound variable away from $fv (υ) \cup {a}$ . The kinding and coercion cases are identical rule by rule; CoInstT additionally uses the equality $(σ [υ / a]) [φ / b] = (σ [φ / b]) [υ / a]$ , valid because $b \notin fv (υ)$ . ◻

Theorem 131.19 — Coercion regularity ¶

Let $Γ$ be well formed, meaning that each binding $d : κ$ or $S^{n} : κ$ satisfies $Γ_{<} ⊢_{k} κ : TY$ , each binding $g : κ$ satisfies $Γ_{<} ⊢_{k} κ : CO$ and each binding $u : σ$ satisfies $Γ_{<} ⊢_{TY} σ : ⋆$ , where $Γ_{<}$ is the prefix preceding it. If $Γ ⊢_{CO} γ : κ$ in $F C^{r} (X)$ then $Γ ⊢_{k} κ : CO$ .

Referenced from 8 locations

Explicit Equality Evidence and System FC

Proof of Theorem 131.19 — Coercion regularity

Proof. Induction on the coercion derivation. CoRefl: TyVar gives $Γ ⊢_{TY} d : κ$ from the same premises, and EqTy gives $Γ ⊢_{k} d \sim d : CO$ . CoVar: the kind is the one recorded in $Γ$ , which is well formed by hypothesis and by lemma 131.5. Sym and Trans: EqTy is symmetric and transitive in the required sense, since by lemma 131.4 the shared kind is determined.

CoAllT $^{r}$ : the added premise gives $Γ, a : κ ⊢_{TY} σ : ⋆$ ; the induction hypothesis gives $Γ, a : κ ⊢_{k} σ \sim τ : CO$ , whose EqTy premise and lemma 131.4 give $Γ, a : κ ⊢_{TY} τ : ⋆$ . TyAll then kinds both $\forall a : κ . σ$ and $\forall a : κ . τ$ at $⋆$ , and EqTy concludes. CoInstT: by the induction hypothesis both quantified types have kind $⋆$ ; inverting TyAll and applying lemma 131.18 kinds $σ [υ / a]$ and $τ [υ / b]$ at $⋆$ .

Comp: the third premise gives $Γ ⊢_{TY} σ_{1} σ_{2} : κ$ ; inverting TyApp gives $Γ ⊢_{TY} σ_{1} : κ_{1} \to κ$ and $Γ ⊢_{TY} σ_{2} : κ_{1}$ . The induction hypotheses and lemma 131.4 give $τ_{1}$ the kind $κ_{1} \to κ$ and $τ_{2}$ the kind $κ_{1}$ , so TyApp kinds $τ_{1} τ_{2}$ at $κ$ . SComp: the same argument at the declared argument kinds of $S^{n}$ .

Left $^{r}$ : by the induction hypothesis $σ_{1} σ_{2}$ and $τ_{1} τ_{2}$ have one kind $κ$ . The added premises give $σ_{2}$ and $τ_{2}$ the same kind $κ_{1}$ ; inverting TyApp twice and using lemma 131.4 gives both $σ_{1}$ and $τ_{1}$ the kind $κ_{1} \to κ$ , and EqTy concludes. Right $^{r}$ : the added premises are the conclusion.

CompC $^{r}$ : the induction hypothesis on $γ$ gives $Γ ⊢_{k} κ_{1} \sim κ_{2} : CO$ , which by EqCo makes both $κ_{1}$ and $κ_{2}$ equality kinds; the added premise and the induction hypothesis on $γ^{'}$ give $σ_{1}, σ_{2}$ kind $⋆$ . TyAll then forms both $κ_{i} \Rightarrow σ_{i}$ at $⋆$ . LeftC and RightC: invert TyAll on the two sides supplied by the induction hypothesis; the first gives $Γ ⊢_{k} κ_{i} : CO$ and hence EqCo, the second gives $Γ ⊢_{TY} σ_{i} : ⋆$ and hence EqTy.

EqCoerce $^{r}$ : the added premise is the left half of the conclusion; the right half follows because $τ_{i}$ shares the kind of $σ_{i}$ by the induction hypothesis, so EqTy applies to $τ_{1}, τ_{2}$ . CastC: the induction hypothesis on $γ_{2}$ gives $Γ ⊢_{k} κ \sim κ^{'} : CO$ ; its EqCo premise gives $Γ ⊢_{k} κ^{'} : CO$ . ◻

Remark 131.20 ¶

Regularity is not decoration. Cast concludes $Γ ⊢_{e} e ▸ γ : τ$ with no kinding premise on $τ$ ; without theorem 131.19 a well-typed term could have an ill-kinded type, and the canonical-forms argument of section 131.6 — which reads the head constructor off the type of a value — would have nothing to read.

Referenced from 2 locations

Explicit Equality Evidence and System FC

Exercise 131.5 ¶

★★☆ For each of Left $^{r}$ and EqCoerce $^{r}$ , delete the added premise and exhibit a well-formed environment in which the resulting rule derives a coercion whose kind is not well formed. For CoAllT $^{r}$ , say why deleting the added premise leaves a statement that is still well formed but no longer implies regularity.

Referenced from 2 locations

Explicit Equality Evidence and System FC

Dynamics

Definition 131.21 — Values, cvalues, contexts ¶

$\begin{aligned} v & ::= Λ a : κ . e ∣ λ x : σ . e ∣ K \overset{―}{σ} \overset{―}{φ} \overset{―}{e} & plain values, \\ cv & ::= v ∣ v ▸ γ & cvalues, \\ E & ::= [] ∣ E e ∣ E φ ∣ E ▸ γ ∣ case E of \overset{―}{p \to e} & evaluation contexts, \end{aligned}$ where $K \overset{―}{σ} \overset{―}{φ} \overset{―}{e}$ is a saturated constructor application. The step relation is closed under contexts: $E ⟨ e ⟩ ⟶ E ⟨ e^{'} ⟩$ whenever $e ⟶ e^{'}$ .

Referenced from 3 locations

Explicit Equality Evidence and System FC

A cvalue is a plain value under at most one cast. A term such as $true ▸ γ$ with $Γ ⊢_{CO} γ : Bool \sim S^{1} υ$ cannot be reduced further without changing its type, so the finished forms of evaluation must include it.

Definition 131.22 — Reduction ¶

$\begin{aligned} T B e t a & (Λ a : κ . e) φ & ⟶ e [φ / a] \\ B e t a & (λ x : σ . e) e^{'} & ⟶ e [e^{'} / x] \\ L e t B e t a & let x : σ = e_{1} in e_{2} & ⟶ e_{2} [e_{1} / x] \\ C a s e R e d & case (K \overset{―}{σ} \overset{―}{φ} \overset{―}{e}) of \dots K \overset{―}{b} \overset{―}{x} \to e^{'} \dots & ⟶ e^{'} [\overset{―}{φ} / \overset{―}{b}, \overset{―}{e} / \overset{―}{x}] \\ C o m b & (v ▸ γ_{1}) ▸ γ_{2} & ⟶ v ▸ γ_{1} \circ γ_{2} \end{aligned}$ together with four rules that move a cast off the head of an elimination. With $Γ ⊢_{CO} γ : \forall a : κ . σ_{1} \sim \forall b : κ . σ_{2}$ and $Γ ⊢_{k} κ : TY$ , $T P u s h ((Λ a : κ . e) ▸ γ) φ ⟶ (Λ a : κ . e ▸ γ @ a) φ .$ With $Γ ⊢_{CO} γ : κ \Rightarrow σ \sim κ^{'} \Rightarrow σ^{'}$ , $γ_{1} = sym (leftc γ)$ and $γ_{2} = rightc γ$ , $C P u s h ((Λ a : κ . e) ▸ γ) φ ⟶ (Λ a^{'} : κ^{'} . (e [a^{'} ▸ γ_{1} / a]) ▸ γ_{2}) φ .$ With $Γ ⊢_{CO} γ : σ_{1} \to σ_{2} \sim τ_{1} \to τ_{2}$ , $γ_{1} = sym (right (left γ))$ and $γ_{2} = right γ$ , $P u s h ((λ x : σ_{1} . e) ▸ γ) e^{'} ⟶ (λ y : τ_{1} . (e [y ▸ γ_{1} / x]) ▸ γ_{2}) e^{'} .$ Finally, for $K : \forall \overset{―}{a^{n} : κ} . \forall \overset{―}{b : ι} . \overset{―}{ρ} \to T \overset{―}{a^{n}}$ and $Γ ⊢_{CO} γ : T \overset{―}{σ} \sim T \overset{―}{τ}$ , $K P u s h case ((K \overset{―}{σ} \overset{―}{φ} \overset{―}{e}) ▸ γ) of \overset{―}{p \to rhs} ⟶ case (K \overset{―}{τ} \overset{―}{φ^{'}} \overset{―}{e^{'}}) of \overset{―}{p \to rhs},$ where $γ_{i} = right (\underset{n - i}{\underset{⏟}{left \dots left}} γ)$ , $θ = \overset{―}{[γ_{i} / a_{i}]}, \overset{―}{[φ_{i} / b_{i}]}$ , $φ_{i}^{'} = φ_{i} ▸ θ (ι_{i})$ when $ι_{i}$ is an equality kind and $φ_{i}^{'} = φ_{i}$ otherwise, and $e_{i}^{'} = e_{i} ▸ θ (ρ_{i})$ .

Referenced from 3 locations

Explicit Equality Evidence and System FC

Remark 131.23 — Two completions of the printed figure ¶

The printed operational semantics has no rule for $let$ and no evaluation context that enters one, so $let x : Int = 0 in x$ is a closed well-typed term that is neither a cvalue nor reducible; the progress statement is false for the printed term grammar. LetBeta above repairs this by the call-by-name rule; its preservation case is lemma 131.25, and a reader who prefers to delete $let$ from definition 131.1 obtains the same theory. Second, TPush and CPush have the same left-hand side, because $κ \Rightarrow σ$ is notation for $\forall_: κ . σ$ . They do not overlap: TPush requires $Γ ⊢_{k} κ : CO$ to fail and CPush requires it to hold, and definition 131.2 assigns each kind exactly one sort.

Referenced from 3 locations

Explicit Equality Evidence and System FC

Example 131.24 — Running the evaluator ¶

Take the declarations of example 131.10 and evaluate $eval Int (Zero Int Int)$ . The second $Int$ is the coercion argument: by CoRefl it has kind $Int \sim Int$ , which is what $Zero$ ’s second quantifier demands after instantiating $a$ by $Int$ . $\begin{aligned} eval Int (Zero Int Int) & \overset{T B e t a}{⟶} (λ e : Exp Int . case e of \dots) (Zero Int Int) \\ \overset{B e t a}{⟶} case (Zero Int Int) of \dots \\ \overset{C a s e R e d}{⟶} 0 ▸ sym Int . \end{aligned}$ The result is a cvalue, not a plain value, and its type is $Int$ : the substitution replaced the pattern variable $c o$ by the reflexivity coercion $Int$ . Theorem 131.35 shows that the erasure of the whole computation is the two-step reduction of $eval () Zero$ to $0$ .

Referenced from 2 locations

Explicit Equality Evidence and System FC

Lemma 131.25 — Term substitution ¶

If $Γ, x : σ, Γ^{'} ⊢_{e} e : τ$ and $Γ ⊢_{e} e^{'} : σ$ then $Γ, Γ^{'} ⊢_{e} e [e^{'} / x] : τ$ .

Referenced from 6 locations

Explicit Equality Evidence and System FC

Proof of Lemma 131.25 — Term substitution

Proof. Induction on the typing derivation. Var at $x$ returns $e^{'}$ , whose typing is the hypothesis after lemma 131.5; Var at another subject is unchanged. Abs, AbsT, Let and Alt rename their bound subject away from $fv (e^{'}) \cup {x}$ and apply the induction hypothesis to the body. App, AppT, Cast and Case apply it to each premise; no type or coercion changes, because $x$ is a term variable. ◻

Lemma 131.26 — Type and coercion substitution in terms ¶

Let $a \notin fv (Γ)$ , $Γ ⊢_{δ} φ : κ$ , and $Γ, a : κ, Γ^{'} ⊢_{e} e : σ$ . Then $Γ, Γ^{'} [φ / a] ⊢_{e} e [φ / a] : σ [φ / a]$ .

Referenced from 5 locations

Explicit Equality Evidence and System FC

Proof of Lemma 131.26 — Type and coercion substitution in terms

Proof. Induction on the typing derivation, using lemma 131.18 at every kinding and coercion premise. The only case that is not a direct rewriting is Cast: its coercion premise $Γ, a : κ, Γ^{'} ⊢_{CO} γ : σ \sim τ$ becomes $Γ, Γ^{'} [φ / a] ⊢_{CO} γ [φ / a] : σ [φ / a] \sim τ [φ / a]$ by the coercion clause of lemma 131.18, which is the premise Cast needs at the substituted types. ◻

Theorem 131.27 — Preservation ¶

Let $Γ$ be a well-formed top-level environment, $Γ ⊢_{e} e : σ$ and $e ⟶ e^{'}$ . Then $Γ ⊢_{e} e^{'} : σ$ .

Referenced from 6 locations

Explicit Equality Evidence and System FC

Proof of Theorem 131.27 — Preservation

Proof. It suffices to treat the eight contraction rules, since each evaluation context of definition 131.21 is an elimination whose typing rule uses the type of the hole as a premise, so replacing the hole by a term of the same type reuses the same derivation.

TBeta. Inverting AppT and AbsT gives $Γ, a : κ ⊢_{e} e : σ_{0}$ with $σ = σ_{0} [φ / a]$ and $Γ ⊢_{δ} φ : κ$ ; lemma 131.26 concludes.

Beta and LetBeta. Invert App together with Abs, respectively Let, and apply lemma 131.25.

CaseRed. Inverting Case gives $Γ ⊢_{e} K \overset{―}{σ} \overset{―}{φ} \overset{―}{e} : T \overset{―}{υ}$ and, for the selected alternative, $Γ ⊢_{p} K \overset{―}{b : θ (ι)} \overset{―}{x : θ (σ)} \to e^{'} : T \overset{―}{υ} \to σ$ with $θ = \overset{―}{[υ / a]}$ . Inverting the constructor application through Var, AppT and App shows $\overset{―}{σ} = \overset{―}{υ}$ , that each $φ_{i}$ has kind $θ (ι_{i})$ , and that each $e_{i}$ has type $θ (σ_{i})$ further instantiated by $\overset{―}{[φ / b]}$ . Applying lemma 131.26 once per $b_{i}$ and lemma 131.25 once per $x_{i}$ gives the substituted right-hand side the type $σ$ .

Comb. Inverting Cast twice gives $Γ ⊢_{CO} γ_{1} : σ_{v} \sim τ_{1}$ and $Γ ⊢_{CO} γ_{2} : τ_{1} \sim σ$ ; Trans composes them and Cast reapplies.

TPush. Here $Γ ⊢_{CO} γ : \forall a : κ . σ_{1} \sim \forall b : κ . σ_{2}$ and $Γ, a : κ ⊢_{e} e : σ_{1}$ . Under $a : κ$ , TyVar gives $Γ, a : κ ⊢_{TY} a : κ$ , so CoInstT gives $Γ, a : κ ⊢_{CO} γ @ a : σ_{1} \sim σ_{2} [a / b]$ — the left side is $σ_{1} [a / a] = σ_{1}$ . Then Cast types $e ▸ γ @ a$ at $σ_{2} [a / b]$ and AbsT gives $\forall a : κ . σ_{2} [a / b]$ , which is $\forall b : κ . σ_{2}$ up to renaming. The enclosing AppT premise is unchanged.

CPush. Here $κ$ is an equality kind, $Γ, a : κ ⊢_{e} e : σ$ with $a \notin fv (σ)$ , and $Γ ⊢_{CO} γ : κ \Rightarrow σ \sim κ^{'} \Rightarrow σ^{'}$ . LeftC and Sym give $Γ ⊢_{CO} γ_{1} : κ^{'} \sim κ$ and RightC gives $Γ ⊢_{CO} γ_{2} : σ \sim σ^{'}$ . Under $a^{'} : κ^{'}$ , CoVar gives $Γ, a^{'} : κ^{'} ⊢_{CO} a^{'} : κ^{'}$ and CastC gives $Γ, a^{'} : κ^{'} ⊢_{CO} a^{'} ▸ γ_{1} : κ$ . Lemma 131.26 with $δ = CO$ types $e [a^{'} ▸ γ_{1} / a]$ at $σ$ , Cast moves it to $σ^{'}$ , and AbsT gives $κ^{'} \Rightarrow σ^{'}$ .

Push. Writing $σ_{1} \to σ_{2}$ as $(\to) σ_{1} σ_{2}$ , the premises of Left $^{r}$ and Right $^{r}$ are discharged by theorem 131.19 applied to $γ$ , so $γ_{1}$ has kind $τ_{1} \sim σ_{1}$ and $γ_{2}$ has kind $σ_{2} \sim τ_{2}$ . Then $y : τ_{1}$ gives $y ▸ γ_{1} : σ_{1}$ by Cast, lemma 131.25 types the substituted body at $σ_{2}$ , a second Cast moves it to $τ_{2}$ , and Abs gives $τ_{1} \to τ_{2}$ .

KPush. Let $K : \forall \overset{―}{a^{n} : κ} . \forall \overset{―}{b : ι} . \overset{―}{ρ} \to T \overset{―}{a^{n}}$ . Repeated Left $^{r}$ and one Right $^{r}$ give $Γ ⊢_{CO} γ_{i} : σ_{i} \sim τ_{i}$ , their side premises again supplied by theorem 131.19. Theorem 131.12, clause 1 for each $ρ_{i}$ and clause 2 for each equality kind $ι_{i}$ , gives $θ (ρ_{i})$ the kind $\overset{―}{[σ / a]} ρ_{i} \sim \overset{―}{[τ / a]} ρ_{i}$ and $θ (ι_{i})$ the kind $\overset{―}{[σ / a]} ι_{i} \sim \overset{―}{[τ / a]} ι_{i}$ . Hence Cast types each $e_{i}^{'}$ and CastC kinds each $φ_{i}^{'}$ at the arguments required by $K$ instantiated at $\overset{―}{τ}$ , so the reduct is a constructor application of type $T \overset{―}{τ}$ . The scrutinee’s type changed from $T \overset{―}{σ}$ cast to $T \overset{―}{τ}$ into $T \overset{―}{τ}$ directly, and the alternatives were already typed against $T \overset{―}{τ}$ by Case. ◻

Consistency, canonical forms and progress

Definition 131.28 — Value type ¶

A type $υ$ is a value type when it has the form $\forall a : κ . υ^{'}$ or $T \overset{―}{υ^{'}}$ .

Referenced from 3 locations

Explicit Equality Evidence and System FC

Definition 131.29 — Consistency ¶

A top-level environment $Γ$ is consistent when

if $Γ ⊢_{CO} γ : T \overset{―}{σ} \sim υ$ and $υ$ is a value type, then $υ = T \overset{―}{τ}$ for some $\overset{―}{τ}$ ; and
if $Γ ⊢_{CO} γ : \forall a : κ . σ \sim υ$ and $υ$ is a value type, then $υ = \forall a : κ . τ$ for some $τ$ .

Referenced from 8 locations

Explicit Equality Evidence and System FC

Consistency is undecidable in general; the parameter $X$ of $F C (X)$ is a decision procedure for it, chosen with the source construct being compiled. Theorem 131.41 discharges it outright for GADT programs.

Lemma 131.30 — Canonical forms ¶

Let $Γ$ be a consistent top-level environment and let $Γ ⊢_{e} cv : σ$ with $cv$ a cvalue.

If $σ = σ_{1} \to σ_{2}$ then $cv$ is $λ x : σ_{1} . e$ or $(λ x : τ_{1} . e) ▸ γ$ .
If $σ = \forall a : κ . σ_{0}$ then $cv$ is $Λ a : κ . e$ or $(Λ a : κ^{'} . e) ▸ γ$ .
If $σ = T \overset{―}{υ}$ then $cv$ is $K \overset{―}{σ^{'}} \overset{―}{φ} \overset{―}{e}$ or $(K \overset{―}{σ^{'}} \overset{―}{φ} \overset{―}{e}) ▸ γ$ with $K$ a constructor of $T$ .

Referenced from 4 locations

Explicit Equality Evidence and System FC

Proof of Lemma 131.30 — Canonical forms

Proof. A plain value is typed by Abs, AbsT or a saturated chain of Var, AppT and App at a constructor; the three cases give types $(\to) σ_{x} σ$ , $\forall a : κ . σ$ and $T \overset{―}{υ}$ . Each is a value type, and its head determines the shape of the value, because $Γ$ binds no term variable.

For $cv = v ▸ γ$ , inverting Cast gives $Γ ⊢_{e} v : τ$ and $Γ ⊢_{CO} γ : τ \sim σ$ with $τ$ one of the three value types just listed. Sym gives $Γ ⊢_{CO} sym γ : σ \sim τ$ . In case 1, $σ = (\to) σ_{1} σ_{2}$ is of the form $T \overset{―}{σ}$ with $T = (\to)$ ; clause 1 of definition 131.29 applied to $sym γ$ and the value type $τ$ gives $τ = (\to) τ_{1} τ_{2}$ , so $v$ is a lambda abstraction. Case 3 is the same argument with $T$ in place of $(\to)$ . In case 2, clause 2 gives $τ = \forall a : κ . τ_{0}$ , so $v$ is a type abstraction; and its binder kind is $κ$ because $\forall a : κ . τ_{0}$ and $\forall a : κ . σ_{0}$ are related, whose kinds TyAll records. ◻

Theorem 131.31 — Progress and subject reduction ¶

Let $Γ$ be a consistent well-formed top-level environment in which every $case$ of the term has one alternative for each constructor of the scrutinee’s type constructor, and let $Γ ⊢_{e} e : σ$ . Then either $e$ is a cvalue, or there is $e^{'}$ with $e ⟶ e^{'}$ and $Γ ⊢_{e} e^{'} : σ$ .

Referenced from 9 locations

Explicit Equality Evidence and System FC

Proof of Theorem 131.31 — Progress and subject reduction

Proof. Preservation is theorem 131.27, so only the disjunction must be proved; induct on the typing derivation. Var cannot occur, since $Γ$ binds no term variable and a bare constructor is not saturated unless it takes no arguments, in which case it is a plain value. Abs and AbsT give plain values. Let gives an LetBeta redex.

App with $Γ ⊢_{e} e_{1} e_{2} : σ_{1}$ and $Γ ⊢_{e} e_{1} : σ_{2} \to σ_{1}$ . By the induction hypothesis either $e_{1}$ steps, in which case the context $E e_{2}$ lifts the step; or $e_{1}$ is a cvalue. By lemma 131.30 clause 1 it is then $λ x . e_{3}$ , giving a Beta redex, or $(λ x . e_{3}) ▸ γ$ , giving a Push redex.

AppT with $Γ ⊢_{e} e φ : σ_{0} [φ / a]$ . Either $e$ steps under $E φ$ , or by clause 2 it is $Λ a : κ . e_{0}$ , giving TBeta, or $(Λ a : κ^{'} . e_{0}) ▸ γ$ . In the last case definition 131.2 assigns $κ^{'}$ exactly one sort, which selects TPush or CPush; the side conditions of the selected rule are the kinding facts supplied by theorem 131.19 applied to $γ$ .

Case with scrutinee $e_{0}$ of type $T \overset{―}{υ}$ . Either $e_{0}$ steps under the context $case E of \overset{―}{p \to e}$ , or by clause 3 it is $K \overset{―}{σ} \overset{―}{φ} \overset{―}{e}$ , giving CaseRed because the alternatives are exhaustive for $T$ , or it is that application under a cast, giving KPush.

Cast with $Γ ⊢_{e} e_{0} ▸ γ : τ$ . Either $e_{0}$ steps under $E ▸ γ$ ; or $e_{0}$ is a plain value, and then $e_{0} ▸ γ$ is already a cvalue; or $e_{0}$ is $v ▸ γ^{'}$ , giving a Comb redex. ◻

Corollary 131.32 — Syntactic soundness ¶

Under the hypotheses of theorem 131.31, either $e ⟶^{*} cv$ with $Γ ⊢_{e} cv : σ$ for some cvalue $cv$ , or the reduction from $e$ is infinite.

Referenced from 2 locations

Explicit Equality Evidence and System FC

Proof of Corollary 131.32 — Syntactic soundness

Proof. Iterate theorem 131.31. Each step preserves the type and the hypotheses, so no finite reduction sequence ends at a non-cvalue. ◻

Remark 131.33 — Local assumptions may be inconsistent ¶

The term $f = λ g : (Int \sim Bool) . 1 + true ▸ g$ is well typed in a consistent top-level environment: the false equality is a hypothesis of $f$ , not an axiom. Theorem 131.31 is not violated, because to reduce a call of $f$ one must first supply a closed coercion of kind $Int \sim Bool$ , and consistency of the top-level environment says that none exists.

Referenced from 2 locations

Explicit Equality Evidence and System FC

Erasure

Definition 131.34 — Erasure ¶

$\begin{aligned} x^{\circ} & = x, & K^{\circ} & = K, & (λ x : φ . e)^{\circ} & = λ x . e^{\circ}, \\ (Λ a : κ . e)^{\circ} & = λ a . e^{\circ}, & (e σ)^{\circ} & = e^{\circ} (), & (e_{1} e_{2})^{\circ} & = e_{1}^{\circ} e_{2}^{\circ}, \\ (e ▸ γ)^{\circ} & = e^{\circ}, & (K \overset{―}{a : κ} \overset{―}{x : φ})^{\circ} & = K \overset{―}{a} \overset{―}{x}, \end{aligned}$ extended homomorphically to $let$ and $case$ . Type abstraction erases to abstraction over a unit argument, and type application to application to $()$ , so that the number of reduction steps of a call-by-value target is not changed by erasure.

Referenced from 3 locations

Explicit Equality Evidence and System FC

Theorem 131.35 — Erasure ¶

Let $Γ$ be a consistent well-formed top-level environment and $Γ ⊢_{e} e_{1} : σ$ .

If $e_{1}$ is a cvalue then $e_{1}^{\circ}$ is a value.
If $e_{1} ⟶ e_{2}$ then $e_{1}^{\circ} ⟶ e_{2}^{\circ}$ or $e_{1}^{\circ} = e_{2}^{\circ}$ .

Referenced from 10 locations

Proof of Theorem 131.35 — Erasure

Proof. Clause 1 is immediate: erasure deletes the outer cast of $v ▸ γ$ and maps the three plain-value forms to abstractions and saturated constructor applications.

Clause 2 is by cases on the contraction rule, and the only work is to see which rules disappear. Beta, LetBeta and CaseRed erase to the corresponding untyped steps, using $(e [e^{'} / x])^{\circ} = e^{\circ} [e^{' \circ} / x]$ , which holds by induction on $e$ because erasure is compositional and does not bind. TBeta erases to a beta step at the unit argument, using $(e [φ / a])^{\circ} = e^{\circ} [() / a]$ . Comb, TPush, CPush, Push and KPush all erase to an equality. For Comb and TPush both sides erase to $v^{\circ}$ and $(λ a . e^{\circ}) ()$ . For CPush and Push, the reduct’s binder is renamed and its body is $e [y ▸ γ_{1} / x]$ , whose erasure is $e^{\circ} [y / x]$ ; both sides therefore erase to the same term up to renaming of the bound variable. For KPush the arguments change only by casts, so both sides erase to $case (K \overset{―}{a} \overset{―}{e^{\circ}}) of \dots$ . Closure under evaluation contexts follows because $E ⟨ e ⟩^{\circ} = E^{\circ} ⟨ e^{\circ} ⟩$ for the erased contexts, where $(E ▸ γ)^{\circ} = E^{\circ}$ . ◻

Corollary 131.36 — Erasure soundness ¶

For well-typed $e_{1}$ in a consistent well-formed top-level environment, $e_{1} ⟶^{*} e_{2}$ implies $e_{1}^{\circ} ⟶^{*} e_{2}^{\circ}$ , and $e_{1}$ reduces to a cvalue if and only if $e_{1}^{\circ}$ reduces to a value.

Referenced from 3 locations

Explicit Equality Evidence and System FC

Proof of Corollary 131.36 — Erasure soundness

Proof. The forward direction iterates theorem 131.35. For the converse, note that every step of the erased term is the erasure of a step of the typed term: by theorem 131.31 a well-typed non-cvalue steps, and by theorem 131.35 its erasure either steps correspondingly or is unchanged; the unchanged cases Comb, TPush, CPush, Push and KPush strictly decrease the number of casts standing on the head of an elimination, so only finitely many of them occur consecutively. ◻

The practical content of corollary 131.36 is that equality evidence costs nothing at run time. It also explains why coercions are types rather than terms: a coercion is guaranteed to be a proof by being well kinded, whereas a term of an equality type would first have to be evaluated to check that it is not divergent.

Exercise 131.6 ¶

★★☆ Compute both sides of one KPush step for $Cons : \forall a : ⋆ . a \to [a] \to [a]$ and $Γ ⊢_{CO} γ : [Int] \sim [τ]$ , then erase both. State which clause of theorem 131.12 produces the coercion that casts the tail.

Referenced from 2 locations

Explicit Equality Evidence and System FC

Elaborating the GADT source fragment

The source language is Hindley–Milner with constrained constructor signatures: $π ::= η ∣ \forall a . π, η ::= τ ∣ (τ \sim τ) \Rightarrow η, τ ::= a ∣ τ \to τ ∣ T \overset{―}{τ},$ and $C ::= ϵ ∣ C, c o : τ_{1} \sim τ_{2}$ is a set of named equality assumptions. The judgment $C; Γ ⊢_{G} e : π ⇝ e^{'}$ reads: under the assumptions $C$ and environment $Γ$ , the source expression $e$ has type $π$ and elaborates to the $F C^{r}$ term $e^{'}$ .

Definition 131.37 — Elaboration ¶

x : π \in Γ

C; Γ ⊢_{G} x : π ⇝ x

G-Var

C; Γ ⊢_{G} e : τ ⇝ e^{'}

C ⊢_{CO} γ : τ \sim τ^{'}

C; Γ ⊢_{G} e : τ^{'} ⇝ e^{'} ▸ γ

G-Eq

C; Γ ⊢_{G} e : π ⇝ e^{'}

a \notin fv (C, Γ)

C; Γ ⊢_{G} e : \forall a . π ⇝ Λ a : ⋆ . e^{'}

G-Gen

C; Γ ⊢_{G} e : \forall a . π ⇝ e^{'}

C; Γ ⊢_{G} e : π [τ / a] ⇝ e^{'} τ

G-Inst

C, c o : τ_{1} \sim τ_{2}; Γ ⊢_{G} e : η ⇝ e^{'}

C; Γ ⊢_{G} e : (τ_{1} \sim τ_{2}) \Rightarrow η ⇝ Λ c o : (τ_{1} \sim τ_{2}) . e^{'}

G-CIntro

C; Γ ⊢_{G} e : (τ_{1} \sim τ_{2}) \Rightarrow η ⇝ e^{'}

C ⊢_{CO} γ : τ_{1} \sim τ_{2}

C; Γ ⊢_{G} e : η ⇝ e^{'} γ

G-CElim

For a pattern alternative, with $K :: \forall \overset{―}{a}, \overset{―}{b} . (τ^{'} \sim τ^{″}) \Rightarrow \overset{―}{τ} \to T \overset{―}{a}$ , $\overset{―}{a} \cap \overset{―}{b} = \emptyset$ , $fv (\overset{―}{τ}, τ^{'}, τ^{″}) = fv (\overset{―}{a}, \overset{―}{b})$ , $θ = \overset{―}{[υ / a]}$ and fresh $\overset{―}{c o}$ ,

C, \overset{―}{c o : θ (τ^{'}) \sim θ (τ^{″})}; Γ, \overset{―}{x : θ (τ)} ⊢_{G} e : τ_{r} ⇝ e^{'}

C; Γ ⊢_{G} K \overset{―}{x} \to e : T \overset{―}{υ} \to τ_{r} ⇝ K \overset{―}{b : ⋆} \overset{―}{c o : θ (τ^{'}) \sim θ (τ^{″})} \overset{―}{x : θ (τ)} \to e^{'}

G-Alt

Referenced from 4 locations

Explicit Equality Evidence and System FC

The coercion $γ$ in G-Eq and G-CElim is an output, not an input: the elaborator must construct a proof of $τ_{1} \sim τ_{2}$ from the named assumptions $C$ . That search is decidable, and the algorithm is first-order unification with evidence.

Construction 131.38 — Finding the coercion ¶

Given $C$ and a goal $τ_{1} \sim τ_{2}$ :

normalize $C$ to a solved form $\overset{―}{γ : a \sim υ}$ with the $a$ pairwise distinct, ordered, and disjoint from $fv (\overset{―}{υ})$ , by decomposing each assumption with Right $^{r}$ and orienting it with Sym and Trans;
normalize the fresh assumption $c o^{'} : τ_{1} \sim τ_{2}$ the same way, obtaining $\overset{―}{γ^{'} : a^{'} \sim υ^{'}}$ ;
match each equation of step 2 against an equation of step 1;
reverse the normalization of step 2 to obtain $γ$ .

Failure at any step means that no $γ$ exists.

Referenced from 2 locations

Explicit Equality Evidence and System FC

Example 131.39 ¶

Let $C = {c_{1} : [a] \sim [b], c_{2} : b \sim c}$ with $a < b < c$ , and let the goal be $[a] \sim [c]$ . Step 1 decomposes $c_{1}$ to $right c_{1} : a \sim b$ and composes it with $c_{2}$ , giving the solved form ${(right c_{1}) \circ c_{2} : a \sim c, c_{2} : b \sim c}$ . Step 2 normalizes the goal to $right c_{3} : a \sim c$ . Step 3 matches the two. Step 4 reverses the decomposition: since $Γ ⊢_{CO} [] : [] \sim []$ by CoRefl, the coercion is $γ = [] ((right c_{1}) \circ c_{2})$ , an instance of Comp whose kind is $[a] \sim [c]$ .

Referenced from 2 locations

Explicit Equality Evidence and System FC

Lemma 131.40 — Elaboration is type preserving ¶

If $C; ϵ ⊢_{G} e : τ ⇝ e^{'}$ then $C ⊢_{e} e^{'} : τ$ , where $C$ is read as an $F C^{r}$ environment of coercion variables.

Referenced from 2 locations

Explicit Equality Evidence and System FC

Proof of Lemma 131.40 — Elaboration is type preserving

Proof. Induction on the elaboration derivation. G-Var matches Var. G-Gen and G-Inst match AbsT and AppT with $δ = TY$ and $κ = ⋆$ ; the freshness side condition of G-Gen is the side condition of AbsT. G-CIntro and G-CElim match the same two rules with $δ = CO$ , the second using its coercion premise as the third premise of AppT. G-Eq matches Cast directly. G-Alt matches Alt: the source constructor signature is already an $F C^{r}$ type, its equality constraints becoming coercion binders $\overset{―}{b : ι}$ with $ι$ an equality kind, and the pattern binds exactly those binders. ◻

Theorem 131.41 — GADT consistency ¶

Let $Γ$ be an environment whose domain contains no type variable and no coercion constant. If $Γ ⊢_{CO} γ : σ_{1} \sim σ_{2}$ then $σ_{1} = σ_{2}$ . Consequently every environment produced by definition 131.37 from a GADT program is consistent.

Referenced from 5 locations

Explicit Equality Evidence and System FC

Proof of Theorem 131.41 — GADT consistency

Proof. Induction on the derivation of the coercion judgment. The two leaf rules are CoRefl, whose conclusion has $σ_{1} = σ_{2} = d$ , and CoVar, which is unavailable: a coercion variable $c o$ is a type variable and a coercion constant $C$ is a coercion constant, and the hypothesis excludes both from $dom (Γ)$ .

Every other rule builds its conclusion from premises about coercions in the same $Γ$ . Sym and Trans preserve the identity of the two sides. CoAllT $^{r}$ : the induction hypothesis in $Γ, a : κ$ does not apply directly, because that environment does contain a type variable; but $a$ is bound with a type kind, so CoVar still cannot fire at $a$ — it requires an equality kind — and the induction goes through with the strengthened hypothesis “ $Γ$ contains no coercion constant and no variable of equality kind”. Under that hypothesis Comp, SComp, CompC $^{r}$ and EqCoerce $^{r}$ give $σ_{1} = σ_{2}$ componentwise; Left $^{r}$ , Right $^{r}$ , LeftC and RightC give it by taking the corresponding component of an identity; CoInstT substitutes the same $υ$ on both sides of an identity; and CastC rewrites a kind by an identity and so changes nothing. Since elaboration introduces coercion variables only at pattern binders, and introduces no axiom, the resulting top-level environment satisfies the hypothesis, and definition 131.29 follows: a coercion between two value types forces them to be equal, so in particular their heads agree. ◻

Exercise 131.7 ¶

★★☆ Elaborate the source evaluator of example 131.10 using definition 131.37, and check every generated coercion against definition 131.6. Then say which elaboration rule introduces the coercion $sym c o$ and which source subterm forces it.

Referenced from 2 locations

Explicit Equality Evidence and System FC

Explicit convertibility in pure type systems

A pure type system with explicit convertibility proofs, written $λ^{f} S$ , also stores in the term the reason two types were identified; the system $λ^{f} S$ of van Doorn, Geuvers and Wiedijk (2013) is the reference point here, and its rules are that paper’s Figure 4.1. Its conversion rule is $\frac{\begin{matrix} Γ ⊢_{f} a : A \\ Γ ⊢_{f} A^{'} : s \\ Γ ⊢_{f} H : A = A^{'} \end{matrix}}{Γ ⊢_{f} a^{H} : A^{'}} f - Conv,$ and the erasure $| \cdot |$ deleting every $H$ satisfies: if $Γ ⊢_{f} A : B$ then $| Γ | ⊢ | A | : | B |$ , and $λ S$ and $λ^{f} S$ are equivalent frameworks. The resemblance to Cast is real but shallow, and the exact differences matter for what can be transferred.

	$F C^{r} (X)$	$λ^{f} S$
What evidence proves	interchangeability of two types of one kind	convertibility of two terms, types included
Sort of evidence	a type, of kind $σ_{1} \sim σ_{2}$	a proof term $H$ of a separate judgment $Γ ⊢_{f} H : A = A^{'}$
Source of the equations	top-level axioms, restricted by definition 131.29	the fixed $β$ -rule, closed under congruence
Evidence in the type language	yes; coercions are erased with types	no; $H$ is a term-level annotation
Decidability	type checking is syntax-directed and decidable; consistency is the parameter $X$	type checking is linear in the size of the term; every judgment has one derivation
Erasure theorem	theorem 131.35: run-time behaviour is unchanged	$λ^{f} S \Rightarrow λ S$ : typability is preserved

The table also records what is not shared. In $λ^{f} S$ the equations are generated by one fixed reduction relation and are therefore consistent by confluence; in $F C^{r} (X)$ they are supplied by the program and consistency is an assumption that a decision procedure must discharge. Conversely $λ^{f} S$ equates terms of dependent types, which $F C^{r} (X)$ has no means to express, since its equality kinds relate types only. Neither erasure theorem implies the other.

Limits and seminar

The frozen source is the 2007 System $F C (X)$ of Sulzmann, Chakravarty, Peyton Jones and Donnelly; the calculus proved about here is the audited system $F C^{r} (X)$ of convention 131.17, which adds five side conditions to the coercion rules, corrects the scope of Data (remark 131.9) and completes the reduction relation with LetBeta (remark 131.23). Proposition 131.16 shows that the additions are not cosmetic. Theorem 131.19, Theorem 131.27, Theorem 131.31, Theorem 131.35, Theorem 131.41 are local theorems about $F C^{r} (X)$ ; the published proofs supply the architecture of the argument and the statements of definition 131.28, definition 131.29, and are cited as comparisons, not as exact-signature imports.

Four boundaries are worth stating plainly. Consistency of a top-level environment is undecidable, so no theorem here provides a procedure; the chapter proves consistency outright only for the GADT fragment (theorem 131.41), where no axiom is generated. Nothing here is a theorem about type-family termination, overlap or confluence: an axiom set generated from associated types must be checked non-overlapping by whatever procedure plays the role of $X$ . Nothing here bounds the size of coercions; the push rules make them grow, and the simplifications $sym σ = σ$ and $e ▸ σ = e$ for a reflexivity witness $σ$ are optional compiler transformations, not part of the calculus. Finally, the later role and equality machinery of production compilers is a different system with different theorems, and the elaboration of section 131.8 covers the GADT fragment only; associated types add the class-predicate rules that were not developed here.

[4]

Suggested first pass.

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

Exercise 131.8 ¶

★★☆ Exhibit a two-axiom top-level environment that is inconsistent by clause 1 of definition 131.29, and a closed well-typed term that reduces, using that environment, to a stuck non-cvalue. Identify the exact step of the proof of theorem 131.31 that fails, and the clause of lemma 131.30 it depended on.

Referenced from 3 locations

Explicit Equality Evidence and System FC

Exercise 131.9 ¶

★★☆ In a program where $x : T a$ and $y : a$ and matching $x$ against a constructor refines $a$ to $Int$ , a compiler proposes to float $let z = y + 1$ out of the enclosing abstraction. Write the source and the floated form in $F C^{r} (X)$ , show which typing premise the floated form lacks, and give the repaired transformation that abstracts the binding over the coercion bound by the match.

Referenced from 2 locations

Explicit Equality Evidence and System FC

Exercise 131.10 ¶

★★★ Take $e = Λ c o : (σ_{1} \sim Int) . λ x : σ_{1} . x ▸ c o$ and a coercion $γ^{'}$ of kind $((σ_{1} \sim Int) \Rightarrow σ_{1} \to Int) \sim ((σ_{2} \sim Int) \Rightarrow σ_{2} \to Int)$ . Reduce $(e ▸ γ^{'}) γ^{″}$ by CPush, giving the kind of every coercion that appears, and then verify the reduct’s type by the argument of theorem 131.27. Finally erase both sides and check theorem 131.35 clause 2 on this instance.

Referenced from 2 locations

Explicit Equality Evidence and System FC

Exercise 131.11 — Practical: coercion kinder and eraser ¶

★★★ Practical project.fc-coercion-kinder Complete project fc-coercion-kinder. Implement, for the finite signature of example 131.10 extended by one type function and one axiom, (i) kind well-formedness and type kinding, (ii) the coercion kinder of definition 131.6 under convention 131.17, (iii) the cast rule Cast, (iv) the reduction of definition 131.22 restricted to the rules TBeta, Beta, CaseRed and Comb, and (v) the erasure of definition 131.34. The invariant the implementation must maintain is that the kinder returns an equality kind only when both sides are assigned one common kind by the type kinder — that is, theorem 131.19 as a run-time check. The named cases print

lift-tree: Tree(a) ~ Tree(b)
decompose-typefun: rejected
left-mixed-kind: rejected
gadt-zero: 0
bogus-axiom: inconsistent

The checker is independent evidence for the finite signature; it does not prove theorem 131.27, theorem 131.31 and does not decide consistency for an arbitrary axiom set.

Referenced from 3 locations