Chapter 164Core route

Dependent Parametricity

Let $g$ be a closed term of type $\prod_{A : U} A \to A$ . Nothing in the typing rules forbids $g$ from behaving differently at different instances: the rules say that $g A$ has type $A \to A$ for every $A$ , and they say nothing about the relation between $g 2$ and $g N$ . Consider the informal specification $g A x : = {\begin{cases} tt & if A is 2, \\ x & otherwise, \end{cases}$ which is well typed at every instance considered separately. It is not a term of the calculus, because there is no elimination form for $U$ that could decide the case split. But that is a statement about which terms exist, and it is proved by inspecting the syntax; what we want is a statement about what every term does, proved once for all terms.

Reynolds’ answer is to interpret a type not as a set of values but as a relation, and to prove that every term is related to itself. In a dependent theory that answer needs revision twice over. The relation for $\prod_{x : A} B$ must relate $f_{1}$ and $f_{2}$ at arguments $x_{1}$ and $x_{2}$ that are themselves only related, and the codomain $B$ is then instantiated at two different arguments, so the relation for $B$ must be allowed to depend on a proof that $x_{1}$ and $x_{2}$ are related. And types are terms, so the relational interpretation must itself be a term of the theory.

The simply typed case, and one free theorem

We begin where the difficulty is absent. Fix a finite set of type variables $Θ = α_{1}, \dots, α_{k}$ and let types be generated by $σ, τ ::= α_{i} ∣ σ \to τ .$ A relation environment $ϱ$ assigns to each $α_{i}$ a triple $(X_{i}, Y_{i}, R_{i})$ of two sets and a relation $R_{i} \subseteq X_{i} \times Y_{i}$ .

Definition 164.1 — Relational interpretation of simple types ¶

For a type $τ$ over $Θ$ and a relation environment $ϱ$ define a relation $R_{τ} [ϱ]$ between the two sets $A_{1} (τ)$ and $A_{2} (τ)$ given by $A_{1} (α_{i}) : = X_{i}$ , $A_{2} (α_{i}) : = Y_{i}$ , and $A_{j} (σ \to τ) : =$ the set of functions $A_{j} (σ) ⟶ A_{j} (τ)$ . A term $\vec{x} : \vec{σ} ⊢ e : τ$ denotes, in the copy $j$ , a function $A_{j} (e)$ from tuples in $A_{j} (σ_{1}) \times \dots$ to $A_{j} (τ)$ , by the usual clauses for variables, abstraction and application. Set $\begin{aligned} R_{α_{i}} [ϱ] & : = R_{i}, \\ R_{σ \to τ} [ϱ] & : = {(f_{1}, f_{2}) | \forall (a_{1}, a_{2}) \in R_{σ} [ϱ] . (f_{1} a_{1}, f_{2} a_{2}) \in R_{τ} [ϱ]} . \end{aligned}$

Referenced from 5 locations

Dependent Parametricity

Proposition 164.2 — Abstraction for simple types ¶

Let $x_{1} : σ_{1}, \dots, x_{m} : σ_{m} ⊢ e : τ$ over $Θ$ and let $ϱ$ be a relation environment. If $(a_{j}, b_{j}) \in R_{σ_{j}} [ϱ]$ for every $j$ , then $(A_{1} (e) (\vec{a}), A_{2} (e) (\vec{b})) \in R_{τ} [ϱ]$ .

Referenced from 2 locations

Dependent Parametricity

Proof of Proposition 164.2 — Abstraction for simple types

Proof. By induction on the derivation. Variable case. $A_{1} (x_{j}) (\vec{a}) = a_{j}$ and $A_{2} (x_{j}) (\vec{b}) = b_{j}$ , and the pair is related by hypothesis. Abstraction case. Let $e = λ y . e_{0}$ with $y : σ_{0}$ . To show the pair of functions is in $R_{σ_{0} \to τ_{0}} [ϱ]$ , take $(c_{1}, c_{2}) \in R_{σ_{0}} [ϱ]$ ; the induction hypothesis for $e_{0}$ with the extended environments gives $(A_{1} (e_{0}) (\vec{a}, c_{1}), A_{2} (e_{0}) (\vec{b}, c_{2})) \in R_{τ_{0}} [ϱ]$ , which is the required condition by definition 164.1. Application case. As in the abstraction case with the two quantifiers exchanged: the induction hypothesis for the operator gives membership in $R_{σ_{0} \to τ} [ϱ]$ , and the induction hypothesis for the operand supplies the pair at which that membership is instantiated. ◻

Now add one quantifier. Suppose a term $g$ has, at every set $X$ , an element $g_{X} \in X \to X$ , and suppose these are related in the sense that $(g_{X}, g_{Y}) \in R_{α \to α} [α \mapsto (X, Y, R)]$ for every relation $R$ .

Proposition 164.3 — The identity free theorem ¶

Under that hypothesis, $g_{X} (a) = a$ for every set $X$ and every $a \in X$ .

Referenced from 2 locations

Dependent Parametricity

Proof of Proposition 164.3 — The identity free theorem

Proof. Take $Y : = X$ and $R : = {(a, a)}$ , the one-element relation at the given $a$ . Then $(a, a) \in R$ , so by definition 164.1 the pair $(g_{X} (a), g_{X} (a))$ lies in $R$ ; the only pair in $R$ is $(a, a)$ , so $g_{X} (a) = a$ . ◻

The proof used a relation that is not a function and not the identity: it is the graph of nothing at all. That freedom is the entire content of parametricity, and the reason (164.1) is impossible is that the relation $R$ can be chosen to separate $tt$ from the intended answer.

The dependent case will repeat this argument at a signature in which the relation itself is a term. Two things must change. The environment $ϱ$ , an external object, becomes part of the context. And the clause for $\to$ becomes a clause for $\prod_{x : A} B$ in which $B$ is instantiated at both $x_{1}$ and $x_{2}$ , so its relation depends on the proof relating them.

The dependent signature

Definition 164.4 — The signature S ¶

$S$ is Martin-Löf type theory with the following formers, presented in the order formation, introduction, elimination, computation.

A cumulative hierarchy of universes $U_{0} : U_{1} : \dots$ , with types as terms of a universe (the Russell presentation), so that $Γ ⊢ A : U_{i}$ and $Γ ⊢ A type$ are interchangeable at level $i$ .
Dependent products $\prod_{x : A} B$ , with $λ x . b$ , application $f a$ , the computation rule $(λ x . b) a \equiv b [a / x]$ and the uniqueness rule $λ x . f x \equiv f$ .
Dependent sums $\sum_{x : A} B$ , with $(a, b)$ , projections ${pr}_{1}$ and ${pr}_{2}$ , the computation rules ${pr}_{1} (a, b) \equiv a$ and ${pr}_{2} (a, b) \equiv b$ , and the uniqueness rule $({pr}_{1} p, {pr}_{2} p) \equiv p$ .
The unit type $1$ with $⋆$ and the uniqueness rule $u \equiv ⋆$ .
The natural numbers $N$ with $0$ , $suc$ and the dependent recursor ${ind}_{N}$ .
Identity types ${Id}_{A} (a, b)$ with $refl$ and the eliminator $J$ , with $J$ computing on $refl$ .

We write $U$ for an unspecified level when the level plays no role.

Referenced from 9 locations

Dependent Parametricity

Convention 164.5 — Two copies and a relation ¶

Every judgment of $S$ will be translated into a judgment of $S$ itself, in which each variable $x$ of the source is replaced by three variables $x_{1}, x_{2}, x_{R}$ . Write $e_{1}$ and $e_{2}$ for the two copies of a source expression $e$ obtained by subscripting all its free variables with $1$ and with $2$ respectively.

Referenced from 2 locations

Dependent Parametricity

The relational translation

Definition 164.6 — Translation of types and terms ¶

For a raw expression $e$ of $S$ write $e^{R}$ for its relational translation, the expression defined by the following clauses; for a type $A$ it is a relation between the two copies $A_{1}$ and $A_{2}$ , and for a term $a$ it is a proof that $a_{1}$ and $a_{2}$ are related by the translation of $a$ ’s type. $\begin{aligned} {U_{i}}^{R} & : = λ X_{1} . λ X_{2} . X_{1} \to X_{2} \to U_{i}, \\ x^{R} & : = x_{R}, \\ {\prod_{x : A} B}^{R} & : = λ f_{1} . λ f_{2} . \prod_{x_{1} : A_{1}} \prod_{x_{2} : A_{2}} \prod_{x_{R} : A^{R} x_{1} x_{2}} B^{R} (f_{1} x_{1}) (f_{2} x_{2}), \\ {λ x . b}^{R} & : = λ x_{1} . λ x_{2} . λ x_{R} . b^{R}, \\ {f a}^{R} & : = f^{R} a_{1} a_{2} a^{R} . \end{aligned}$ On contexts, $\cdot^{R} : = \cdot, {Γ, x : A}^{R} : = Γ^{R}, x_{1} : A_{1}, x_{2} : A_{2}, x_{R} : A^{R} x_{1} x_{2} .$

Referenced from 17 locations

Dependent Parametricity

Read the clause for $U_{i}$ as the decision that fixes everything else: a type is translated to a relation, so the translation of the universe is the type of relations. Read the clause for $\prod_{x : A} B$ as the dependent form of definition 164.1: two functions are related when they send related arguments to related results, and the relation at the result is $B^{R}$ instantiated at both arguments, in a context that also holds the proof $x_{R}$ .

Definition 164.7 — Translation of the remaining formers ¶

$\begin{aligned} {\sum_{x : A} B}^{R} & : = λ p_{1} . λ p_{2} . \sum_{x_{R} : A^{R} ({pr}_{1} p_{1}) ({pr}_{1} p_{2})} B^{R} ({pr}_{2} p_{1}) ({pr}_{2} p_{2}), \\ {(a, b)}^{R} & : = (a^{R}, b^{R}), {{pr}_{1} p}^{R} : = {pr}_{1} p^{R}, {{pr}_{2} p}^{R} : = {pr}_{2} p^{R}, \\ 1^{R} & : = λ u_{1} . λ u_{2} . 1, ⋆^{R} : = ⋆, \\ N^{R} & : = N, 0^{R} : = z_{R}, {suc n}^{R} : = s_{R} n^{R}, \\ {{Id}_{A} (a, b)}^{R} & : = λ p_{1} . λ p_{2} . I_{A^{R}} a^{R} b^{R} p_{1} p_{2}, {refl}^{R} : = r_{R}, \end{aligned}$ where $N$ is the inductive relation on $N \times N$ generated by $z_{R} : N 0 0$ and $s_{R} : \prod_{n_{1} : N} \prod_{n_{2} : N} N n_{1} n_{2} \to N (suc n_{1}) (suc n_{2})$ , and $I_{A_{R}} a_{R} b_{R}$ is the inductive family on ${Id}_{A_{1}} (a_{1}, b_{1}) \times {Id}_{A_{2}} (a_{2}, b_{2})$ generated by $r_{R} : I_{A_{R}} a_{R} a_{R} refl refl$ .

Referenced from 9 locations

Dependent Parametricity

Lemma 164.8 — Translation commutes with substitution ¶

For all raw expressions $b$ and $a$ and every variable $x$ , ${b [a / x]}^{R} = b^{R} [a_{1} / x_{1}] [a_{2} / x_{2}] [a^{R} / x_{R}] .$ Consequently $A ⟶_{β}^{*} A^{'}$ implies $A^{R} ⟶_{β}^{*} {A^{'}}^{R}$ .

