Fixed Points of Type Constructors

and Primitive Recursion

Andreas Abel joint work with Ralph Matthes

CSL’04

Karpacz, Karkonoski National Park, Poland September 21, 2004

Work supported by: GKLI (DFG), TYPES & APPSEM-II (EU), CoVer (SSF)

Regular Data Types

• Regular data types in Haskell:

data Nat    = Zero | Succ Nat
data List a = Nil | Cons a (List a)

• Least fixed points of type transformers of kind ∗ → ∗:

NatF : ∗ → ∗
NatF := λX. 1 + X
Nat : ∗
Nat := μ NatF

• Works also for List, since parameter a can be abstracted.

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

Nested Datatypes

• Non-regular or nested datatype: non-empty triangles.

  data Tri a = Sg a | Cons a (Tri (e,a))

• Parameter (resp., element type) grows in recursion.

A E E E
A E E
A E
A

• Fixed point of a type constructor of kind (∗ → ∗) → (∗ → ∗)

(rank-2 type).

TriF : (∗ → ∗) → ∗ → ∗  Tri : ∗ → ∗
TriF := λXλA. A + A × X (E × A)  Tri := μ TriF

Programming with Nested Datatypes …

• … requires polymorphic recursion.

• Example: cutting the top row off a trapezium.

  cut :: Tri(e,a) -> Tri a
  cut (Sg   (e,a)  ) = Sg a
  cut (Cons (e,a) r) = Cons a (cut r)

• In the recursive call, the argument r has type Tri(e,(e,a)).

• Does the recursive definition of cut have a solution? (Yes.)

• Instance of a terminating programming scheme.

Programming Scheme: Iteration

• Description:

– top-down pass: recursive decent into datastructure, adjusting parameters for the …

– … bottom-up pass: composing the result

– herein: each node treated generically, no access to current position or whole data structure

• Example: Nat.add, List.map, List.foldr

• Properties: termination, computational laws (fusion).

• Drawback: Result is always built from scratch, hence predecessor functions like Nat.pred, List.tail have linear time complexity.

Programming Scheme: Primitive Recursion

• Primitive recursive functions: e.g., Nat.factorial or redecoration (Uustalu/Vene, 2002)

redec :: (List a -> b) -> List a -> List b
redec f Nil         = Nil
redec f (Cons a as) = Cons (f (Cons a as)) (redec f as)

• Like iteration, but access to immediate sublist as itself, not just to the result of redec for as.

• Hence, access to current position l = (Cons a as) on r.h.s.

The Programming Schemes for Rank 1

• Iteration for rank-1 (= regular) datatypes can be simulated by β-reduction in System F (= λ2).

• Primitive recursion can be simulated in an extension Fix (= λ2U) of System F by positive fixed point (=retract) types. (Geuvers 1992)

\xymatrix{It \ar[r] & F \\ Rec \ar[r] & Fix}

• Primitive recursion cannot be simulated by β-reduction in System F. (Spławski/Urzyczyn 1999)

Prim. Rec. for Rank 2: Triangle Redecoration

• Relabelling the diagonal of a triangular matrix: The new diagonal element is computed from its subtriangle by the redecoration rule f :: Tri a -> b.

redec :: (Tri a -> b) -> Tri a -> Tri b
redec f t@(Sg   a  ) = Sg   (f t)
redec f t@(Cons a r) = Cons (f t) (redec (lift f) r)

• Herein, we need to lift the redecoration rule to a trapezium.

lift :: (Tri a -> b) -> Tri (e,a) -> (e,b)
lift f t = (aux t, f (cut t))
    where aux (Sg   (e,a)  ) = e
          aux (Cons (e,a) r) = e

The Programming Schemes for Higher Ranks

• Iteration for rank-n datatypes can be simulated in System F^{ω}. (TYPES 02, FoSSaCS 03, forthcoming TCS)

• New result: primitive recursion can be simulated in Fix^{ω}.

\xymatrix{It^{ω} \ar[r] & F^{ω} \\ _{Rec_{ω}} \ar[r] & Fix^{ω}}

