appendix sectionrules

Gradual source and ground-cast target

The source and target of chapter 11 share $A, B ::= 2 ∣ N ∣ ? ∣ A \to B, G ::= 2 ∣ N ∣ ? \to ? .$ For every $A \neq ?$ , the ground-shape operation used below is $gnd (2) = 2, gnd (N) = N, gnd (A \to B) = ? \to ? .$ Consistency is the least relation generated by

? \sim_{c} A

C-UnkL

A \sim_{c} ?

C-UnkR

2 \sim_{c} 2

C-Bool

N \sim_{c} N

C-Nat

A_{1} \sim_{c} B_{1}

A_{2} \sim_{c} B_{2}

A_{1} \to A_{2} \sim_{c} B_{1} \to B_{2}

C-Arr

Function matching is the partial operation $fun (A \to B) = A \to B$ and $fun (?) = ? \to ?$ . For $e ::= b ∣ n ∣ x ∣ λ x : A . e ∣ (e_{1} e_{2})^{ℓ}$ , the complete source table is

Γ ⊢ b : 2

G-Bool

Γ ⊢ n : N

G-Nat

x : A \in Γ

Γ ⊢ x : A

G-Var

Γ, x : A ⊢ e : B

Γ ⊢ λ x : A . e : A \to B

G-Lam

Γ ⊢ e_{1} : C

fun (C) = A \to B

Γ ⊢ e_{2} : D

D \sim_{c} A

Γ ⊢ (e_{1} e_{2})^{ℓ} : B

G-App

Target terms and blame-label complementation are $a ::= b ∣ n ∣ x ∣ λ x : A . a ∣ a_{1} a_{2} ∣ ⟨ B \Leftarrow A ⟩^{p} a ∣ {blame}_{p}, \overset{―}{\bar{p}} = p .$ Their complete typing table is

Γ ⊢_{C} b : 2

T-Bool

Γ ⊢_{C} n : N

T-Nat

x : A \in Γ

Γ ⊢_{C} x : A

T-Var

Γ, x : A ⊢_{C} a : B

Γ ⊢_{C} λ x : A . a : A \to B

T-Lam

Γ ⊢_{C} a_{1} : A \to B

Γ ⊢_{C} a_{2} : A

Γ ⊢_{C} a_{1} a_{2} : B

T-App

Γ ⊢_{C} a : A

A \sim_{c} B

Γ ⊢_{C} ⟨ B \Leftarrow A ⟩^{p} a : B

T-Cast

Γ ⊢_{C} {blame}_{p} : B

T-Blame

The value and evaluation-frame grammars are $\begin{array}{rcl} v & ::= & b ∣ n ∣ λ x : A . a ∣ ⟨ A_{2} \to B_{2} \Leftarrow A_{1} \to B_{1} ⟩^{p} v ∣ ⟨ ? \Leftarrow G ⟩^{p} v, \\ F & ::= & [] a ∣ v [] ∣ ⟨ B \Leftarrow A ⟩^{p} [] . \end{array}$ Reduction is compatible with $E ::= [] ∣ F [E]$ and has exactly

(λ x : A . a) v ⟼ a [v / x]

E-Beta

B \in {2, N}

⟨ B \Leftarrow B ⟩^{p} v ⟼ v

E-IdBase

⟨ ? \Leftarrow ? ⟩^{p} v ⟼ v

E-IdUnk

⟨ G \Leftarrow ? ⟩^{p} (⟨ ? \Leftarrow G ⟩^{q} v) ⟼ v

E-Project

G_{1} \neq G_{2}

⟨ G_{2} \Leftarrow ? ⟩^{p} (⟨ ? \Leftarrow G_{1} ⟩^{q} v) ⟼ {blame}_{p}

E-Mismatch

A \neq ?

A \neq gnd (A)

⟨ ? \Leftarrow A ⟩^{p} v ⟼ ⟨ ? \Leftarrow gnd (A) ⟩^{p} (⟨ gnd (A) \Leftarrow A ⟩^{p} v)

E-Ground

A \neq ?

A \neq gnd (A)

⟨ A \Leftarrow ? ⟩^{p} v ⟼ ⟨ A \Leftarrow gnd (A) ⟩^{p} (⟨ gnd (A) \Leftarrow ? ⟩^{p} v)

E-Expand

u = ⟨ A_{2} \to B_{2} \Leftarrow A_{1} \to B_{1} ⟩^{p} v

u w ⟼ ⟨ B_{2} \Leftarrow B_{1} ⟩^{p} (v (⟨ A_{1} \Leftarrow A_{2} ⟩^{\bar{p}} w))

E-WrapApp

F [{blame}_{p}] ⟼ {blame}_{p}

E-Blame

The polar blame-safety orders are generated by

2 ⪯^{+} 2

P-Bool

N ⪯^{+} N

P-Nat

A ⪯^{+} ?