Referenced from 5 locations

Dependent Parametricity

Proof of Lemma 164.8 — Translation commutes with substitution

Proof. By induction on $b$ . Variable case. If $b = x$ then the left side is $a^{R}$ and the right side is $x_{R} [a^{R} / x_{R}] = a^{R}$ . If $b = y$ with $y$ distinct from $x$ , both sides are $y_{R}$ . Binder case. If $b = λ y . b_{0}$ with $y \notin FV (a) \cup {x}$ , then both sides are $λ y_{1} . λ y_{2} . λ y_{R} . -$ applied to the two sides of the induction hypothesis for $b_{0}$ , and the three fresh variables $y_{1}, y_{2}, y_{R}$ avoid $FV (a^{R})$ by the same freshness condition. Remaining cases. Each clause of definition 164.6, definition 164.7 builds its output from the outputs at the immediate subterms and from the two copies $e_{1}, e_{2}$ , and both operations commute with substitution.

For the consequence, a one-step $β$ -reduction $(λ x . b) a ⟶_{β} b [a / x]$ translates to $\begin{aligned} {(λ x . b) a}^{R} & \overset{d e f i n i t i o n 164.6}{=} (λ x_{1} . λ x_{2} . λ x_{R} . b^{R}) a_{1} a_{2} a^{R} \\ ⟶_{β}^{*} b^{R} [a_{1} / x_{1}] [a_{2} / x_{2}] [a^{R} / x_{R}], \end{aligned}$ which is ${b [a / x]}^{R}$ by the displayed equation; the compatible closure follows because every clause is a congruence. ◻

