Towards Generic Programming with Sized Types

Termination of Generic Programs

Andreas Abel July 3, 2006 MPC’06, Kurressaare, Estonia

Teaser

Termination of Higher-Order Functions

• Recursive function applied to arguments:

f(x) = … f(a) … f(b) …

• Check that a < x, b < x.

• What about a function passed to its argument?

f(g) = … g(f) …

• How to establish termination of f?? Generic Programs and Termination

• Typical generic program: traversal

• Observation: structurally recursive

• How to substantiate this observation?

• Are all generic programs total on total input?

• Are all generic programs even primitive recursive (catamorphisms)? Outline

Contents

1 Example: Generic Finite Maps 2

2 Termination via Sized Types 3

3 Generic Programming (Romanticism) 4

4 Generic Programming with Sized Types 6

1 Example: Generic Finite Maps

Finite Maps for List-shaped Keys

• R. Hinze (JFP 2000): Generalizing Generalized Tries

• Key type: [a], value type: v

data MapList f v
   = Leaf
   | Node (Maybe v) (f (MapList f v))

• If fw≅ a →_{fin} w, then MapListfv≅ [a] →_{fin} v.

• Looking up a list-shaped key:

lookupList :: (forall w. a -> f w -> Maybe w) ->
                [a] -> MapList f v -> Maybe v
lookupList lo l       Leaf         = Nothing
lookupList lo []      (Node mv m) = mv
lookupList lo (a:as) (Node mv m)
     = lo a m >>= lookupList lo as

Merging Finite Maps

• Merging (possibly undefined) values.

comb :: (v -> v -> v)
      -> Maybe v -> Maybe v -> Maybe v

• Merging finite maps:

mergeList ::
  (forall w. (w -> w -> w) -> f w -> f w -> f w)
  -> (v -> v -> v)
  -> MapList f v -> MapList f v -> MapList f v
mergeList mergeF c Leaf t = t

  mergeList mergeF c t Leaf = t
  mergeList mergeF c (Node m1 t1) (Node m2 t2) =
    Node (comb c m1 m2)
          (mergeF (mergeList mergeF c) t1 t2)

Termination of Merging

• Is mergeList terminating on all inputs?

  mergeList mergeF c (Node m1 t1) (Node m2 t2) =
    Node (comb c m1 m2)
          (mergeF (mergeList mergeF c) t1 t2)

• Consider:

  mf m t1 t2 = m (Node Nothing t1) (Node Nothing t2)
  run = mergeList mf fst (Node Nothing t1)
                            (Node Nothing t2)

• But: mf cannot be assigned the type

    forall w. (w -> w -> w) -> f w -> f w -> f w

2 Termination via Sized Types

Sized Inductive Types

• Type constructor

\frac{a : ord F : ∗ →^{+} ∗}{μ^{a}F : ∗}

• μ^{a+1}F = F (μ^{a}F).

• μ^{a}F contains trees of height < a.

• Semantically, a is an ordinal.

• Syntactically, a ::= ı + n | ∞.

Sized Lists • Example: List^{a}A = μ^{a}F where F X = 1 + A × X.

• List^{a}A contains lists of length < a.

• Definable data constructors:

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

Type-Based Termination

• Terminating recursion letrec f = t:

\frac{ı : ord, f : μ^{ı}F → C(ı) ⊢ t : μ^{ı+1}F → C(ı + 1)}{fix^{μ}(λf. t) : μ^{a}F → C(a)}

Analysis of Merging

Map⟨List⟩^{a} F V = μ^{a} (λX. 1 + (1 + V) × F X)
Bin V  = V → V → V
comb  : ∀V. Bin V → Bin (1 + V)
merge⟨List⟩  : ∀F. (∀W. Bin W → Bin (F W)) →
∀V. Bin V → ∀ı. Bin (Map⟨List⟩^{ı} F V)
merge⟨List⟩  := λmerge_{F} λc. fix^{μ} λmerge.
comb (λ(mv_{1}, t_{1})λ(mv_{2}, t_{2}).
(comb c mv_{1} mv_{2}, merge_{F} merge t_{1} t_{2}))

with

