Implementing a Normalizer Using Sized Heterogeneous Types

Normalization of λ-Terms by Structural Recursion

Andreas Abel Mathematically Structured Functional Programming Kuressaare, Estonia, July 2, 2006

Outline

Contents

1 Introduction 1 2 The Meta-Language: F_{ω} 2 3 The Object Language: STL 3 4 De Bruijn Implementation 5 5 Conclusion 7

1 Introduction

Interpreters • Turing-complete Language L: can implement its own interpreter.

• What meta-language ML is required to interpret a total (=terminating) language L?

• ML should also be total.

• Here: L = simply-typed λ-calculus

• ML = F_{ω}, a functional programming language with sized types

• Termination can be ensured by the type-checker!

2 The Meta-Language: F_{ω}

The meta-language: F_{ω} • Pure functional language (no assignments, pointers, I/O)

• Higher-order functions

• Impredicative polymorphism

• Sized recursive types of higher-kind

• Recursion, restricted; termination guaranteed by type system

• Corecursion, restricted: productivity guaranteed by type system

• Mathematical structure: ordinals, transfinite induction Sized types, semantically

• Recursive types defined from below by transfinite iteration.

• Example: List A = μ^{ω}F

• F X = {nil, cons a as | a ∈ A, as ∈ X}

• Transfinite Iteration:

\begin{aligned}μ^{0}F & = & ∅ \\ μ^{α+1}F & = & F (μ^{α}F) \\ μ^{λ}F & = & ⋃_{α<λ} μ^{α}F \end{aligned}

• F monotone: μ^{α}F ⊆ μ^{β}F for α ≤ β.

• Sized type: List^{α}A = μ^{α}F. Sized types, syntactically

• Data types are equipped with a size index (upper bound)

• E.g., List^{ı} A denotes lists of length < ı with elements in A

• Constructors (polymorphic):

nil : ∀ı∀A. List^{ı+1}A
cons : ∀ı∀A. A → List^{ı} → List^{ı+1} A

• Size expressions must have the form ı + n (ı size variable, n natural number) or ∞ (unbounded size).

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

Recursion over sized types, semantically

• Prove that fix s = s (fix s) ∈ A(β) by transfinite induction on β.

1. Base: fix s ∈ A(0) (bottom-check)

2. Step: fix s ∈ A(α) implies fix s ∈ A(α + 1)

3. Limit: fix s ∈ A(λ) if fix s ∈ A(α) for all α < λ.

• Proof skeleton:

1. Base: holds e.g., for A(α) = List^{α}B → C.

2. Step: holds if s ∈ A(α) → A(α + 1).

3. Limit: holds for upper-semicontinuous A [CSL 06].

Recursion over sized types, syntactically • Recursion restricted to this pattern:

\begin{matrix}f : ∀ı.A(ı) → C(ı) \\ f(x : A(ı + 1)) = \begin{matrix}(… f(t : A(ı)) … \\ … g(f : A(ı) → C(ı)) …) : C(ı + 1) \end{matrix} \end{matrix}

• Termination of recursion ensured by types.

• Example:

filter : ∀ı∀A. (A → Bool) → List^{ı}A → List^{ı}A filter p nil = nil filter p (cons a as : List^{ı+1}A) =

if p(a) then cons a (filter p (as : List^{ı}A)) else filter p (as : List^{ı}A)

3 The Object Language: STL

The Simply-Typed λ-Calculus

• An even purer functional language (no data types, no recursion, no polymorphism)

• Programs consist of functions and application.

r, s, t ::= x  variable
| λx:a.t  abstraction of x in t
| r s  application

• Types:

a, b, c ::= o  base type
|  a → b  function type

Computation in STL

• Only reduction rule:

(λx:a.t) s ⟶ [s/x]t

• Example:

(λx:((o → o) → (o → o)). x (λz:o.z)) (λy:(o → o). y)
⟶ [(λy:(o → o). y)/x](x (λz:o.z))
= (λy:(o → o). y) (λz:o.z)
⟶ [(λz:o.z)/y]y = λz:o.z

• Normal form v ::= λx:a.v | x v_{1} … v_{n}. A Big-Step Interpreter for STL

• For term t, [[t]] computes its normal form.

[[x]]  = x
[[λx:a.r]] = λx:a. [[r]]
[[r s]]  = [[[s]]^{a}/x]t if [[r]] = λx:a.t
[[r]] [[s]]  otherwise

