A Syntactic Model of

*Sized Dependent Types*

Jonathan Chan�University of British Columbia

18 July 2022

*MSc thesis: Sized Dependent Types via Extensional Type Theory

A Syntactic Model of

Sized Dependent Types

for stating and proving properties of programs within the language itself

A Syntactic Model of

Sized Dependent Types

for stating and proving properties of programs within the language itself

for checking validity of recursive functions

A Syntactic Model of

Sized Dependent Types

for stating and proving properties of programs within the language itself

for checking validity of recursive functions

for proving consistency of the type theory

Outline

for the next hour

• Crash course on dependent types
• Introduction to sized types
• How to model syntactically
• Shortcomings and future work

5

➀ Dependent types ≔

types that abstract over (“depend on”) terms & types

6

➀ :

The Curry–Howard Correspondence (1)

Type system

• dependent type theory
• types
• terms
• type checking

Logical system

• predicate logic
• propositions
• proofs
• automated proof checking

7

➀ :

The Curry–Howard Correspondence (2)

Type system

• Πx: A. B x
• ΠP: Prop. P (or ⊥)
• Π_: A. B (or A → B)
• A → ⊥
• ΠP: Prop. P → P (or ⊤)

Logical system

• for all x in A, B(x) holds
• falsehood
• A implies B
• negation of A
• truthhood

…and existential quantification, conjunction, disjunction, equality, etc.

8

➀ :

The Curry–Howard Correspondence (3)

Type system

There exists no term e of type ⊥

(not all types are inhabited)

Logical system

Logical consistency

(not all propositions are provable)

9

➀ :

Beyond Propositions

data nat: 𝒰 ≔� zero: nat� succ: nat → nat

​

fix _≤_: nat → nat → Prop�zero ≤ _ ≔ ⊤�succ n ≤ succ m ≔ n ≤ m�succ _ ≤ zero ≔ ⊥

Peano naturals (not a proposition)

Total order on nat (a proposition)

10

➀ :

Recursive Functions (1)

fix _≤_: nat → nat → Prop�zero ≤ _ ≔ ⊤�succ n ≤ succ m ≔ n ≤ m�succ _ ≤ zero ≔ ⊥

​

fix ng: ΠP: Prop. P�ng P ≔ ng P

11

➀ :

Recursive Functions (1)

✅ recursive call on�syntactic subargument

❌ recursive call on own argument

fix _≤_: nat → nat → Prop�zero ≤ _ ≔ ⊤�succ n ≤ succ m ≔ n ≤ m�succ _ ≤ zero ≔ ⊥

​

fix ng: ΠP: Prop → P�ng P ≔ ng P

12

➀ :

Recursive Functions (2)

fix monus: nat → nat → nat�monus n zero ≔ n�monus zero _ ≔ zero�monus (succ n) (succ m) ≔� monus n m

​

fix div: nat → nat → nat�div zero _ ≔ zero�div (succ n) m ≔� succ (div (monus n m) m)

monus(n, m) = max(0, n - m)

div(n, m) = ⌈n/(m+1)⌉

13

➀ :

Recursive Functions (2)

✅ recursive call on�syntactic subargument

❌ recursive call on function call on�syntactic subargument

fix monus: nat → nat → nat�monus n zero ≔ n�monus zero _ ≔ zero�monus (succ n) (succ m) ≔� monus n m

​

fix div: nat → nat → nat�div zero _ ≔ zero�div (succ n) m ≔� succ (div (monus n m) m)

14

➀ :

② Sized types ≔�inductive types annotated�with constr. depth (“size”)

15

② :

Sized Types

data nat [s]: 𝒰 ≔� zero: ∀ α < s. nat [s]� succ: ∀ α < s. nat [α] → nat [s]

16

additional size information

larger size

② :

Sized Types

data nat [s]: 𝒰 ≔� zero: ∀ α < s. nat [s]� succ: ∀ α < s. nat [α] → nat [s]

fix monus: ∀α. ∀β. nat [α] → nat [β] → nat [α]

fix div: ∀α. ∀β. nat [α] → nat [β] → nat [α]�div [α] [β] (zero [γ]) _ ≔ zero [γ]�div [α] [β] (succ [γ] n) m ≔� succ [γ] (div [γ] [β] (monus [γ] [β] n m) m)

17

② :

Sized Types

data nat [s]: 𝒰 ≔� zero: ∀ α < s. nat [s]� succ: ∀ α < s. nat [α] → nat [s]

