Sized (Co-)Inductive Types

With Applications to Generic Programming

Andreas Abel

ProgLog Seminar, April 5, 2006

1 Example: Generic Finite Maps

Finite Maps for List-shaped Keys

• 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 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

Sized Inductive Types

• Type constructor μ : ord →^{+} (∗ →^{+} ∗) →^{+} ∗.

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

• Finite maps:

Map⟨List⟩  : ord →^{+} (∗ →^{+} ∗) →^{+} ∗ →^{+} ∗
Map⟨List⟩^{a} F V = μ^{a} (λX. 1 + (1 + V) × F X)

• Terminating recursion

\frac{s : ∀ı. (μ^{ı}F → C) → μ^{ı+1}F → C}{fix^{μ} s : μ^{a}F → C}

Analysis of Merging

• Auxiliary definitions:

Map⟨List⟩^{a} F V = μ^{a} (λX. 1 + (1 + V) × F X)
Bin  : ∗ →^{∘} ∗
Bin  := λV. V → V → V
comb  : ∀V. Bin V → Bin (1 + V)

• Merging, formalized:

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

2 Iso- and Equi-(Co)inductive Types

Iso-Inductive Types • Principle: μ^{a+1} F is isomorphic to F (μ^{a} F).

• Size-level equality:

∞ + 1 = ∞

• Introduction:

\frac{t : F (μ^{a} F)}{in t : μ^{a+1}F}

• Elimination:

\frac{t : μ^{a+1}F}{out t : F (μ^{a} F)}  \frac{s : ∀ı. (μ^{ı}F → C) → μ^{ı+1}F → C}{fix^{μ} s : μ^{a}F → C}

• Reductions:

out (in t) ⟶ t
fix^{μ} s (in t) ⟶ s (fix^{μ} s) (in t)

Iso-Coinductive Types • Principle: ν^{a+1} F is isomorphic to F (ν^{a} F).

• Size-level equality:

∞ + 1 = ∞ • Introduction:

\frac{t : F (ν^{a} F)}{in t : ν^{a+1}F}  \frac{s : ∀ı. (A_{1..n} → ν^{ı} F) → A_{1..n} → ν^{ı+1}F}{fix_{n}^{ν} s : A_{1..n} → ν^{a}F}

• Elimination:

\frac{t : ν^{a+1}F}{out t : F (ν^{a} F)}

• Reductions:

out (in t)  ⟶ t
out (fix_{n}^{ν} s t_{1..n}) ⟶ out (s (fix_{n}^{ν} s) t_{1..n})

Equi-Inductive Types • Principle: μ^{a+1} F = F (μ^{a} F) as type-level equality.

• Deep (un)folding.

• No tagging on the term level.

• No native introduction/elimination principles.

• Recursion:

\frac{s : ∀ı. (μ^{ı}F → C) → μ^{ı+1}F → C}{fix^{μ} s : μ^{a}F → C}

• Reduction:

fix^{μ} s v ⟶ s (fix^{μ} s) v

• Values: v ::= λxt | (r, s) | inl r | inr r | …

Equi-Coinductive Types • Principle: ν^{a+1} F = F (ν^{a} F) as type-level equality.

• Corecursion:

\frac{s : ∀ı. (A_{1..n} → ν^{ı} F) → A_{1..n} → ν^{ı+1}F}{fix_{n}^{ν} s : A_{1..n} → ν^{a}F}

• Reduction:

e(fix_{n}^{ν} s t_{1..n}) ⟶ e(s (fix_{n}^{ν} s) t_{1..n})

• Elimination frames:

e(_) ::= _s | fst _| snd _| case _… Embedding Iso into Equi

• μ_{iso}^{a} (λX.A) := μ^{a} (λX. 1 → A).

• in t := λ_.t

• out t := t ()

• Note: in t is translated into a value

• out _is translated into an evaluation frame

• Reductions are simulated:

out (in t)  ⟶ t
fix^{μ} s (in t)  ⟶ s (fix^{μ} s) (in t)
out (fix_{n}^{ν} s t_{1..n}) ⟶ out (s (fix_{n}^{ν} s) t_{1..n})

Non-Confluence • Recursive evaluation frame e(_) = fix^{μ} s _.

• Corecursive value v = fix_{n}^{ν} s t_{1..n}