Theorem 164.9 — Abstraction ¶

If $Γ ⊢ a : A$ in $S$ , then $Γ^{R} ⊢ a^{R} : A^{R} a_{1} a_{2}$ in $S$ .

Referenced from 10 locations

Dependent Parametricity

Proof of Theorem 164.9 — Abstraction

Proof. By induction on the derivation of $Γ ⊢ a : A$ . Throughout, the induction hypothesis at a subterm $b$ of type $B$ is $Γ^{R} ⊢ b^{R} : B^{R} b_{1} b_{2}$ , and we use that each of the two copies $Γ_{1}, Γ_{2}$ is a sub-context of $Γ^{R}$ , so every source judgment can be reused in each copy.

Variable. For $x : A$ in $Γ$ , definition 164.6 puts $x_{R} : A^{R} x_{1} x_{2}$ in $Γ^{R}$ , and $x^{R} = x_{R}$ .

Universe. For $Γ ⊢ A : U_{i}$ the required conclusion is $Γ^{R} ⊢ A^{R} : {U_{i}}^{R} A_{1} A_{2}$ , and ${U_{i}}^{R} A_{1} A_{2} \overset{β}{\equiv} A_{1} \to A_{2} \to U_{i},$ so the conclusion says that $A^{R}$ is a relation between the two copies of $A$ . This is what the induction hypothesis at $A$ delivers in every clause below, and the two statements are therefore proved simultaneously: types and terms are the same syntactic class in definition 164.4.