• Fix^{ω}: System F^{ω} with fixed points of positive type constructors.

• Difficulty: What is positivity for higher ranks?

• Solution: Distinguish co-/contra-/invariant type constructors by polarity annotation in their kind (Steffen 1998).

System Fix^{ω}: Syntax

Polarities  p  ::= +  covariant
| −  contravariant
| ∘  invariant
Kinds  κ  ::= ∗ | pκ → κ′
Constructors  A, B, F, G ::= X | λX^{pκ}. F | F G | A → B | ∀X^{κ}. A | fix F
Objects (terms) r, s, t  ::= x | λx.t | r s
Contexts  Δ  ::= ⋄ | Δ, x:A | Δ, X^{pκ}

System Fix^{ω}: Examples

• Impredicative encodings (non-strictly positive):

\begin{aligned}× & : & +∗ → +∗ → ∗ \\ × & := & λX^{+∗}λY^{+∗}∀Z^{∗}. (X → Y → Z) → Z \\ + & : & +∗ → +∗ → ∗ \\ + & := & λX^{+∗}λY^{+∗}∀Z^{∗}. (X → Z) → (Y → Z) → Z \end{aligned}

• Self-composition of monotone X : +∗ → ∗ is monotone in X: λX^{+(+∗→∗)}λA^{+∗}. X (X A) : +(+∗ → ∗) → (+∗ → ∗)

• But: self-composition of arbitrary X : ∘∗ → ∗ is not monotone

in X: ⊬ λX^{+(∘∗→∗)}λA^{∘∗}. X (X A) : +(∘∗ → ∗) → (∘∗ → ∗)

System Fix^{ω}: Kinding

• Function space and quantification:

\frac{−Δ ⊢ A : ∗ Δ ⊢ B : ∗}{Δ ⊢ A → B : ∗} \frac{Δ, X^{∘κ} ⊢ A : ∗}{Δ ⊢ ∀X^{κ}. A : ∗}

−Δ inverts all polarities in Δ.

• Positive fixed points:

\frac{Δ ⊢ F : +κ → κ}{Δ ⊢ fix F : κ}

• Variables:

\frac{X^{pκ} ∈ Δ  p ∈ \{+, ∘\}}{Δ ⊢ X : κ}  \frac{Δ, X^{pκ} ⊢ F : κ′}{Δ ⊢ λX^{pκ}. F : pκ → κ′}

System Fix^{ω}: Kinding of Application

• Application of covariant constructor:

\frac{Δ ⊢ F : +κ → κ′ Δ ⊢ G : κ}{Δ ⊢ F G : κ′}

• Application of contravariant constructor:

\frac{Δ ⊢ F : −κ → κ′ −Δ ⊢ G : κ}{Δ ⊢ F G : κ′}

• Application of invariant constructor:

\frac{Δ ⊢ F : ∘κ → κ′ ∘Δ ⊢ G : κ}{Δ ⊢ F G : κ′}

∘Δ erases all assumptions with positive or negative polarity from Δ.

System Fix^{ω}: Equality

• Fixed-point axiom.

\frac{Δ ⊢ F : +κ → κ}{Δ ⊢ fix F = F (fix F) : κ}

• Computation: β-axiom.

\frac{Δ, X^{pκ} ⊢ F : κ′ pΔ ⊢ G : κ}{Δ ⊢ (λX^{pκ}. F) G = [G/X]F : κ′}

• Extensionality: η-axiom.

\frac{Δ ⊢ F : pκ → κ′}{Δ ⊢ λX^{pκ}. F X = F : κ′} X ∉ FV(F)

• Congruences for all type constructors.

• Symmetry and transitivity. (Reflexivity admissible.)

System Fix^{ω}: Typing and Reduction

• Typing rules of simply typed lambda-calculus,

• plus quantification,

\frac{Δ, X^{∘κ} ⊢ t : A}{Δ ⊢ t : ∀X^{κ}. A}  \frac{Δ ⊢ t : ∀X^{κ}. A ∘Δ ⊢ F : κ}{Δ ⊢ t : [F/X]A}