fix monus: ∀α. ∀β. nat [α] → nat [β] → nat [α]

fix div: ∀α. ∀β. nat [α] → nat [β] → nat [α]�div [α] [β] (zero [γ]) _ ≔ zero [γ]�div [α] [β] (succ [γ] n) m ≔� succ [γ] (div [γ] [β] (monus [γ] [β] n m) m)

18

recursion on smaller size γ < α

② :

Sized Recursive Functions (Fixpoint Expressions)

α ⊢ τ : 𝒰�α; f: ∀β < α. τ[α ↦ β] ⊢ e : τ�───────────────────────────────�⊢ fix f [α]: τ ≔ e : ∀α. τ

19

② :

Past Work on Sized Dependent Types

20

② :

Past Work on Sized Dependent Types

21

② :

Bounded sizes: ∀α < s. τ

• Elegant interpretation of fixpoint expressions
• Otherwise: fixpoint types must be “semi-continuous” in recursion size
• Implemented in Agda

Past Work on Sized Dependent Types

22

② :

Higher-rank sizes: (∀α. σ) → τ

• Greater expressivity
• Can pass around size-preserving functions
• Implemented in Agda

Past Work on Sized Dependent Types

(∀ α. σ) → τ

∀ α < s. τ

⊬ e : ⊥

23

② :

③ Syntactic model ≔�type-preserving translation

into a consistent language

24

③ :

Translation from STT to Target Type Theory

Φ; Γ ⊢ e : τ ⇝ e : typing derivation → term

⟦e⟧ : (well-typed) term → term

25

③ :

Type Preservation and Consistency

Recall: ⊥ ≔ ΠP: Prop. P

• Postulate (consistency).�There is no term e such that ⊢ e : ⊥.
• Theorem (type preservation).�If Φ; Γ ⊢ e : τ ⇝ e, then ⟦Φ⟧,⟦Γ⟧ ⊢ e : ⟦τ⟧.
• Corollary (consistency).�There is no term e such that ⊢ e : ⊥.�Proof: If ⊢ e : ⊥, then ⊢ ⟦e⟧ : ⊥ by type preservation,�contradicting consistency.

26

③ :

Translation Details

Terms in STT

Size expressions

Order on sizes

Fixpoints on sizes

Terms in CIC_E

Elements of inductive type Size

_<_: Size → Size → Prop

Uses of well-founded induction on�Size, <

27

translate to

⟿

③ :

…Well-Founded Induction Principle

wfInd : ΠP: Size → 𝒰.� Let P be a predicate on Sizes.

(Πα: Size. (Πβ: Size. β < α → P β) → P α)� Given that P holds for every β strictly smaller than some α,� if I can show that P holds for α…

→� Πα: Size. P α� …then P holds for any α.

28

③ :

Fixpoints…

α ⊢ P α : 𝒰� Let P be a predicate on sizes.

α; f: ∀β < α. P β ⊢ e : P α� Given that P holds for every β strictly smaller than some α,� if I can show that P holds for α…

───────────────────────────────� ⊢ fix f [α]: P α ≔ e : ∀α. P α� …then P holds for any α.

29

③ :

Fixpoints are a Well-Founded Induction Principle

⟦fix f [α]: τ ≔ e⟧ =

wfInd (λα: Size. ⟦τ⟧)� (λα: Size. λf: (Πβ: Size. β < α → ⟦τ⟧[α ↦ β]). ⟦e⟧)

30

③ :

More Technical Details