merge  : Bin (Map⟨List⟩^{ı} F V)
comb (λ …) : Bin (Map⟨List⟩^{ı+1} F V)
t_{1}, t_{2}  : F (Map⟨List⟩^{ı} F V)

3 Generic Programming (Romanticism)

Generic Programming (Romanticism)

• Kinds

κ ::= ∗ | κ → κ′

• Grammar of types

\begin{aligned}F, G & ::= & C | X | λX.F | F G | μF \\ C & ::= & 1 | + | × | Int | … \end{aligned}

• Data types definable

List : ∗ → ∗
List := λA. μ(λX. 1 + A × X)

Generic Equality

• Type of generic equality (kind-indexed type)

Eq⟨A:∗⟩  = A → A → Bool
Eq⟨F:κ → κ′⟩ = ∀G:κ. Eq⟨G:κ⟩ → Eq⟨F G:κ′⟩

• Instance: equality for lists

Eq⟨List:∗ → ∗⟩ = ∀A:∗. (A → A → Bool) →

(List A → List A → Bool)

Generic Equality

• Generic equality (type-indexed value) eq⟨F:κ⟩ : Eq⟨F:κ⟩

• User-defined clauses

eq⟨1:∗⟩ () ()  = true
eq⟨+:∗→∗→∗⟩ eqA eqB (inl a) (inl a′) = eqA a a′
eq⟨+:∗→∗→∗⟩ eqA eqB (inr b) (inr b′) = eqB b b′
eq⟨+:∗→∗→∗⟩ eqA eqB  = false
eq⟨×:∗→∗→∗⟩ eqA eqB (a, b) (a′, b′) = eqA a a′ && eqB b b′
eq⟨Int⟩ n n′  = n == n′

Generic Equality

• Hardwired clauses

eq⟨F G⟩ = eq⟨F ⟩ eq⟨G⟩
eq⟨λX.F ⟩ = λeqX .eq⟨F ⟩
eq⟨X⟩ = eqX
eq⟨μF ⟩ = fix eq⟨F ⟩

where fix f = f (fix f)

• Example

eq⟨List⟩ = eq⟨λA. μ(λX. 1 + A × X)⟩
= λeqA. fix (λeqX . eq⟨+⟩ eq⟨1⟩ (eq⟨×⟩ eqA eqX ))

• Recursive version eq⟨List⟩ eqA = eq⟨+⟩ eq⟨1⟩ (eq⟨×⟩ eqA (eq⟨List⟩ eqA))

Instantiating Generic Equality

• Type of eq⟨List⟩

Eq⟨List:∗ → ∗⟩ = ∀A:∗. (A → A → Bool) →

(List A → List A → Bool)

• Computing eq⟨List⟩

eq⟨List⟩ eqA (inl ()) (inl ())  = true
eq⟨List⟩ eqA (inr (a, x)) (inr (a′, x′)) = (eqA a a′)
&& (eq⟨List⟩ eqA x x′)

• Structurally recursive!

4 Generic Programming with Sized Types

Sized-Type Indexed Values

• Sized-Type Indexed Values

poly⟨C⟩  = user-defined
poly⟨X⟩  = x
poly⟨λıF : ord → κ⟩ = poly⟨F ⟩
poly⟨λXF : κ_{1} → κ_{2}⟩ = λx. poly⟨F ⟩  where κ_{1} ≠ ord
poly⟨F G⟩  = poly⟨F ⟩ poly⟨G⟩
poly⟨μ^{a}F ⟩  = fix^{μ} poly⟨F ⟩

Sized Type-Indexed Types

• Sized Type-Indexed Types

Type⟨C⟩ = user-defined for C ∈ {1, +, ×, Int, Char, … }
Type⟨X⟩  = X
Type⟨λXF ⟩ = λX. Type⟨F ⟩
Type⟨F G⟩ = Type⟨F ⟩ Type⟨G⟩
Type⟨μ^{a}F ⟩ = μ^{a} Type⟨F ⟩

Conclusions

Conclusions

• Sized types can certify termination for functions that are passed to their arguments

• Sized types interact well with:

– higher-order functions – rank-2 polymorphism

• Conjecture: (Romantic) generic grograms are structurally recursive • … from the perspective of sized types.