• and type equality (includes fixed point (un)folding).

\frac{Δ ⊢ t : A Δ ⊢ A = B : ∗}{Δ ⊢ t : B}

• Reduction: just β.

System Fix^{ω}: Strong Normalization

• Construct a model of untyped strongly normalizing terms.

• Types are interpreted as saturated set of SN terms, constructors as operators on these sets:

A : ∗  ⟹  [[A]] ∈ SAT
F : +κ → κ′  ⟹  [[F]] ∈ SAT^{κ} ⟶^{+} SAT^{κ′}

• Positive constructors are interpreted as monotone operators.

• Soundness: If t : A then t ∈ [[A]].

• Entails that t cannot be reduced infinitely.

Mendler-Style Primitive Recursion

• Natural transformation F ⊆^{κ⃗→∗} G := ∀X⃗κ⃗. F X⃗ → G X⃗.

• Formation

μ^{κ} : (κ → κ) → κ

• Introduction

in^{κ} : F (μ^{κ}F) ⊆^{κ} μ^{κ}F

• Elimination

\frac{s : ∀X^{κ}. (X ⊆^{κ} μ^{κ}F) → (X ⊆^{κ} G) → (F X ⊆^{κ} G)}{MRec^{κ} s : μ^{κ}F ⊆^{κ} G}

• Reduction

MRec s (in t) ⟶_{β} s id (MRec s) t

• μ^{κ}, in^{κ}, and MRec^{κ} can be defined in Fix^{ω}; the reduction rule is simulated.

On “Conventional” Primitive Recursion

• Conventional primitive recursion relies on monotonicity of type generating functor F.

• For rank 1: monF := ∀A∀B. (A → B) → (F A → F B).

• For higher ranks: several formulations of monotonicity.

• Basic monotonicity:

monF := ∀A^{κ}∀B^{κ}. (A ⊆^{κ} B) → (F A ⊆^{κ} F B).

• But: λX.X ∘ X not basic monotone.

• Hence no primitive recursion principle for truly nested datatypes like

  data Bush a = Nil | Cons a (Bush (Bush a))

• Other notions of monotonicity: FoSSaCS 2003, TCS 200?.

Conclusion

Results:

• First formulation (!?) of primitive recursion for nested data types.

• First formulation (!?) of positive recursive types for higher ranks.

• Embedding of primitive recursion into fixed-point types (Geuvers 1992) works also for higher ranks.

Further work: conventional primitive recursion

Related Work

• Nested datatypes: Okasaki 1996, Hinze 1998, Bird/Paterson 1999, Altenkirch/Reus 1999

• Polarized higher-order subtyping: Steffen 1998, Duggan/Compagnoni 1998

Appendix: Semantics of Constructors

Let U = ⋃_{κ} SAT^{κ}. For valuation θ ∈ TyVar ⇀ U, define [[−]]_{θ} ∈ Constr ⇀ U:

[[X]]_{θ}  := θ(X)
[[λX^{pκ}. F]]_{θ} := \{ \begin{matrix}F & if F ∈ SAT^{κ} ⟶^{p} SAT^{κ′} for some κ′ \\ undef. & else \end{matrix}

where F(G ∈ SAT^{κ}) := [[F]]_{θ[X↦G]}

[[F G]]_{θ}  := [[F]]_{θ}([[G]]_{θ})
[[fix F]]_{θ}  := \{ \begin{matrix}lfp F & if F ∈ SAT^{κ} ⟶^{+} SAT^{κ} for some κ \\ undef. & else \end{matrix}
where F := [[F]]_{θ}

Properties of Semantics

• Extend interpretation to contexts Δ.

• Let θ ∈ SAT^{Δ} (each variable mapped to semantical operator of correct kind).

• If Δ ⊢ F : κ then [[F]]_{θ} ∈ SAT^{κ} (welldefinedness).

• If Δ ⊢ F = F′ : κ then [[F]]_{θ} = [[F′]]_{θ} (soundness of equality).