• Accessibility predicate w.r.t. size order�data Acc (α: Size): Prop where� acc: (∀β: Size. β < α → Acc β) → Acc α
• Well-foundedness of sizes�fix wf: Πα: Size. Acc α
• Proof-irrelevance of accessibility�α: Size, acc₁: Acc α, acc₂: Acc α ⊢ acc₁ ≡ acc₂ : Acc α
• Preservation of fixpoint reduction�⊢ ⟦(fix f [α]: τ ≔ e) [s]⟧ ≡� ⟦e[α ↦ s][f ↦ Λβ < s. (fix f [α]: τ ≔ e) [β]⟧ : ⟦∀α. τ⟧

31

③ :

Inconsistent Infinity

If STT has:

+ ∞

⊢ s� + ───────� ⊢ s ≤ ∞

⟹ ⊢ ∞ < ∞

​

∴ STT must not have ∞!

Then CIC_E would have:

let ∞<∞ : ⟦∞⟧ < ⟦∞⟧

fix ¬wf∞: Acc ⟦∞⟧ → ⊥�¬wf∞ (acc p) ≔ p ⟦∞⟧ ∞<∞

let ng: ⊥�ng ≔ ¬wf∞ (wf ⟦∞⟧)

​

∵ Inconsistent!

32

③ :

➃ Shortcomings and

Future Work

33

➃ :

Problem 1: Limited Size Expressions

fix add: ∀α. ∀β. nat [α] → nat [β] → nat [?]�add [α] [β] (zero [α’]) n ≔ ⟨α, zero [_]⟩�add [α] [β] m (zero [β’]) ≔ ⟨β, zero [_]⟩�add [α] [β] (succ [α’] n) (succ [β’] m) ≔� let ⟨γ, sum⟩ ≔ add [α’] [β’] n m� in ⟨γ+2, succ [ _ ] (succ [_] sum)⟩

• ? = ∞ (since _ < ∞; but inconsistent!)
• ? = α + β (when does it end? α × β? α^β? α!? f [α] [β] for any f??)

34

➃ :

Solution 1: Existentially-Quantified Sizes

fix add: ∀α. ∀β. nat [α] → nat [β] → ∃γ. nat [γ]�add [α] [β] (zero [α’]) n ≔ ⟨α, zero [α’]⟩�add [α] [β] m (zero [β’]) ≔ ⟨β, zero [β’]⟩�add [α] [β] (succ [α’] n) (succ [β’] m) ≔� let ⟨γ, sum⟩ ≔ add [α’] [β’] n m� in ⟨γ+2, succ [γ+1] (succ [γ] sum)⟩

• ? = ∞ (since _ < ∞; but inconsistent!)
• ? = α + β (when does it end? α × β? α^β? α!? f [α] [β] for any f??)
• ? = …it doesn’t matter as long as it has some size!

35

➃ :

Problem 2: Infinitary Inductives

data ord [s]: 𝒰 ≔� zero: ∀α < s. ord [s]� succ: ∀α < s. ord [α] → ord [s]� lim: ∀α < s. (∃β. nat [β] → ord [α]) → ord [s]

fix natToOrd: ∃β. nat [β] → ∃α. ord [α]�natToOrd [β] (zero [β’]) ≔ ⟨β, zero [β’]⟩�natToOrd [β] (succ [β’] n) ≔ succ (natToOrd n)� [α] x⟩

let ω: ∃α. ord [α]�ω ≔ ⟨?+1, lim [?] (Λβ. λn. let ⟨α, m⟩ ≔ natToOrd [β] n in m)⟩

36

➃ :

Problem 2: Infinitary Inductives

data ord [s]: 𝒰 ≔� zero: ∀α < s. ord [s]� succ: ∀α < s. ord [α] → ord [s]� lim: ∀α < s. (∀β. nat [β] → ord [α]) → ord [s]

fix natToOrd: ∀β. nat [β] → ∃α. ord [α]�natToOrd [β] (zero [β’]) ≔ ⟨β, zero [β’]⟩�natToOrd [β] (succ [β’] n) ≔� let ⟨α, x⟩ ≔ natToOrd [β’] n in ⟨α+1, succ [α] x⟩

let ω: ∃α. ord [α]�ω ≔ ⟨?+1, lim [?] (Λβ. λn. let ⟨α, m⟩ ≔ natToOrd [β] n in m)⟩

37

➃ :

Solution 2: ???

let ac: (τ → ∃α. σ [α]) → ∃α. (τ → σ [α])� ⤷ requires size projection (bad) and limit sizes (worse) to implement��

���

let ω: ∃α. ord [α]�ω ≔ let ⟨α, f⟩ ≔ ac natToOrd in ⟨α+1, lim [α] f⟩

38

➃ :

Future Work: Missing Features and Properties

• Inductives in general (only ℕ, 𝕎):� straightforward, tedious, no new insights
• Coinductives:� straightforward source extension,� suspicious target translation
• Normalization wrt reduction,�decidability of type checking:� conjectured (doesn’t follow from model)
• Infinitary constructs (lack of ∞)

39

➃ :

Summary

of contributions

1. Explicit, higher-rank, bounded sized dependent type theory
2. Syntactic model for sized types and proof of consistency

40

➃ :

⑤ Questions?

41

⑤ :