Product formation. Assume $Γ ⊢ A : U_{i}$ and $Γ, x : A ⊢ B : U_{j}$ . The induction hypotheses give $A^{R} : A_{1} \to A_{2} \to U_{i}$ over $Γ^{R}$ and $B^{R} : B_{1} \to B_{2} \to U_{j}$ over $Γ^{R}, x_{1} : A_{1}, x_{2} : A_{2}, x_{R} : A^{R} x_{1} x_{2}$ . The displayed body of ${\prod_{x : A} B}^{R}$ in definition 164.6 is then a well-formed type of the universe at the level of the source product, formed by three nested products over those three variables.

Abstraction. Assume $Γ, x : A ⊢ b : B$ , so that $Γ ⊢ λ x . b : \prod_{x : A} B$ . The induction hypothesis gives $b^{R} : B^{R} b_{1} b_{2}$ over the extended translated context. Abstracting the three variables gives ${λ x . b}^{R} : \prod_{x_{1} : A_{1}} \prod_{x_{2} : A_{2}} \prod_{x_{R} : A^{R} x_{1} x_{2}} B^{R} b_{1} b_{2},$ and the type ${\prod_{x : A} B}^{R} (λ x_{1} . b_{1}) (λ x_{2} . b_{2})$ $β$ -reduces to the same one, because $(λ x_{j} . b_{j}) x_{j} \equiv b_{j}$ by the computation rule of definition 164.4.

Application. Assume $Γ ⊢ f : \prod_{x : A} B$ and $Γ ⊢ a : A$ . The induction hypotheses give $f^{R} : {\prod_{x : A} B}^{R} f_{1} f_{2}$ and $a^{R} : A^{R} a_{1} a_{2}$ . Instantiating the three products of ${\prod_{x : A} B}^{R}$ at $a_{1}, a_{2}, a^{R}$ yields $f^{R} a_{1} a_{2} a^{R} : B^{R} [a_{1}, a_{2}, a^{R} / x_{1}, x_{2}, x_{R}] (f_{1} a_{1}) (f_{2} a_{2}),$ and lemma 164.8 identifies the displayed type with ${B [a / x]}^{R} (f_{1} a_{1}) (f_{2} a_{2})$ , which is the required conclusion.

Sum, unit, natural numbers, identity. Each is a copy of the product case with the clause of definition 164.7 in place of the clause for $\prod_{x : A} B$ : the introduction form translates to the introduction form of the translated type, and the elimination form is typed by instantiating the translated family. For $N$ and ${Id}_{A} (a, b)$ the eliminator case additionally uses that the translated inductive family has one constructor for each source constructor and the same recursive structure, so the translated motive is eliminated by the translated eliminator.