• Substitution [[[s]]^{a}/x]t of one normal form s into another normal form t may

trigger new reductions. Hereditary Substitutions

• Normalizing substitution of normal forms: [s^{a}/x]t

[s^{a}/x]x  = s^{a}
[s^{a}/x]y = y if x ≠ y
[s^{a}/x](λy:b.r) = λy:b. [s^{a}/x]r where y fresh for s, x
[s^{a}/x](t u) = ([û^{b}/y]r′)^{c} if t̂= (λy:b′.r′)^{b→c}
t̂û  otherwise
where t̂ = [s^{a}/x]t
û = [s^{a}/x]u

• Invariant: |b → c| ≤ |a| in line 4.

What is happening in hereditary substitutions? • In [s^{a}/x]t, size of type |a| is “fuel”.

• As long as there is fuel, new her. substitutions can be performed.

• Each new substitution starts with less fuel.

• E.g. [w^{a→b→c}/x](x v_{1} v_{2})

• Possibly new subst. of v_{1} into w: fuel = |a|.

• Substitution of v_{2} into the result: fuel = |b|.

• [s^{a}/x]t terminates by lexicographic order (|a|, |t|). What happens for ill-typed terms?

• [s^{a}/x]t also terminates for ill-typed or non-normal s, t.

• But fuel might run out before normal form is reached.

• Result might be non-normal form.

• Example:

[[(λx:(o → o). x x) (λx:o. x x)]]
⟶ [(λx:o. x x)^{o→o}/x](x x)
⟶ (λx:o. x x)^{o→o} (λx:o. x x)^{o→o}
⟶ [(λx:o. x x)^{o}/x](x x)
⟶ (λx:o. x x)^{o} (λx:o. x x)^{o}

4 De Bruijn Implementation

Representation of STL in F_{ω}

• STL-types represented as a sized type.

o : Ty^{ı+1}
arr : Ty^{ı} → Ty^{ı} → Ty^{ı+1}

• If a : Ty^{ı} then |a| < ı.

• STL-terms represented by nested data type Tm^{ı} A:

var : A → Tm^{ı+1} A
app : Tm^{ı} A → Tm^{ı} A → Tm^{ı+1} A
abs : Ty^{∞} → Tm^{ı} (1 + A) → Tm^{ı+1} A

• Tm^{ı} A contains terms of height < ı with free variables in A.

Results of hereditary substitution

• Result of a hereditary substitution can either be a term with remaining fuel or a

term with no fuel.

Res^{ı} A = Tm^{∞} A × (1 + Ty^{ı})
ne_{Res} : Tm^{∞} A → Res^{ı} A
nf_{Res} : Tm^{∞} A → Ty^{ı} → Res^{ı} A

• Extracting the term from a result:

tm : Res^{ı}A → Tm^{∞} A

Simultaneous hereditary substitutions

• For TmA, only simultaneous substitution

TmA → (A → TmB) → TmB

is directly definable.

• Valuations for all variables:

Val^{ı}A B = A → Res^{ı}B

sg_{Val} : Tm^{∞}A → Ty^{ı} → Val^{ı} (1 + A) A
lift_{Val} : Val^{ı} A B → Val^{ı} (1 + A) (1 + B)

The F_{ω} -Code subst : ∀ı. Ty^{ı} → ∀A. Tm^{∞} A → Tm^{∞}(1 + A) → Tm^{∞} A

subst a s t = tm (simsubst t (sg_{Val} s a))

where simsubst : ∀ȷ. ∀A∀B. Tm^{ȷ}A → Val^{ı+1} A B → Res^{ı+1}B

simsubst t ρ = match t with

var x ↦ ρ x
abs b r ↦ abs_{Res} b (simsubst r (lift_{Val} ρ))
app t u ↦ let t̂ = simsubst t ρ û = simsubst u ρ
in match t̂with

nf_{Res} (abs b′ r′) (arr b c)

↦ nf_{Res} (subst b (tm û) r′) c ↦ app_{Res} t̂û

5 Conclusion

Conclusion • A natural implementation of a normalizer

• Structurally recursive

• Termination statically ensured by the type system • Host language: F_{ω} (but ML-Polymorphism sufficient)

• Slogan:

In each recursive program there is a structurally recursive one struggling to get out.—Conor McBride