Higher-Order Subtyping, Revisited

Syntactic Completeness Proofs for Algorithmic Judgements

Andreas Abel TYPES Workshop, April 21, 2006

Contents 1. Subtyping for type constructors (F^{ω})

2. Proof Technique for Metatheory • Elementary (no model)

• Works for weak theories: STL, LF

1 Higher-Order Subtyping

Subtyping for Collections

• When a Float is expected, an Int is acceptable.

Int ≤ Float

• Read-only collections: a list of Ints passes for a list of Floats. \frac{Int ≤ Float}{List Int ≤ List Float}

• Mutable collections: cannot store a Float into an Int cell.

not \frac{Int ≤ Float}{Array Int ≤ Array Float}

Subtyping and Variance

• Distinguish type constructors by their variance

Array : ∗ →^{∘} ∗  mixed-variant
List : ∗ →^{+} ∗  covariant
Sink : ∗ →^{−} ∗  contravariant

• Subtyping applications:

\frac{F : ∗ →^{∘} ∗ A = B}{F A ≤ F B}

\frac{F : ∗ →^{+} ∗  A ≤ B}{F A ≤ F B}  \frac{F : ∗ →^{−} ∗  B ≤ A}{F A ≤ F B}

Polarized F^{ω}

• Polarities

p ::= ∘ | + | −

• Kinds

κ ::= ∗ | κ →^{p} κ′

• Type constructors

F, G ::= C | X | λX.F | F G

• Constants C, e.g.,

\begin{aligned}× & : & ∗ →^{+} ∗ →^{+} ∗ \\ → & : & ∗ →^{−} ∗ →^{+} ∗ \\ ∀_{κ} & : & (κ →^{∘} ∗) →^{+} ∗ \end{aligned}

Polarized Kinding

• Polarized contexts

Γ ::= ⋄ | Γ, X:pκ

• Polarized kinding

Γ ⊢ F : κ

• E.g.,

F:∘(∗ →^{+} ∗),

X:−∗,

Y :+∗  ⊢ F X → F Y : ∗

Declarative Equality and Subtyping

• Judgements

Γ ⊢ F = F′ : κ  βη-equality
Γ ⊢ F ≤ F′ : κ  polarized subtyping

• Subtyping axioms, e.g., Γ ⊢ Array ≤ List : ∗ →^{+} ∗.

• Axioms for β and η.

• Reflexivity, transitivity, (anti)symmetry.

• Closure under abstraction and application.

\begin{matrix}Γ ⊢ F : κ →^{+} κ′ \\ Γ ⊢ G ≤ G′ : κ \\ Γ ⊢ F G ≤ F G′ : κ′ \end{matrix}  \begin{matrix}Γ ⊢ F : κ →^{∘} κ′ \\ Γ ⊢ G = G′ : κ \\ Γ ⊢ F G = F G′ : κ′ \end{matrix}

Algorithmic Subtyping

• Judgement for algorithmic subtyping Γ ⊢ F ≤ F′ ⇇ κ

• Steps

Array ≤ (λX. List X) ⇇ ∗ →^{+} ∗ apply down to kind ∗:
Array Y ≤ (λX. List X) Y ⇇ ∗  weak head normalize:
Array Y ≤ List Y ⇇ ∗ compare heads (axiom):
Array ≤ List : ∗ →^{+} ∗  continue with arguments:
Y ≤ Y ⇇ ∗

Kind-directed Algorithmic Subtyping

• Weak head normal forms

N ::= C | X | N G  neutral (atomic)
W ::= N | λXF  weak head normal

• Weak head evaluation

F ↘ W

• Kind-directed algorithmic subtyping

Γ ⊢ F ≤ F′ ⇇ κ checking mode
Γ ⊢ N ≤ N′ ⇉ κ inference mode

• (Analogously for algorithmic equality) Rules for Algorithmic Subtyping

• Checking mode

\frac{Γ, X:pκ ⊢ F X ≤ F′ X ⇇ κ′}{Γ ⊢ F ≤ F′ ⇇ pκ → κ′}

\frac{F ↘ N  F′ ↘ N′  Γ ⊢ N ≤ N′ ⇉ ∗}{Γ ⊢ F ≤ F′ ⇇ ∗}

• Inference mode: Axioms +

\frac{(X:pκ) ∈ Γ p ∈ \{∘, +\}}{Γ ⊢ X ≤ X ⇉ κ}

\frac{Γ ⊢ N ≤ N′ ⇉ +κ → κ′ Γ ⊢ G ≤ G′ ⇇ κ}{Γ ⊢ N G ≤ N′ G′ ⇉ κ′}

Completeness of Algorithmic Subtyping • Soundness of algorithmic judgements easy

• Transitivity, (anti)symmetry easy

• Completeness hard: Closure under application?

• Alternatives:

1. From strong normalization (Aspinall Hofmann 2005; Goguen 2005)

2. Model (e.g., Harper Pfenning 2004)

3. Direct, syntactically From a Bird’s Perspective

• Type language of F^{ω} is weak (no recursion)

• Roughly simply-typed λ-calculus

• Proof theory says: there is an elementary meta theory

• How to construct this elementary proof?

• Technical skill required Main Lemma: Application and Substitution

• Let Γ ⊢ G ≤ G′ ⇇ κ. Prove simultaneously: 1. If Γ ⊢ F ≤ F′ ⇇ +κ → κ′ then Γ ⊢ F G ≤ F′ G′ ⇇ κ′.

2. If Γ, X:+κ ⊢ N ≤ N′ ⇉ κ′ then

– either Γ ⊢ [G/X]N ≤ [G/X]N′ ⇉ κ′,
– or Γ ⊢ [G/X]N ≤ [G/X]N′ ⇇ κ′ and |κ′| ≤ |κ|.

3. If Γ, X:+κ ⊢ F ≤ F′ ⇇ κ′ then Γ ⊢ [G/X]F ≤ [G′/X]F′ ⇇ κ′.

• Lexicographic induction on |κ| and derivation length.

2. Case N = N′ = Y ≠ X. Case N = N′ = X. Case

\frac{Γ ⊢ M ≤ M′ ⇉ +κ′′ → κ′ Γ ⊢ H ≤ H′ ⇇ κ′′}{Γ ⊢ M H ≤ M′ H′ ⇉ κ′}

Consequences and Evaluation Consequences of Main Lemma:

• Closure under β and application.

• Reflexivity.

• Completeness. Evaluation of proof:

• Short, direct

• Purely syntactical

• Avoiding logical relations and models

• Well-suited for formalization (e.g., in Twelf)

Applicability of Proof Technique • Normalization of simply-typed lambda-calculus (Joachimski Matthes 2003)

• Algorithmic equality for LF

• Other logical frameworks (LLF, CLF)

• Predicative polymorphism!?

• Languages of low proof-theoretical complexity

• POPLmark challenges

• Limitations – Impredicativity

– Inductive types Related Work

• Cut elimination for FOL

• Troelstra 1973: Syntactical normalization proof

• Joachimski Matthes 2003: λ + permutative conversions • Hereditary substitutions:

– Watkins Cervesato Pfenning Walker 2003: Concurrent LF

– Nanevski Pfenning Pientka 2005: Contextual Modal Type Theory – Adams (PhD 2005): λ-free LF

• Goguen 1995-2005: Typed Operational Semantics Conclusions

• Purely syntactical approach to meta theory

• Does not work for CC or inductive types

• But applicable to many logical frameworks

• Proofs suited for formalization (HOAS)

• Should be in your tool box!