Conversion. If $Γ ⊢ A \equiv A^{'} type$ is derived from $A ⟶_{β}^{*} C$ and $A^{'} ⟶_{β}^{*} C$ , then $A^{R} ⟶_{β}^{*} C^{R}$ and ${A^{'}}^{R} ⟶_{β}^{*} C^{R}$ by lemma 164.8, so the two translated types are convertible and the conversion rule of $S$ applies. ◻

Corollary 164.10 — Closed terms are self-related ¶

If $\cdot ⊢ a : A$ then $\cdot ⊢ a^{R} : A^{R} a a$ .

Referenced from 3 locations

Dependent Parametricity

Proof of Corollary 164.10 — Closed terms are self-related

Proof. Both copies of a closed expression are the expression itself, and $\cdot^{R} = \cdot$ by definition 164.6. ◻

The translation computed on an abstract data type

Definition 164.11 — The counter interface ¶

Fix $Client : = \prod_{S : U_{0}} S \to (S \to S) \to (S \to N) \to N,$ the type of programs that use a state type $S$ through an initial state, a step function and a readout, and return a number. Two implementations of the interface are $\begin{array}{ll} first: & S : = N, i : = 0, s : = suc, r : = λ n . n; \\ second: & S : = N \times N, i : = (0, suc 0), \\ s : = λ p . (suc ({pr}_{1} p), {pr}_{2} p), r : = λ p . {pr}_{1} p . \end{array}$ The second carries an extra component that no operation reads.

Referenced from 4 locations

Dependent Parametricity

Example 164.12 — The translation of Client ¶

Apply definition 164.6 clause by clause. The outer product is over $S : U_{0}$ , so by the universe clause the translation introduces three variables $S_{1}, S_{2} : U_{0}$ and $S_{R} : S_{1} \to S_{2} \to U_{0}$ . Each of the three remaining arguments is a non-dependent product, so its clause introduces two arguments and a relatedness hypothesis. The codomain is $N$ , whose translation is $N$ . Writing $c_{1}, c_{2}$ for the two copies, $\begin{aligned} {Client}^{R} c_{1} c_{2} \equiv & \prod_{S_{1} : U_{0}} \prod_{S_{2} : U_{0}} \prod_{S_{R} : S_{1} \to S_{2} \to U_{0}} \\ \prod_{i_{1} : S_{1}} \prod_{i_{2} : S_{2}} \prod_{i_{R} : S_{R} i_{1} i_{2}} \\ \prod_{s_{1} : S_{1} \to S_{1}} \prod_{s_{2} : S_{2} \to S_{2}} \\ \prod_{s_{R} : \prod_{x_{1} : S_{1}} \prod_{x_{2} : S_{2}} S_{R} x_{1} x_{2} \to S_{R} (s_{1} x_{1}) (s_{2} x_{2})} \\ \prod_{r_{1} : S_{1} \to N} \prod_{r_{2} : S_{2} \to N} \\ \prod_{r_{R} : \prod_{x_{1} : S_{1}} \prod_{x_{2} : S_{2}} S_{R} x_{1} x_{2} \to N (r_{1} x_{1}) (r_{2} x_{2})} \\ N (c_{1} S_{1} i_{1} s_{1} r_{1}) (c_{2} S_{2} i_{2} s_{2} r_{2}) . \end{aligned}$ Every hypothesis is forced: the clause for a product supplies exactly one relatedness argument for each argument of the source type, and no clause is free to omit one.

Referenced from 5 locations

Dependent Parametricity

Lemma 164.13 — Identity extension at ¶

For all $m, n : N$ the types $N m n$ and ${Id}_{N} (m, n)$ are logically equivalent: there are terms in each direction.

Referenced from 10 locations

Dependent Parametricity

Proof of Lemma 164.13 — Identity extension at

Proof. From $N$ to ${Id}_{N} (-, -)$ : eliminate the inductive relation with motive $λ m . λ n . λ_. {Id}_{N} (m, n)$ . The case $z_{R}$ requires ${Id}_{N} (0, 0)$ , discharged by $refl$ ; the case $s_{R} m n q$ has an induction hypothesis $p : {Id}_{N} (m, n)$ and requires ${Id}_{N} (suc m, suc n)$ , discharged by ${ap}_{suc} (p)$ .

From ${Id}_{N} (-, -)$ to $N$ : it suffices, by $J$ with motive $λ m . λ n . λ_. N m n$ , to give $N m m$ for every $m$ , and that is obtained by induction on $m$ with ${ind}_{N}$ : the base case is $z_{R}$ and the step case is $s_{R} m m$ applied to the induction hypothesis. ◻

Lemma 164.13 is what makes a relational conclusion at $N$ usable: the abstraction theorem produces $N$ , and the statement we want is an identity. The same question at an arbitrary type is the identity extension property, and remark 164.18 records exactly what is and is not available.

Theorem 164.14 — Representation independence for the counter ¶

Let $\cdot ⊢ c : Client$ . Then ${Id}_{N} (c N 0 suc (λ n . n), c (N \times N) (0, suc 0) (λ p . (suc ({pr}_{1} p), {pr}_{2} p)) (λ p . {pr}_{1} p))$ is inhabited.

Referenced from 4 locations

Dependent Parametricity

Proof of Theorem 164.14 — Representation independence for the counter

Proof. Proof idea. Instantiate the relation variable of example 164.12 at the relation “the first state is the first component of the second”, check the three relatedness hypotheses, and convert the relational conclusion at $N$ into an identity by lemma 164.13. The extra component of the second implementation is never mentioned by the relation, which is why it cannot be observed.

By corollary 164.10 we have $c^{R} : {Client}^{R} c c$ . Instantiate the first three arguments with $S_{1} : = N, S_{2} : = N \times N, S_{R} : = λ n . λ p . {Id}_{N} (n, {pr}_{1} p) .$

Initial states. The required type is $S_{R} 0 (0, suc 0)$ , which computes as $S_{R} 0 (0, suc 0) \overset{β}{\equiv} {Id}_{N} (0, {pr}_{1} (0, suc 0)) \overset{{pr}_{1} - c o m p .}{\equiv} {Id}_{N} (0, 0),$ inhabited by $refl$ .

Step functions. The required type is $\prod_{n : N} \prod_{p : N \times N} S_{R} n p \to S_{R} (suc n) ((λ p . (suc ({pr}_{1} p), {pr}_{2} p)) p) .$ Given $q : {Id}_{N} (n, {pr}_{1} p)$ , the target computes as $S_{R} (suc n) (suc ({pr}_{1} p), {pr}_{2} p) \overset{β, {pr}_{1} - c o m p .}{\equiv} {Id}_{N} (suc n, suc ({pr}_{1} p)),$ inhabited by ${ap}_{suc} (q)$ .

Readouts. The required type is $\prod_{n : N} \prod_{p : N \times N} S_{R} n p \to N n ({pr}_{1} p)$ , and given $q : {Id}_{N} (n, {pr}_{1} p)$ the conclusion follows from lemma 164.13 in the direction from identities to $N$ .

Conclusion. Instantiating $c^{R}$ at these twelve arguments gives a term of type $N (c N 0 suc (λ n . n)) (c (N \times N) (0, suc 0) (λ p . (suc ({pr}_{1} p), {pr}_{2} p)) (λ p . {pr}_{1} p)),$ and lemma 164.13 in the direction from $N$ to identities gives the displayed inhabitant. ◻

Example 164.15 — The failure of eq:dp-bad-id, made exact ¶

Let $\cdot ⊢ g : \prod_{A : U_{0}} A \to A$ . Fix $A : U_{0}$ and $a : A$ , and instantiate $g^{R}$ at $\begin{aligned} A_{1} : = A, A_{2} : = A, A_{R} : = λ x . λ y . {Id}_{A} (y, a), \\ x_{1} : = a, x_{2} : = a, x_{R} : = refl . \end{aligned}$ The hypothesis $A_{R} a a$ computes to ${Id}_{A} (a, a)$ and is inhabited by $refl$ , and the conclusion is $A_{R} (g A a) (g A a)$ , which computes to ${Id}_{A} (g A a, a)$ . Hence $g A a = a$ for every $A$ and $a$ : no closed term of that type can behave as (164.1) describes. The relation $A_{R}$ used here is not the graph of a function and is not symmetric; the universe clause of definition 164.6 permits it because it quantifies over all relations.

Referenced from 6 locations

Exercise 164.1 ¶

★☆☆ Let $\cdot ⊢ k : \prod_{A : U_{0}} \prod_{B : U_{0}} A \to B \to A$ . Choose relations and arguments as in example 164.15 and derive ${Id}_{A} (k A B a b, a)$ . State which of the two relation variables must be instantiated at a singleton relation and why the other may be arbitrary.

Referenced from 3 locations

Dependent Parametricity

Exercise 164.2 ¶

★★☆ Compute ${(\sum_{A : U_{0}} A \times (A \to A))}^{R}$ $p_{1} p_{2}$ in full by definition 164.7, and show that its inhabitants are exactly the triples consisting of a relation between the two carriers together with proofs that the two chosen elements and the two chosen functions are related. Then exhibit two closed elements of that sum whose relatedness fails for every relation, and name the component at which it fails.

Referenced from 2 locations

Dependent Parametricity

Exercise 164.3 ¶

★★☆ Theorem 164.9 concludes $Γ^{R} ⊢ a^{R} : A^{R} a_{1} a_{2}$ , not $Γ^{R} ⊢ a^{R} : A^{R} a a$ .

Explain, using definition 164.6 for contexts, why the two statements differ for an open term, and give a term for which the second is not even well typed.
Show that they coincide for a closed term, and identify the clause of definition 164.6 that makes this work.

Referenced from 2 locations

Dependent Parametricity

Identity types, universes, and what is not derivable

Lemma 164.13 converted a relational conclusion at $N$ into an identity. The general question is whether $A^{R}$ , instantiated at the reflexive relations, is the identity type of $A$ .

Definition 164.16 — Identity extension ¶

The closed type $A$ of $S$ satisfies identity extension when for all $a_{1}, a_{2} : A$ the types $A^{R} a_{1} a_{2}$ and ${Id}_{A} (a_{1}, a_{2})$ are logically equivalent.

Referenced from 2 locations

Dependent Parametricity

Proposition 164.17 — Identity extension is at least function extensionality ¶

If $N \to N$ satisfies identity extension, then for all $f_{1}, f_{2} : N \to N$ , $(\prod_{n : N} {Id}_{N} (f_{1} n, f_{2} n)) ⟶ {Id}_{N \to N} (f_{1}, f_{2})$ is inhabited.

Referenced from 3 locations

Dependent Parametricity

Proof of Proposition 164.17 — Identity extension is at least function extensionality

Proof. Unfolding definition 164.6 at the non-dependent product, ${(N \to N)}^{R} f_{1} f_{2} \equiv \prod_{n_{1} : N} \prod_{n_{2} : N} N n_{1} n_{2} \to N (f_{1} n_{1}) (f_{2} n_{2}) .$ Assume $H$ of type $\prod_{n : N} {Id}_{N} (f_{1} n, f_{2} n)$ , and let $n_{1}, n_{2}$ and $q : N n_{1} n_{2}$ be given. By lemma 164.13, $q$ yields ${Id}_{N} (n_{1}, n_{2})$ , and transporting $H n_{1}$ along it gives ${Id}_{N} (f_{1} n_{1}, f_{2} n_{2})$ ; the same lemma turns that back into $N (f_{1} n_{1}) (f_{2} n_{2})$ . Hence $H$ yields an element of ${(N \to N)}^{R} f_{1} f_{2}$ , and identity extension converts it into ${Id}_{N \to N} (f_{1}, f_{2})$ . ◻

Remark 164.18 — What the abstraction theorem does and does not give ¶

Theorem 164.9 is a statement about the syntax: it produces, for each term, a proof in $S$ . It does not produce identity extension, and by proposition 164.17 it cannot, since function extensionality is not among the rules of definition 164.4. The reason is visible in the universe clause of definition 164.6: the translation of $U_{i}$ is the type of all relations, so a relation variable $A_{R}$ standing in a translated context is an arbitrary relation, and nothing in the syntax connects it to ${Id}_{A} (-, -)$ .

Identity extension is available in a model. Atkey, Ghani and Johann interpret types as reflexive graphs, in which each object carries a distinguished reflexivity edge, and build from them a category with families; their Theorem 1 states that the category of reflexive graphs supports dependent products and natural numbers, and, assuming a universe $U$ of small sets, a predicative universe closed under both, with an impredicative universe when $U$ is closed under large products. Their interpretation of the type-theoretic universe is designed so that identity extension holds, which is why they call the model relationally parametric. Their Theorem 2 gives the dependent naturality statement: if $Γ ⊢ M : \prod_{a : U} T a \to T a$ then for $Γ ⊢ X, Y : U$ , $Γ ⊢ f : T X \to T Y$ and $Γ ⊢ x : T X$ , the equation $Γ ⊢ f (M X x) = M Y (f x) : T Y$ is sound in their model; and their Theorem 3 states that in the impredicative variant every $X$ -indexed functor has an initial algebra. Those three statements hold at their signature, in their model, and are not consequences of theorem 164.9.

Referenced from 4 locations

Dependent Parametricity

Exercise 164.4 ¶

★☆☆ Show that $N$ and $1$ satisfy identity extension, and that $N \times N$ does provided $N$ does. Then state what would have to be proved for $\sum_{A : U_{0}} A$ , and identify the clause of definition 164.6 that makes the question depend on the universe.

Referenced from 2 locations

Dependent Parametricity

External and internal relational structure

Theorem 164.9 is a function on derivations, defined in the metatheory. Its instances are terms of $S$ , but the function itself is not. A program of $S$ that receives a term as input cannot apply the abstraction theorem to it, because the input is a value of a type, not a derivation.

The natural repair is to add the conclusion as an axiom.

Definition 164.19 — The parametricity axiom ¶

Let $S^{p}$ be $S$ extended, for every closed type $B$ , with a constant ${param}_{B} : \prod_{x : B} B^{R} x x$ and no computation rule.

Referenced from 3 locations

Dependent Parametricity

Proposition 164.20 — The axiom has no local interpretation ¶

The assignment ${param}_{B} a \mapsto a^{R}$ does not define a translation from $S^{p}$ to $S$ .

Referenced from 3 locations

Dependent Parametricity

Proof of Proposition 164.20 — The axiom has no local interpretation

Proof. Take $B : = N$ and the open term $a : = x$ in the context $x : N$ . Then ${param}_{N} x$ is well typed over $x : N$ , whereas $x^{R} = x_{R}$ by definition 164.6, and $x_{R}$ is not declared in the context $x : N$ . The proposed image is therefore not a term over the context of its source. ◻

Proposition 164.21 — The axiom breaks canonicity ¶

$S^{p}$ has closed normal forms of type $N$ that are not numerals.

Referenced from 4 locations

Proof of Proposition 164.21 — The axiom breaks canonicity

Proof. Let $B : = \prod_{A : U_{0}} A \to A$ and let $id : = λ A . λ x . x$ . By example 164.15 the term ${param}_{B} id$ , instantiated as there, has type ${Id}_{N} (id N 0, 0)$ ; call that term $p$ . Now consider $J (λ u . λ v . λ_. N; λ u . suc u; p) .$ Its type is $N$ . It is closed. It has no reduction: the computation rule for $J$ in definition 164.4 fires only on $refl$ , and $p$ is headed by ${param}_{B}$ , which has no computation rule by definition 164.19. ◻

The two propositions say what an internal account must supply that an axiom does not: a term former for relational structure must come with binders that place the relational variables in the context where they are needed, and with computation rules that let a proof built from it reduce. Both are changes to the syntax of $S$ , not additions to its constants. A calculus that makes those changes replaces the metatheoretic operation $-^{R}$ by an operator of the object theory with its own formation, introduction, elimination and computation rules; the interval-free span calculus of Altenkirch, Kaposi and Shulman is one such system, and it is developed separately because its judgments and its metatheory are not those of definition 164.4.

Boundary

Proved here. The relational translation (definition 164.6, definition 164.7), its substitution lemma (lemma 164.8), the abstraction theorem (theorem 164.9) and its closed-term corollary, identity extension at $N$ (lemma 164.13), the free theorem for the polymorphic identity type (example 164.15), representation independence for the counter interface (theorem 164.14), and the two obstructions to internalizing the translation (proposition 164.20, proposition 164.21).

Owned elsewhere. The reflexive-graph model and its three theorems belong to Atkey, Ghani and Johann and hold at their signature, as recorded in remark 164.18. Proof-relevant relational structure — where a relation carries not a proposition but a type of witnesses — is a separate development; nothing above is generalized to it by analogy. Cubical paths and their bridge and Gel formers belong to the calculi that define them.

Inductive families. Definition 164.7 gives the clauses for $N$ and for the identity type by the same schema: a source inductive family with constructors $c_{1}, \dots, c_{k}$ translates to an inductive family with one constructor $c_{i}^{R}$ for each $c_{i}$ , whose arguments are the translations of the arguments of $c_{i}$ . The general statement for arbitrary inductive families, together with the argument that the translation preserves strict positivity and hence well-foundedness, is due to Bernardy, Jansson and Paterson; only the two instances used above are proved here.

Size indices. Uniformity can be used to control an index rather than a type: a quantifier that is parametric rather than continuous makes a function’s behaviour independent of the index it is instantiated at, and that is what allows an index to be treated as a size. The parametric quantifiers of Nuyts, Vezzosi and Devriese are the standard calculus for this, and their rules differ from those of definition 164.4: they distinguish a parametric from a continuous function type, with separate formation, introduction and elimination rules. This chapter defines no sized recursion calculus and proves no theorem about one.

Suggested first pass.

Problems exercise 164.6, exercise 164.5, and exercise 164.8 form the suggested first pass. None of these problems is a prerequisite for a later chapter.

Exercise 164.5 ¶

★★★ Theorem 164.9 displayed the cases for variables, universes, products, abstraction, application and conversion, and delegated the sum, unit, natural-number and identity cases as copies of the product case. Write them.

Give the sum case in full: the formation, introduction and both elimination rules, checking at each step which clause of definition 164.7 is used and that the computation rules of definition 164.4 make the translated equations hold.
Give the case of ${ind}_{N}$ : state the translated motive, the two translated methods, and the type of the translated eliminator, and check that the translated computation rules follow from the source ones.
Give the case of $J$ , and state exactly where the argument would fail if the identity type had the eliminator $K$ in addition.

Referenced from 3 locations

Dependent Parametricity

Exercise 164.6 ¶

★★★ Replace the counter of definition 164.11 by a queue interface $QClient : = \prod_{S : U_{0}} S \to (N \to S \to S) \to (S \to 1 + (N \times S)) \to N,$ with the two standard implementations: a single list, and a pair of lists holding the front in order and the back reversed.

Write both implementations, using $N$ -indexed lists encoded with $Σ$ and $N$ if no list former is available, and state the relation $S_{R}$ that relates them.
Compute ${QClient}^{R}$ as in example 164.12.
Prove the three relatedness hypotheses. The one for the dequeue operation requires a case analysis; display both cases and say which one needs the reversal.
Conclude representation independence, and state which step used lemma 164.13.

Referenced from 3 locations

Dependent Parametricity

Exercise 164.7 ¶

★★☆ Investigate the boundary of theorem 164.14.

Add to $Client$ a fourth argument of type $S \to S \to 2$ testing states for equality, and exhibit two implementations of the extended interface, together with a client, for which the two runs differ. Identify the relatedness hypothesis that fails.
Show that if instead the fourth argument has type $N \to N \to 2$ the hypothesis is satisfied, and explain the difference in one sentence.

Referenced from 2 locations

Dependent Parametricity

Exercise 164.8 ¶

★★★ Practical project.dependent-parametricity-translator Implement, in Agda, the relational translation of definition 164.6, definition 164.7 and use it to produce free theorems.

Calculus to implement. Represent the raw syntax of $S$ restricted to $U_{0}$ , $U_{1}$ , dependent products, dependent sums, $1$ , $N$ and identity types, with de Bruijn indices. Implement a bidirectional type checker for it and the translation $-^{R}$ as a function on raw terms, with the context translation of definition 164.6. Capture-avoiding substitution and the tripling of variables must both be handled explicitly: a source variable at de Bruijn index $i$ becomes three variables, and every index in a translated term must be recomputed.

Invariant. For every input derivation $Γ ⊢ a : A$ the program must produce a term $a^{R}$ that its own checker accepts at type $A^{R} a_{1} a_{2}$ in the context $Γ^{R}$ . This is the executable form of theorem 164.9; the checker, not the translator, is the judge.

Concrete result. A report that, for each named input, prints the translated context, the translated type, the translated term, and the checker’s verdict.

Acceptance test. The following must be accepted, with the printed translated type equal to the one computed by hand in the chapter: the identity $λ A . λ x . x$ at $\prod_{A : U_{0}} A \to A$ , whose translation must be $λ A_{1} . λ A_{2} . λ A_{R} . λ x_{1} . λ x_{2} . λ x_{R} . x_{R};$ the term $λ A . λ B . λ x . λ y . x$ at the type of exercise 164.1; the counter clients of definition 164.11, whose translated type must match example 164.12 up to renaming; and $λ n . suc n$ at $N \to N$ , whose translation must use $s_{R}$ . The following must be rejected by the checker: the term $λ A . λ x . x_{R}$ , in which a relational variable is used where a source variable is required; and a hand-written “translation” of $id$ that omits the argument $x_{R}$ . Produce three mutations that still run — drop $x_{R}$ from the context translation, translate $U_{0}$ to $λ X_{1} . λ X_{2} . U_{0}$ , and translate a product without the relatedness argument — and confirm that each makes the checker reject at least one accepted case. State explicitly that the program illustrates theorem 164.9 on finitely many derivations and does not prove it.

Referenced from 3 locations