• Critical term: s = λzλx.x and [2ex] \begin{matrix}fix^{μ} s (fix_{0}^{ν} s) \\ s (fix^{μ} s) (fix_{0}^{ν} s) \\ (λx.x) (fix_{0}^{ν} s) \\ fix_{0}^{ν} s \\ fix^{μ} s (s (fix_{0}^{ν} s)) \\ fix^{μ} s (λxx) \\ s (fix^{μ} s) (λxx) \\ λxx \end{matrix}

Avoiding Non-Confluence • Consider fix^{μ} s (fix_{0}^{ν} s) blocked (unfold neither recursion nor corecursion).

• Drawback: there are closed, blocked terms.

• Consolidation: arise only for unguarded types like μ(λX.ν(λY.A)).

• Speculative: unfold recursion and corecursion simultaneously.

3 Models and Strong Normalization

Modelling Sized Types (Iso)

• A := [[A]] is a saturated set of strongly normalizing terms.

• [[A → B]] = {r | r s ∈ [[B]] for all s ∈ [[A]].

• A^{μ} = \overline{\{in t | t ∈ A\}}

• A^{ν} = {t | out t ∈ A}

• ⊥ be least saturated set

• ⊤ = SN, greatest saturated set

• [[μ^{a}F]] = μ^{[[a]]}F with F(A) = ([[F]](A))^{μ}

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

Soundness of Recursion (Iso)

• Term model

• Recursion rule:

\frac{s : ∀ı. (μ^{ı}F → C) → μ^{ı+1}F → C}{fix^{μ} s : μ^{a}F → C}

• Soundness by transfinite induction on [[a]].

• Step case – Show fix^{μ} s r ∈ [[C]] for r ∈ [[μ^{a+1}F]].

– Iso-system: we can assume r ⟶ in t.

– Have fix^{μ} s (in t) ⟶ s (fix^{μ} s) (in t).

– Show s (fix^{μ} s) (in t) ∈ [[C]].

– Use assumption for s on induction hypothesis.

Soundness of Corecursion (Iso)

• Corecursion rule:

\frac{s : ∀ı. ν^{ı} F → ν^{ı+1}F}{fix_{n}^{ν} s : ν^{a}F}

• Soundness by transfinite induction on [[a]].

• Step case – Show fix^{ν} s ∈ [[ν^{a+1}F]].

– Iso-system: Show out (fix^{ν} s) ∈ [[F (ν^{a}F)]].

– Have out (fix^{ν} s) ⟶ out (s (fix^{ν} s)).

– Show s (fix^{μ} s) ∈ [[ν^{a+1}F]].

– Use assumption for s on induction hypothesis.

Modelling Types (Equi)

• Semantic terms: set of terms that pass a certain number of test • t passes E :⟺ t ⊥ E

• t ⊥ E :⟺ E(t) ∈ SN

• A = E^{⊥} = {t | t ⊥ E for all E ∈ E}

• A → E^{⊥} = {E ∘ (_s) | E ∈ E, s ∈ A}

• Galois connection: A^{⊥} ⊇ E ⟺ A ⊆ E^{⊥}.

• Closure: \overline{A} = A^{⊥⊥}.

• Infimum of saturated sets: inf_{i∈I} A_{i} = ⋂_{i∈I} A_{i}

• Supremum of saturated sets: sup_{i∈I} A_{i} = \overline{⋃_{i∈I} A_{i}}

Soundness of Corecursion (Equi)

• Corecursion rule:

\frac{s : ∀ı. ν^{ı} F → ν^{ı+1}F}{fix_{n}^{ν} s : ν^{a}F}

• Soundness by transfinite induction on [[a]].

• Step case – Show fix^{ν} s ∈ [[ν^{a+1}F]] = E^{⊥}.

– Assume arbitrary E ∈ E

– Show E (fix^{ν} s) ∈ SN.

– Have E (fix^{ν} s) ⟶ E (s (fix^{ν} s)).

– Show s (fix^{μ} s) ∈ [[ν^{a+1}F]].

– Use assumption for s on induction hypothesis.

4 Generic Programming with Sized Types

Generic Programming: Type-Indexed Types

• 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⟨μ⟩  = μ

Generic Programming: Type-Indexed Values

• 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}⟩ = fix_{n}^{μ} for some n

Generic Programming: Results • Extended gen. prog. to sized types.

• Termination of generic finite map operations (Hinze) through typing.