Polarized Subtyping for Sized Types

Andreas Abel

Computer Science Symposium Russia June 10, 2006

Outline

Contents

1 Applications of Subtyping 1 1.1 Type-Based Termination . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Subtyping Collections . . . . . . . . . . . . . . . . . . . . . . . . . . 2

2 Polarized Subtyping 3 2.1 Types as λ-Expressions . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.2 Kinds and Polarities . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.3 Equality and Subtyping . . . . . . . . . . . . . . . . . . . . . . . . . 4

3 Algorithmic Subtyping 4

4 Completeness through Cut-Elimination 5

5 Conclusion 6

1 Applications of Subtyping

1.1 Type-Based Termination

Type-Based Termination

• Termination for higher-order functional programs.

• Recursive function definition:

f : ∀i. List^{i} A → B
f (x : List^{i+1} A) = … (f : List^{i} A → B)(e) …
… g(f : List^{i} A → B) …

• Sized type: List^{i} A contains lists of length < i.

• Subtyping: List^{i} A ≤ List^{i+1} A ≤ ⋯ ≤ List^{∞} A.

1.2 Subtyping Collections

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}

Unsound subtyping in JAVA This code passes type-checking.

  void init(Object[] a) {
      a[0] = new Object();

}

  void main() {
      Integer[] a = new Integer[1];
      init(a);
      print(a[0].intValue());

}

But throws ArrayStoreException!

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}

2 Polarized Subtyping

2.1 Types as λ-Expressions

Types as λ-Expressions

• Creating type constructors by abstraction: λX.F

• Application of a type constructor

F G

• Representation of ∀A. A → List A ∀ (λA. ((→) A (List A)))

• Equations

(β) (λX.F) G = [G/X]F
(η) λX. (F X) = F  if X does not appear in F

2.2 Kinds and Polarities

Polarized F^{ω}

• Type constructors

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

• Kinds

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

• Polarities

p ::= ∘ | + | −

• Assign kinds, e.g., to constants C:

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

Polarized Kinding

• Polarized contexts

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

• Polarized kinding

Γ ⊢ F : κ

• E.g.,

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

X:−∗,

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

2.3 Equality and Subtyping

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}

3 Algorithmic Subtyping

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 G⃗ | X G⃗  neutral (atomic)
W ::= N | λX.F  weak head normal

• Weak head evaluation (β-steps)

F ↘ W

• Kind-directed algorithmic subtyping

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

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′ ⇉ κ′}

4 Completeness through Cut-Elimination

Completeness of Algorithmic Subtyping Show: 2 kinds of cuts are admissible.

1. Transitivity (easy inductive proof)

\frac{Γ ⊢ F_{1} ≤ F_{2} ⇇ κ Γ ⊢ F_{2} ≤ F_{3} ⇇ κ}{Γ ⊢ F_{1} ≤ F_{3} ⇇ κ}

2. Application (non-trivial)

\frac{Γ ⊢ F ≤ F′ ⇇ κ →^{+} κ′ Γ ⊢ G ≤ G′ ⇇ κ}{Γ ⊢ F G ≤ F′ G′ ⇇ κ}

3. Proof alternatives: (a) From strong normalization (Aspinall Hofmann 2005; Goguen 2005)

(b) Kripke-Model (e.g., Harper Pfenning 2004)

(c) Direct, syntactically

Towards a Direct Proof of Application • Propositional sequent calculus: structural proof of cut elimination.

• Transfer to implicational natural deduction:

1. Kinds = implicational propositions.

2. Application of constructors = modus ponens.

3. Substitution = cut elimination.

Adaption of Cut Elimination

Application is a direct consequence of: Lemma 1 (Substitution). If Γ, X: +κ ⊢ F ≤ F′ ⇇ κ′ and Γ ⊢ G ≤ G′ ⇇ κ, then Γ ⊢ [G/X]F ≤ [G′/X]F′ ⇇ κ′. Proof. By lexicographic induction on κ and size of the first derivation.

5 Conclusion

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

• Polarities arise naturally when subtyping constructors • Idea of algorithm: apply down to base kind

• Direct and short completeness proof

• Next: extend to bounded quantification