P-Unk

B_{1} ⪯^{-} A_{1}

A_{2} ⪯^{+} B_{2}

A_{1} \to A_{2} ⪯^{+} B_{1} \to B_{2}

P-Arr

2 ⪯^{-} 2

N-Bool

N ⪯^{-} N

N-Nat

? ⪯^{-} A

N-Unk

A ⪯^{-} G

A ⪯^{-} ?

N-GroundUnk

B_{1} ⪯^{+} A_{1}

A_{2} ⪯^{-} B_{2}

A_{1} \to A_{2} ⪯^{-} B_{1} \to B_{2}

N-Arr

Here $G$ is ground in N-GroundUnk.

Cast insertion has the complete table

Γ ⊢ b ⇝ b : 2

I-Bool

Γ ⊢ n ⇝ n : N

I-Nat

x : A \in Γ

Γ ⊢ x ⇝ x : A

I-Var

Γ, x : A ⊢ e ⇝ a : B

Γ ⊢ λ x : A . e ⇝ λ x : A . a : A \to B

I-Lam

Γ ⊢ e_{1} ⇝ a_{1} : C

fun (C) = A \to B

Γ ⊢ e_{2} ⇝ a_{2} : D

D \sim_{c} A

Γ ⊢ (e_{1} e_{2})^{ℓ} ⇝ (⟨ A \to B \Leftarrow C ⟩^{ℓ_{f}} a_{1}) (⟨ A \Leftarrow D ⟩^{ℓ_{a}} a_{2}) : B

I-App

Here $ℓ_{f}, ℓ_{a}$ are globally fresh roots determined by $ℓ$ .

Type and context precision are

A ⊑_{ty} ?

Pr-Unk

2 ⊑_{ty} 2

Pr-Bool

N ⊑_{ty} N

Pr-Nat

A_{1} ⊑_{ty} B_{1}

A_{2} ⊑_{ty} B_{2}

A_{1} \to A_{2} ⊑_{ty} B_{1} \to B_{2}

Pr-Arr

\cdot ⊑_{ctx} \cdot

PrCtx-Empty

Γ ⊑_{ctx} Γ^{'}

A ⊑_{ty} A^{'}

Γ, x : A ⊑_{ctx} Γ^{'}, x : A^{'}

PrCtx-Extend

Source-term precision is the least compatible relation generated by

b ⊑_{src} b

PrTm-Bool

n ⊑_{src} n

PrTm-Nat

x ⊑_{src} x

PrTm-Var

A ⊑_{ty} A^{'}

e ⊑_{src} e^{'}

λ x : A . e ⊑_{src} λ x : A^{'} . e^{'}

PrTm-Lam

e_{1} ⊑_{src} e_{1}^{'}

e_{2} ⊑_{src} e_{2}^{'}

(e_{1} e_{2})^{ℓ} ⊑_{src} (e_{1}^{'} e_{2}^{'})^{ℓ}

PrTm-App

For $Δ = (x_{1} : A_{1} ⊑_{ty} A_{1}^{'}, \dots, x_{n} : A_{n} ⊑_{ty} A_{n}^{'})$ , target precision presupposes both projected target typings and the displayed result-type precision, where $Δ_{L} = (x_{1} : A_{1}, \dots, x_{n} : A_{n}), Δ_{R} = (x_{1} : A_{1}^{'}, \dots, x_{n} : A_{n}^{'}) .$ Its structural rules are

Δ ⊢ b : 2 ⊑_{C} b : 2

CPr-Bool

Δ ⊢ n : N ⊑_{C} n : N

CPr-Nat

x : A ⊑_{ty} A^{'} \in Δ

Δ ⊢ x : A ⊑_{C} x : A^{'}

CPr-Var

A ⊑_{ty} A^{'}

Δ, x : A ⊑_{ty} A^{'} ⊢ a : B ⊑_{C} a^{'} : B^{'}

Δ ⊢ λ x : A . a : A \to B ⊑_{C} λ x : A^{'} . a^{'} : A^{'} \to B^{'}

CPr-Lam

Δ ⊢ a_{1} : A \to B ⊑_{C} a_{1}^{'} : A^{'} \to B^{'}

Δ ⊢ a_{2} : A ⊑_{C} a_{2}^{'} : A^{'}

Δ ⊢ a_{1} a_{2} : B ⊑_{C} a_{1}^{'} a_{2}^{'} : B^{'}

CPr-App

The remaining rules are

Δ ⊢ a : S ⊑_{C} a^{'} : S^{'}

S \sim_{c} T

S^{'} \sim_{c} T^{'}

T ⊑_{ty} T^{'}

Δ ⊢ ⟨ T \Leftarrow S ⟩^{p} a : T ⊑_{C} ⟨ T^{'} \Leftarrow S^{'} ⟩^{p} a^{'} : T^{'}

CPr-Cast

Δ ⊢ a : S ⊑_{C} a^{'} : U

S \sim_{c} T

T ⊑_{ty} U

Δ ⊢ ⟨ T \Leftarrow S ⟩^{p} a : T ⊑_{C} a^{'} : U

CPr-CastL

Δ ⊢ a : S ⊑_{C} a^{'} : U

U \sim_{c} V

S ⊑_{ty} V

Δ ⊢ a : S ⊑_{C} ⟨ V \Leftarrow U ⟩^{p} a^{'} : V

CPr-CastR

Δ_{R} ⊢_{C} a^{'} : A^{'}

A ⊑_{ty} A^{'}

Δ ⊢ {blame}_{p} : A ⊑_{C} a^{'} : A^{'}

CPr-Blame

There is no rule relating an arbitrary left term to right-hand blame.

For $Δ = (x_{1} : A_{1} ⊑_{ty} A_{1}^{'}, \dots, x_{n} : A_{n} ⊑_{ty} A_{n}^{'})$ , related closing substitutions are $ρ = (v_{1} / x_{1}, \dots, v_{n} / x_{n}) ⊑_{e n v} ρ^{'} = (v_{1}^{'} / x_{1}, \dots, v_{n}^{'} / x_{n})$ exactly when every $v_{i}, v_{i}^{'}$ is closed and $\cdot ⊢ v_{i} : A_{i} ⊑_{C} v_{i}^{'} : A_{i}^{'}$ . Simultaneous substitution is written $a [ρ]$ .

Related evaluation frames have the rules

Δ ⊢ a : A ⊑_{C} a^{'} : A^{'}

B ⊑_{ty} B^{'}

Δ ⊢ [] a : (A \to B) \Rightarrow B ⊑_{F} [] a^{'} : (A^{'} \to B^{'}) \Rightarrow B^{'}

FPr-AppL

Δ ⊢ v : A \to B ⊑_{C} v^{'} : A^{'} \to B^{'}

Δ ⊢ v [] : A \Rightarrow B ⊑_{F} v^{'} [] : A^{'} \Rightarrow B^{'}

FPr-AppR

S ⊑_{ty} S^{'}

S \sim_{c} T

S^{'} \sim_{c} T^{'}

T ⊑_{ty} T^{'}

Δ ⊢ ⟨ T \Leftarrow S ⟩^{p} [] : S \Rightarrow T ⊑_{F} ⟨ T^{'} \Leftarrow S^{'} ⟩^{p} [] : S^{'} \Rightarrow T^{'}

FPr-Cast

Evaluation-context precision is the reflexive transitive closure generated by

S ⊑_{ty} S^{'}

Δ ⊢ [] : S \Rightarrow S ⊑_{F} [] : S^{'} \Rightarrow S^{'}

FPr-Hole

Δ ⊢ E : S \Rightarrow T ⊑_{F} E^{'} : S^{'} \Rightarrow T^{'}

Δ ⊢ F : T \Rightarrow U ⊑_{F} F^{'} : T^{'} \Rightarrow U^{'}

Δ ⊢ F [E] : S \Rightarrow U ⊑_{F} F^{'} [E^{'}] : S^{'} \Rightarrow U^{'}

FPr-Cons

For a cast descriptor, the charge is $χ (T, S) : = {\begin{cases} 3 & T = ? and S is neither unknown nor ground, \\ 3 & S = ? and T is neither unknown nor ground, \\ 1 & otherwise . \end{cases}$ The total cast weight $cw (a)$ is structural: constants, variables, and blame contribute zero; abstraction takes its body’s weight; application adds both subterm weights; and $cw (⟨ T \Leftarrow S ⟩^{p} a) = χ (T, S) + cw (a) .$ With $| a |$ the syntax-tree size, the stutter measure is $st (a) = (cw (a), | a |) \in N \times N$ in lexicographic order. Total weight includes descriptors in waiting arguments and beneath values, so a change of the next-redex position cannot increase the measure after an administrative cast contraction.

Separate dependent-interoperability card.

The SD comparison has a simply typed component $s : S$ , a dependently typed component $t : T$ , compatibility $S ⟺ T$ , and boundaries ${SD}_{S}^{T} (t) : S, {DS}_{T}^{S} (s) : T .$ For paired constructor declarations $C : S_{1} \to A$ and $C : (y : T_{1}) \to B t_{1}$ , the constructor-specific roots are ${SD}_{A}^{B t} (C v) ⟶_{SD} C u if {argToS}_{C} (v) = u,$ and ${DS}_{B t}^{A} (C u) ⟶_{SD} (t \tilde{=} [v / y] t_{1}) ▹ C v if {argToD}_{C} (u) = v .$ The guard returns its payload when the two closed first-order indices are equal and $error$ otherwise. Call-by-value contexts descend into boundary operands. This card is the signature of definition 23.53; it adds no rule to the gradual cast calculus above.