Higher order recursion

Martin Wehr

15. Januar 1998

1 Motivation

Assume we are given the definition of a recursive data type like :

  data   List a =  Nil | Cons( a, List a)

The meaning the elements and operations on such an data type can be given in several viewpoints. We will concentrate on the view point of functional programming, category theory and type theory. The functional programming view gives the two functions map and fold to every recursive data type. The categorical approach associates a polynomial functor to the data type definition. The operations on the data type are than explained as mediating arrows given by initial algebras of these functor. The type theoretic view translates the data type definition into polymorphic combinators with fold-like behaviour.

The List example involves only simple recursion. The meaning of simple recursive data types is well understood. The whole paper is about extending this solution to higher order recursion. One example of higher order recursion is the bracketing language :

  data  I   =  OpS B ()
  data  B a =  Cl a  | Op B B a

The elements of the data type I are the the words of the bracket language which shows up if we take constructors Op and OpS as the opening brackets “[” and Cl as the closing bracket “]”. Notice the higher order recursive use of type B B a in the definition of type B a.

In the following we want to examine a game theoretic example. The aim is to represent games as higher order recursive data types. The operations on games and strategies should then be represented by simple map and fold functions. Definition A bracketing arena is given by a tuple A = (M_{A}, λ_{A}, ⊢_{A} ) where M_{A} is a set of moves. λ : M_{A} → {Q, A} is a bracketing labelling. ⊢_{A} is a relation ⊢_{A} ⊆ M_{A} + {∗} × M_{A} which satisfies :

• ∗ ⊢_{A} m ⟹ λ_{A}(m) = Q

• m ⊢_{A} n ∧ λ_{A}(n) = A ⟹ λ_{A}(M) = Q

The elements (m, n) of the enabling relation ⊢_{A} are called justifiers A play is a sequence of moves where every move is justified by an earlier move in the sequence. Its not necessary that a move must justify its immediate following move. Every arena can be encoded as a data type similar to the bracketing language. We define a data type M a for every move m in the arena and a type A corresponding to the element ∗. For every justifier (m, n) we introduce a data constructor Mjn.

           data A  = Strtm N () if ∗ ⊢_{A} m

data M a = Mjn a  if m ⊢_{A} n ∧ λ_{A}(n) = A
Mjn N M a if m ⊢_{A} n ∧ λ_{A}(n) = Q

The language coded by A is the language of plays. Now there is an obvious mutual recursive definition of a map functions for every move m :

mapm :: (a -> b) -> (M a -> M b)
  map f (Mjn a)   = f a               \\ if n is an answer
  map f (Mjn nma) = mapn (mapm f) nma \\ if n is a question

The view function compresses a play so that every move is justified by its immediate preceding move. The structure of the view function follows directly from the definition of data type A.

view :: A -> A
  view Strtm ma = viewn ma  \\ one case for every starting move m
viewm :: M a -> M a    \\ for every move m
  viewm  Mjn a   = Mjn a           \\ if n is an answer
  viewm  Mjn nma = mapn viewm nma  \\ if n is a question

Later we will see that the simple structure of the view definition is due to its canonical definition. The view-function will be represented as fold with identity arguments. This canonical structure leads to a simple proof of the idempotence of

view.

2 Background

Let’s recall the techniques to handle simple recursive data types. We start with analysing a familiar example :

  data   List a =  Nil | Cons( a, List a)

2.1 categorical viewpoint

Assume we are given a category C which has finite products and coproducts. We are able to express the definition of lists as a functor of two arguments L(A, B). So that the list can be expressed as the solution of a parametric isomorphism B ≃ L(A, B) The 2-ary functor related to the list definition has form:

L(A, B) = 1 + A × B

The translation of the definition into the functor is done by substituting the simple recursive appearance of List a by the new argument B. Now the functor F (A, ) has to have an initial algebra in C for every object A. That is the we need an object F^{†}A and a morphism a : F (A, F^{†}A) → A which is initial in the comma category F (A, ) ↓ C. The initiality of a gives for every F (A, )-algebra (that is an object C with arrow c : F (A, C) → C) a mediating arrow < c >: F^{†}A → C satisfying :

[figure: F (A, F^{†}A); a; F (A,<c>); F^{†}A; <c>; F (A, C); c; C]

The assignment which gives to every object A ∈ C an object F^{†}A is functorial. This can be verified by the following diagram which can be constructed for every arrow f : A → C.

[figure: F (A, F^{†}A); a; F (A,F^{†}f); F^{†}A; <b∘F (f,F^{†}B)> =^{def}F^{†}f; F (A, F^{†}B); F (f,F^{†}B); F (B, F^{†}B); b; F^{†}B]

In terms of functional programming we can identify the operation < > of building the mediating arrow as the fold function. For the list example an arrow c : L(A, C) → C is simply given by a constant d : 1 → C and a binary operation ⊕ : A × C → C. In this case the application fold d ⊕ denotes the same function as the mediating arrow < [d, ⊕] > which is also called the catamorphism.

2.2 type theoretic viewpoint

Girard gave a treatment of algebraic data types in terms of combinators. Assume we are given the system F_{2} of explicitly typed second order lambda calculus :

types  σ ::= α | σ → σ | ∀α.σ
expressions e ::= x | λx : σ.e | ee | Λα.e | eσ

Now assume that an algebraic data type T is given by a definition like :

data T α_{1} … α_{n} = f_{1}τ_{1}^{1} … τ_{k_{1}}^{1} | … | f_{m}τ_{1}^{m} … τ_{k_{m}}^{m}

Where τ are simple types given by the grammar τ ::= α_{1} | … | α_{n} | T | τ → τ. So look at this as a recursive definition of type T with free type parameters α_{1} … α_{n}. Girard restricts these data definitions in allowing the variable T to occur only positively in the types τ_{j}^{k}. Now the whole idea to handle recursive data types is to give a combinator F_{i} for every type constructor f_{i}. The combinator codes the algorithm for the fold operation which is named in type theoretic circles structural induction. The construction of the combinator uses a type controlled translation of variables into expressions [x_{j} :: τ_{j}^{i}]^{+}.

τ_{i} =^{def} τ_{1}^{i} → … → τ_{k_{i}}^{i} → T

the type for every constructor f_{i}

σ =^{def} ∀T.τ_{1} → … → τ_{m} → T

F_{2} type representing the recursive data type

τ̃ =^{def} τ[σ/T]

the operation to substitute the name T by its interpretation

then τ̃_{i} is type of combinator F_{i}

F_{i} =^{def} λx_{1} : τ̃_{1}^{i}…. λx_{k_{i}} : τ̃_{k_{i}}^{i}.ΛT.λy_{1} : τ_{1}…. λy_{m} : τ_{m}.y_{i}t_{1}^{i} … t_{k_{i}}^{i}

the combinators F_{i}

The argument expressions t_{j}^{i} : τ_{j}^{i} are build by structural induction on the type

structure of τ_{j}^{i}. So the argument expressions are defines as t_{j}^{i} =^{def} (x_{j} :: τ_{j}^{i})^{+}.

\begin{matrix}[x :: T]^{+} & ↦ & xT y_{1} … y_{m} \\ [x :: α_{k}]^{+−} & ↦ & x \\ [x :: τ → τ′]^{+} & ↦ & λy : τ.[(x[y :: τ]^{−}) :: τ]^{+} \\ [x :: τ → τ′]^{−} & ↦ & λy : τ̃.[x :: τ′]^{−}[y :: τ]^{+} \end{matrix}

Notice that there is no case defined for [x :: T]^{−} because type variable T is used only positively. All translations work with use of typotheses Γ = T, α_{1}, …, α_{n}; y_{1} : τ_{1}, …, y_{m} : τ_{m}. The translations give the following conversions which are well typed in F_{2}.

\begin{matrix}Γ ⊢ λx : τ̃.[x :: τ]^{+} : τ̃ → τ \\ Γ ⊢ λx : τ.[x :: τ]^{−} : τ → τ̃ \end{matrix}

In the following we will call these combinators C_{τ}^{+} and C_{τ}^{−}. Keep in mind that these “combinators” are not closed F_{2} expressions because they use the variables of typotheses Γ.

Given a value v : σ and operations s_{i} : τ_{i}[σ′/T] then the evaluation of expression vσ′s_{1} … s_{m} : σ′ results in folding the operations over the value.

The following is a type theoretic presentation of the map function.

Definition 1 (the sign translation) Given a type σ with free type variable α and two two types σ′, σ′′, then the signed substitution σ[σ′, α, σ′′] substitutes positive occuring α by σ′ and negative occuring α by σ′′.

\begin{matrix}α[σ′, α, σ′′] & ↦ & σ′ \\ β[σ′, α, σ′′] & ↦ & β \\ σ_{1} → σ_{2}[σ′, α, σ′′] & ↦ & σ_{1}[σ′′, α, σ′] → (σ_{2}[σ′, α, σ′′]) \\ ∀β.σ_{1}[σ′, α, σ′′] & ↦ & ∀β.(σ_{1}[σ′, α, σ′′]) \end{matrix}

We can extend this type directed translations to F_{2} expressions. Given the typed expression e : σ and two functions p : α → σ′ and n : σ′′ → α then we can construct an new expression ([p, α, n]e :: σ) of type σ[σ′, α, σ′′].

\begin{matrix}[p, α, n]e :: α & ↦ & pe \\ [p, α, n]e :: β & ↦ & e \\ [p, α, n]e :: σ_{1} → σ_{2} & ↦ & λx : σ_{1}[σ′′, α, σ′].([p, α, n](e([n, α, p]x :: σ_{1})) :: σ_{2}) \\ [p, α, n]e :: ∀β.σ_{1} & ↦ & Λβ.([p, α, n]e :: σ_{1})β \end{matrix}

Corolary 1 If e : σ[σ^{+}, α, σ^{−}] is well typed and we have two functions p : σ^{+} → σ′^{+} and n : σ′^{−} → σ^{−} then the translation ([p, α, n]e :: σ) ↦ e′ gives a well typed result e′ : σ[σ′^{+}, α, σ′^{−}]. So we can define the following well typed combinator :

M_{σ,α} = λp : σ^{+} → σ′^{+}.λn : σ′^{−} → σ^{−}.λx : σ[σ^{+}, α, σ^{−}].([p, α, n]x :: σ)

This combinator codes the algorithm of the functor related to type σ. The type variable α is translated into a covariant argument p for every positive occurrence of α in σ and a contravariant argument n for every negative occurrence of α in σ.

If the type variable α occurs only positive in type σ the we can drop argument n and get a simpler combinator :

M_{σ,α} : (σ′ → σ′′) → (σ[σ′/α] → σ[σ′′/α])

3 Intuition

Now that we recalled the handling of algebraic data type which are simple recursive, we want to step forward. Here we will have a in depth look on an example involving higher order recursion. The aim of this section is to give an intuition which will be formalised and proved latter on. As an example we use the following type definition :

   data   D a =  V a | Lev D D a*a

We want to understand the map and fold on data type D. Obviously the type definition gives a functor :

\begin{matrix}D : C × EndC → C \\ D(A, F) = A + F^{2}(A × A) \end{matrix}

Here EndC denotes the category of endofunctors on C. Because of the functor argument F we call D the higher order functor associated to the data definition. The morphism part of this functor can be presented as a functional program in a ML like style.

           map_{D} : (a -> b) -> (D a -> D b)

           map_{D} f (V a)       =  V (f a)
           map_{D} f (Lev dda2)  =  map_{D} (map_{D} (f × f)) dda2

To define the fold function we have to understand the set of operations which will be folded. To express the types of the operation we define the functor D^{∗}(A) = D(A, Id) = A+A×A. So a morphism g : D^{∗}(A) → A can be seen as two operations f = g ∘ inl_{D^{∗}(A)} : A → A and ⊕ = g ∘ inr_{D^{∗}(A)} : A × A → A. With these ingredients we can present the fold function.

     fold_{D}^{i} f ⊕ (V a)       =  f a
     fold_{D}^{i} f ⊕ (Lev dda2)  =  let f = fold_{D}^{i} f ⊕ in

                                  ;;; f : D a -> a
                                    let f' da2 = f (map_{D} ⊕ da2)
                                      ;;; f' : D a*a -> a
                                        in f (map_{D} f' dda2)

We will call the above fold version an isofold because of the unchanged type parameter a in fold_{D}^{i} f ⊕ : Da− > a . To get a general fold function which typed like fld op_{1} … op_{n} : D a -> b there are three kind of useful operations op_{i}.

argument operations g^{a} : D^{∗}(A) → A
transform operations g^{t} : D^{∗}(A) → B
result operations  g^{r} : D^{∗}(B) → B

This gives two ways to define a general fold. The pre fold starts with a transformation operation and continues with result operations. The post fold starts with argument operations and finishes with a transformation operation.

We conclude with the algorithm for the pre fold :

 fold_{D}^{pre} f^{t} ⊕^{t} f^{r} ⊕^{r} (V a)       =  f^{t} a
 fold_{D}^{pre} f^{t} ⊕^{t} f^{r} ⊕^{r} (Lev dda2)  =  let fr = fold_{D}^{i} f^{r} ⊕^{r} in

                                      ;;; fr : D b -> b
                                         let f' da2 = fr (map_{D} ⊕^{t} da2)
                                          ;;; f' : D a*a -> b
                                             in fr (map_{D} f' dda2)

… and the algorithm for the post fold :

 fold_{D}^{post} f^{a} ⊕^{a} f^{t} ⊕^{t} (V a)       =  f^{t} a
 fold_{D}^{post} f^{a} ⊕^{a} f^{t} ⊕^{t} (Lev dda2)  =  let fa = fold_{D}^{i} f^{a} ⊕^{a} in

                                       ;;; fa : D a -> a
                                         let f' da2 = fa (map_{D} ⊕^{a} da2)
                                           ;;; f' : D a*a -> a
                                             in f^{t} (fa (map_{D} f' dda2))

Actually in the definition of fold_{D}^{post} the argument ⊕^{t} is never used so that fold_{D}^{post} can be represented by a an iso fold and a morphism f^{t}.

           fold_{D}^{post} f^{a} ⊕^{a} f^{t} ⊕^{t} = [f^{t}, f^{t} ∘ (fold_{D}^{i} f^{a} ⊕^{a})]

Further observe that iso fold can be represented by the pre and post folds.

          fold_{D}^{post} f ⊕ f ⊕ = fold_{D}^{pre} f ⊕ f ⊕ = fold_{D}^{i} f ⊕

Given an argument operation g^{a} : D^{∗}(A) → A and a result operation g^{r} : D^{∗}(B) → B and a morphism t : A → B, then there are two ways to construct a transformation operation g^{t} : D^{∗}(A) → B as g_{1} = g^{r} ∘ D^{∗}(t) and g_{2} = t ∘ g^{a}. If these morphisms g_{1} and g_{2} coincide the t is called a D^{∗}( )-algebra morphism.

3.1 The fold translation

Here we will present the algorithm which translates a higher order type definition into the fold algorithm corresponding to the type. We start by formalising the language of higher order type definitions. Assume we are given a set Δ of type variables. The language of first order type definitions is given by the following grammar.

t ::= α  for type variables α ∈ Δ
| t × t′ | t + t′
| r  recursive use

A path p, q is an element of ℕ^{∗}, that is a string of natural numbers with ϵ the empty string. The operation • concatenates two pathes. We define the subterm operation t| : ℕ^{∗} → t by :

α_{|ϵ} = α
(t_{1} × t_{2})_{|i•p} = (t_{1} + t_{2})_{|i•p} = (t_{i})_{|p} for i = {1, 2}
r_{|ϵ} = r

t_{|p} undefined else

So pth(t) = {p|t_{|p}defined} is the set of pathes in t and occ(r, t) = {p|t_{|p} = r} is the set of occurrences of variable r in t. Paths are ordered by the prefix order p ⊑ q iff there exists a path q′ with p • q′ = q this suffix is denoted as q′ = p \ q. We define p ↑ is the upper set of a path and the lower set p ↓ is defined dually. for a subset P ⊆ ℕ^{∗} we define.

\begin{aligned}succ(p, P) & = & min (p ↑ ∩P) & = & \{q|p ⊑ q ∧ q ∈ P ∧ ¬∃q′ ∈ P.p ⊏ q′ ⊏ q\} \\ pred(p, P) & = & max (p ↓ ∩P) & = & \{q|q ⊑ p ∧ q ∈ P ∧ ¬∃q′ ∈ P.q ⊏ q′ ⊏ q\} \end{aligned}

If P is downward closed pred(p, P) is a singleton. So we use pred as a function.

Assume that m = |Δ| is the number of typevariables available in the definition of a first order type. Then we define the form of a constructor argument by :

a ::= t_{1} × ⋯ × t_{m}

The pre definition of a higher order type is given by the following grammar :

h ::= t | h[p = a] for p ∈ occ(r, h)

The insertion operation [p = a] substitutes a recursion variable r at path p in the type definition h by \overline{r}(a). So we get an extended subterm operation h[p = a]_{|p} = \overline{r}(a) and h[p = a]_{|p•q} = a_{|q}. A higher order type definition h has no free recursive occurrences occ(r, h) = ∅. So every type definition is of form t[p_{1} = a_{1}] … [p_{n} = a_{n}]. We call R = [p_{1} = a_{1}] … [p_{n} = a_{n}] the insertion to the definition and P = {p_{1}, …, p_{n}} is called the set of recursive uses of the definition.

Given a higher order type definition h = t[p_{1} = a_{1}] … [p_{n} = a_{n}] we define the fold function to a result type B. Let a_{0} = Δ then we define the operation fop_{i} for 0 ≤ i ≤ n. These fold operation are the arguments of the fold function.

fop_{i} : (t[a_{i}/Δ] → r)[B/r]

So that the fold operation has the following type :

fold fop_{0} … fop_{n} : \overline{r}(Δ) → B

Now we define a set of pre fold functions For every constructor argument a_{i} = R(p_{i}) in the set of recursive uses P = {p_{1}, …, p_{n}} we have a map function where we use the occurrence of r in a_{i} as free parameters :

\begin{matrix}set Q = succ(p, P)for p ∈ P \\ map_{p}^{r} : (∏_{q∈Q} α_{q} → β_{q}) → (a_{i}[p \ q = α_{q}] → a_{i}[p \ q = β_{q}]) \end{matrix}

The basic type definition t defines a map function by using the m = |Δ| type variables as free parameters.

map_{t}^{Δ} :: ( ∏_{α∈Δ} α_{α} → β_{α}) → (t[\overline{α}/Δ] → t[\overline{β}/Δ])[B/r]

where [\overline{α}/Δ] and [\overline{β}/Δ] denote the substitution of the type variables Δ be the variables \overline{α} = (α_{α})_{α∈Δ} or \overline{β} = (β_{α})_{α∈Δ}.

Now we define a set of pre fold functions for every constructor argument a_{i} = R(p):

for Q = succ(p, P′) = {q_{1}, …, q_{l}}
and m = |Δ|
define \overline{fld}_{p} = (fld_{q_{1}}, …, fld_{q_{l}})
and \overline{m}_{p} = map_{p}^{r}\overline{fld}_{p} : (∏_{α_{j}∈Δ} h_{|p•j} → (a_{i})_{|j})[B/r]
finally fld_{p} = fop_{p} ∘ (map_{t}^{Δ}\overline{m}_{p}) : h_{|p} → B

By the equivalence h_{|ϵ} = h ≃ \overline{r}(Δ) we define the result fold = fld_{ϵ}.

3.2 second presentation

Given a sequence \overline{a} of type variables and a sequence \overline{r} of recursion variables. A simple pre type t over \overline{a} and \overline{r} is given by the following grammar :

t ::= a_{i} | t + t′ | t × t′ | r_{j}

where every recursion variable r_{j} occurs at most once in t. We define a map-function for every type t over \overline{a} and \overline{r}. For \overline{r} = r_{1} … r_{l} we get :

map_{t}^{\overline{r},\overline{a}} : (b_{1} → c_{1}) → … → (b_{l} → c_{l}) → (t[b_{1}/r_{1}, …, b_{l}/r_{l}] → t[c_{1}/r_{1}, …, c_{l}/r_{l}])

map_{r_{j}}^{\overline{r},\overline{a}}\overline{f}e  = f_{j}e
map_{t_{1}+t_{2}}^{\overline{r},\overline{a}} \overline{f}(inj_{i} e) = inj_{i}(map_{t_{i}}^{\overline{r},\overline{a}}\overline{f}e)  for i ∈ \{1, 2\}
map_{t_{1}×t_{2}}^{\overline{r},\overline{a}} \overline{f}(e_{1}, e_{2}) = (map_{t_{1}}^{\overline{r},\overline{a}}\overline{f}e_{1}, map_{t_{2}}^{\overline{r},\overline{a}}\overline{f}e_{2})
map_{a_{i}}^{\overline{r},\overline{a}}\overline{f}e  = e

So map_{t}^{\overline{r},\overline{a}} takes for every recursive variable r_{j} a function f_{j} : a_{j} → b_{j} and applies it whereas map operates on type variables a_{i} as identity. The function map_{t}^{\overline{a},\overline{r}} is defined the other way round so while evaluation of map_{a_{i}}^{\overline{a},\overline{r}}\overline{f}e every subterm e′ in e of type a_{i} the function f_{i} will be applied while if e′ has type r_{j} its unchanged copied into the result expression.

Now we fix the sequence of type variables as \overline{a} = a_{1} … a_{m}. So for a sequence \overline{r} we call :

\overline{s} ::= t_{1} × ⋯ × t_{m}

a type argument where every r_{j} is used at most once.

A higher order pre type is given by

h ::= t | h[r = \overline{s}]

Where every recursion variable r′ occurs uniquely either in h or in \overline{s}. We call the recursion variable r in h[r = \overline{s}] bound. A higher order type is a pre type h without free recursion variables. We extend the map-function on higher order pre types h = t[r_{1} = \overline{s}_{1}] … [r_{n} = \overline{s}_{n}]. We call S = [r_{1} = \overline{s}_{1}] … [r_{n} = \overline{s}_{n}] the replacement and use it as a function from recursion variables to type arguments. If \overline{r} are the free recursion variables of h we define imap_{t′,S}^{\overline{r},\overline{a}} as :

imap_{r′_{j},S}^{\overline{r},\overline{a}}\overline{f}e = f_{j}e if r′_{j} in \overline{r}
imap_{r_{i},S}^{\overline{r},\overline{a}}\overline{f}e = imap_{t[\overline{s}_{i}/\overline{a}],S}^{\overline{r},\overline{a}}\overline{f}e if R(r_{i}) = \overline{s_{i}}
imap_{t,S}^{\overline{r},\overline{a}}  = else defined as map_{t}^{\overline{r},\overline{a}}

So we define map_{h}^{\overline{r},\overline{a}}\overline{f} = imap_{t,S}^{\overline{r},\overline{a}}\overline{f} for h = tS.

3.2.1 type directed fold construction

We introduce the operations an _{ ˆ r} on simple types t type arguments \overline{s} and higher order types h. By definition t̃ is given through substitution of every recursion variablein t by b. The pre type t̂_{r} is given if all recursion variables but r are replaced by b.

Given a higher order type of form h = t[r_{1} = \overline{s}_{1}] … [r_{n} = \overline{s}_{n}]. In the following we assume to be given the data type definition :

data R\overline{a} = h[R\overline{a}/r_{1}, …, R\overline{a}/r_{n}]

for type variables \overline{a} = a_{1} … a_{m} We define h_{j} =^{def} h = t[r_{1} = \overline{s}_{1}] … [r_{j} = \overline{s}_{j}] for 1 ≤ j ≤ n and h_{0} = t. We assume for every type argument \overline{s}_{j} = s_{1j} × ⋯ × s_{mj} we are given a sequence \overline{f}_{j} for 1 ≤ j ≤ n with f_{ji} : s̃_{ij} → a_{i} for 1 ≤ i ≤ m and an operation fop : t̃→ b. These functions will be used to define a function :

fold_{R}\overline{f}_{1} … \overline{f}_{n}fop : R\overline{a} → b

This function will be recursively used so we assume given fld : R\overline{a} → b. Now using the sequence \overline{f}_{j} we get :

map_{h}^{\overline{a},∅}\overline{f}_{j} : h[\overline{s}_{j}/\overline{a}] ≃ R\overline{s}_{j} → h[\overline{a}/\overline{a}] ≃ R\overline{a}

Composition with fold gives :

fld ∘ (map_{h}^{\overline{a},∅}\overline{f}_{j}) : [figure: R\overline{s}_{j}; map; R\overline{a}; fld; b]

If we define ĥ_{i} =^{def} ĥ_{i−1}_{|}r_{i} so ĥ_{i} is h_{i−1} where all recursion variables are replaced by b but the recursion variable r_{i}. Using ĥ_{i} we get the following reduction function :

red_{i} = mapr_{i},\overline{a}.b ; ĥ_{i}(fld ∘ map_{h}^{\overline{a},∅}\overline{f}_{j}) : h̃_{i} = ĥ_{i}[r_{i} = ˜ \overline{s}_{i}] → ĥ_{i}[r_{i} = b] = h̃_{i−1}

Finaly we get the definition of fold by :

fop∘red_{1}∘⋯∘red_{n} : [figure: R\overline{a} ≃ h = h_{n} = h̃_{n}; red_{n}; { \atop h_{n−1}}; red_{n−1}; …; red_{1}; h̃_{0} = t̃; fop; b]

4 Algebraic data types

Here are the formal notions needed for the use of algebraic data types. Given a set E then the set E^{∗} denotes the set of finite sequences of elements of E, where ϵ is the empty sequence and dot “.” denotes concatenation of sequences p.q. The prefix order on strings p, q ∈ E^{∗} is defined by p ⊑_{p} q iff there exists a suffix s ∈ E^{∗} such that p.s = q. Further for a sequence p ∈ E^{∗} we write |p| for the length of the sequence. We call the set ℕ^{∗} of strings over natural numbers paths p. A signature S is a tuple S = (C, a) where C is a set of constructors and a is the arity of the constructors which is a function a : C → ℕ_{0}. Let’s assume we are given a set Var of variables then T m(S, Var) or T m(C, Var) (if the arity a is clear) is the set of terms over variables Var. We define a term t as a prefix closed partial map from paths to constructors or variables :

t : ℕ^{∗} → C ∪ Var
t.p =^{def} t(p)  where p ∈ ℕ^{∗}
t.p.q def ⟹ t.p def  (prefix closure)
t.p = c ∈ C ∧ 1 ≤ i ≤ a(c) ⟹ t.p.i def (arity correct)

where t.p def expresses that t is defined for path p.

We define the set pth(t) =^{def} {p | t.p def} which is the domain of t and we define occ(t, c) =^{def} {p | t.p = c} where c ∈ C ∪ Var. We write c occ t if element c occurs in term t t.i. iff occ(t, c) ≠ ∅. The terms defined so far are node labelled trees including trees with infinite branches. We call a tree t finite iff |pth(t)| < ∞ where |S| is the cardinality of set S.

A subtree of a given term t at a path p is given by t|p =^{def} λq. t.p.q. The set of subtrees of a given term is defined by sub(t) =^{def} {t|p | p ∈ pth(t)}. The set of variables used in a term t is written as tv(t) = sub(t) ∩ V. If terms use no variables (t.i tv(t) = ∅) then this term is called ground. So we define GT m(S) the set of ground terms for a given signature S.

Definition 2 (algebraic data types) A algebraic data type A is a a 5-tuple (T , a, D, arg, t). Where T is the set of type constructors and the tuple (T , a) is signature with T y =^{def} T m(T , Var) is the set of types. We define for each n ∈ ℕ that V_{n} =^{def} {α_{1}, …, α_{n}} is a set of n type variables. The set D holds the data constructors. The map t gives the sort of a data constructor so t : D → T . We define for each T ∈ T the set of data constructors for T as D_{T} =^{def} {D | t(D) = T }. The map arg gives the arguments for a data constructor.

arg : D → T y^{∗}  where  ∀D ∈ D.a(t(D)) = n ⟹ arg(D) ∈ T m(T , V_{n})^{∗}

We do extend the path application notion from types to type sequences. For \overline{τ} = τ_{1} … τ_{n} ∈ T y^{∗} we define \overline{τ}.i =^{def} τ_{i} iff 1 ≤ i ≤ n so \overline{τ}.i is the i-th element of the sequence.

For example the definition List a = Nil | Cons (a , List a) will give a algebraic data type A = (T , a, D, arg, t) where

                 T  = {List}

a(List) = 1

                 D  = {Nil, Cons}
                 t  = {Nil ↦ List, Cons ↦ List}
                 arg  = {Nil ↦ ϵ, Cons ↦ α.Listα}

A type τ is defined by the grammar τ ::= α | τ → τ | T \overline{τ} (we take “→” as a type constructor with arity 2). A pure data type is build only with use of algebraic data type constructors only (τ ::= α | T \overline{τ}) if the arguments of the data constructors don’t use function types. We assign a polarity to the occurrence p of a variable α in a type τ t.i if τ.p = α. The occurrence is called positive if the path p went even times along the left side of type constructor “→”. The negative occurrence is defined opposite. For instance in type α → β the type variable α occurs negative and β occurs positive. A type τ is called polarised iff for every α ∈ tv(τ) all occurrences of this type variable in τ have the same polarity. So in a polarised type one can assign the polarity to type variables instead of their occurrence.

4.1 Algebraic data schemes

Definition 3 (substitution) A substitution S is a mapping from Var to T y. with dom(S) =^{def} {Sα ≠ α | α ∈ Var} finite. We can extend S structural to work on types and type sequences. Given a type constructor T we define the type argument substitution [\overline{τ}] =^{def} α_{i} ↦ \overline{τ}.i for 1 ≤ i ≤ a(T) so dom([\overline{τ}]) = V_{a(T)}.

A substitution is called ground if ∀α ∈ dom(S). tv(Sα) = ∅.

The definition ad =^{def} λd.|arg(d)| : D → ℕ_{0} gives arity function for set D so (D, ad) is a signature. We call the set of terms T m(D, V) for this signature the set of pre data schemes. A algebraic data scheme should be type correct. A algebraic data scheme is a value with holes which has type variables as place holders.

Definition 4 (algebraic data schemes) Let τ be a pure data type and V = tv(τ) be separated in the set of bound variables V_{b} and the set of free variables V_{f}. We define the set of data schemes by a mapping val : V × T y → T m(D, V) which maps a pure data type τ (or a sequence \overline{τ}) and a set of bound type variables to a set of pre data value :

val(∀V_{b}.T \overline{τ}) =^{def} \{D\overline{v} | D ∈ D_{T} and \overline{v} ∈ val(∀V_{b}.[\overline{τ}]arg(D))\}
val(∀V_{b}.α) =^{def} \begin{cases}∅ & iff α ∈ V_{b} \\ \{α\} & else \end{cases}

Sequences of types \overline{τ} are mapped to the cartesian product of their components val(∀V_{b}.\overline{τ}) = ∏_{i} val(∀V_{b}.\overline{τ}_{i}).

So clearly val(∀V_{b}.τ) = val(τ) ∩ T m(D, V \ V_{b}). Finally we define the data values which can be used in an eager evaluating language fval(σ) = {v | v ∈ val(σ) and v finite}.

For a term t ∈ T m(S, Var) we get the set of variable occurences vocc(t) = {p|t.p ∈ Var}. The lexicographic order on pathes p, q ∈ ℕ^{∗} is defined by p ⊏_{l} q iff p ⊏_{p} q or p = s.n.u and q = s.m.v with s, u, v ∈ ℕ^{∗} and m, n ∈ ℕ such that n < m. The set of pathes vocc(t) can be ordered by the lexicographic order to a sequence vs(t) ∈ Var^{∗}. A term t ∈ T m(S, Var) can compose with a sequence of terms \overline{t} ∈ (T m(S, Var))^{∗} if the the lenght of sequence \overline{t} coincides with the number of variable occurences in t (t.i. if |\overline{t}| = |vr(t)|) so the resulting term is :

t\overline{t}.p = \{ \begin{matrix}t.p iff t.pdef and t.p ∉ Var \\ t_{i}.q iff p = q′.q and t.q′ = |vs(t)|_{i} \end{matrix}

We call t\overline{t} a decomposition of term t′ iff the term can be represented as t′ = t\overline{t}.

Proposition 1 (decomposition) For every pure type T \overline{τ} we can decompose the schemes s ∈ schm(T \overline{τ}) into s = s′\overline{s} such that :

\begin{aligned}s′ & ∈ & schm(T α_{1} … α_{n}) \\ and \overline{s} & ∈ & schm([τ_{1}/α_{1}, …, τ_{n}/α_{n}]vs(s′)) \end{aligned}

Proposition 2 (full decomposition) For every decomposition of a pure type τ = τ′\overline{τ} we can decompose the schemes s ∈ schm(τ) into s = s′\overline{s} such that :

\begin{aligned}s′ & ∈ & schm(τ′) \\ and \overline{s} & ∈ & schm([\overline{τ}/vs(τ′)]vs(s′)) \end{aligned}

4.2 The connection of algebraic data types and context free languages

The languages of brackets is is an example for the difference between regular and context free languages. The bracklet language B ⊆ {[,]}^{∗} is defined by the grammar Br ::= [Br] | BrBr | [ ]. Herewe will use algebraic data types to represent the bracket language.

      data   Q a = Op A a
      data   A a = Cl a   | Nest Q A a | Juxt A Q a

In the following a type τ will denote a pure data type build by use of the type constructors Q and A and type variable a. We give a translation ^{o} : σ(τ → {[,]}^{∗} which reveals the how data schemes represent words of the bracket language.

Ops^{o} = [ (s)^{o}  Nests^{o} = (s)^{o}
Cls^{o} = ] (s)^{o}  Juxts^{o} = (s)^{o}
a^{o}  = ϵ

Proposition 3 Given a pure type τ build from constructors Q and A then data schemes s ∈ schm(τ) (in short s : τ) have the following properties :

\begin{aligned}s : Q a & ⟹ & s^{o} ∈ B \\ s : A a & ⟹ & [s^{o} ∈ B \end{aligned}

proof by structural induction on s

s =Op s′:Q a So s′ :A a because of the type of Op’s argument. Induction hypothesis applied on s′ gives [s′ ∈ B. Now definition of translation ^{o} gives in case Op the result s^{o} = [s′^{o}.

s =Cl s′:A a So s′ :a which gives the trivial case s′ =a so s′^{o} = ϵ. because of the type of Now by definition of translation ^{o} in case Cl we get [s^{o} = [] ∈ B.

s =Nest s′:A a So s′ :Q A a and we apply decomposition so s′ = s_{1}s_{2} with s_{1} :Q a and s_{2} :A a. Application of induction on s_{1} and s_{2} gives s_{1}^{o} ∈ B and [s_{2}^{o} ∈ B.

So [s^{o} = [s_{1}s_{2} ∈ B.

s =Juxt s′:a a So s′ :A Q a and we apply decomposition so s′ = s_{1}s_{2} with s_{1} :A a and s_{2} :Q a. Application of induction on s_{1} and s_{2} gives [s_{1}^{o} ∈ B and s_{2}^{o} ∈ B.

So [s^{o} = [s_{1}s_{2} ∈ B.

Now we extend this bracket language to the language of plays in a bracketing arena. Definition A bracketing arena is given by a tuple A = (M_{A}, λ_{A}, ⊢_{A} ) where M_{A} is a set of moves. λ : M_{A} → {Q, A} is a bracketing labelling. ⊢_{A} is a relation ⊢_{A} ⊆ M_{A} + {∗} × M_{A} which satisfies :

• ∗ ⊢_{A} m ⟹ λ_{A}(m) = Q

• m ⊢_{A} n ∧ λ_{A}(n) = A ⟹ λ_{A}(M) = Q

The elements (m, n) of the enabling relation ⊢_{A} are called justifiers A play is a sequence of moves where every move is justified by an earlier move in the sequence. Its not necessary that a move must justify its immediate following move. Every arena can be encoded as a data type similar to the bracketing language. We define a data type M a for every move m in the arena and a type A corresponding to the element ∗. For every justifier (m, n) we introduce a data constructor Mjn and for every answer m we introduce a data constructor Mcl.

 data A  = Strtm N ()  if ∗ ⊢_{A} m

for every move m ∈ M_{A} define the following type

 data M a = Mcl a  if λ_{A}(m) = A

Mjn N a  if m ⊢_{A} n ∧ λ_{A}(n) = A
Mjn N M a  if m ⊢_{A} n ∧ λ_{A}(n) = Q

The data schemes of type A correspond to the language of plays. Given a pure data type τ which is A or build by constructors M and type variable a we define a translation ^{o} : schm(τ) → M_{a}^{∗} :

Strtms^{o} = m (s)^{o}  Mcls^{o} = s^{o}
Mjns^{o}  = n (s)^{o}  a^{o} = ϵ

Proposition 4 For a data scheme s :M a the string m(s^{o}) is well opened, closed justified sequence.

4.3 The type constructor termination problem

Now we have a look on the properties of arguments of type constructors. Here are some examples to illustrate the definition

    relevant in a     Tree a   = Leaf a | Brnch (Tree a, Tree a)
    discardable in a  List a   = Nil | Cons (a, List a)
    Cycle is cyclic Cycle a  = C Cycle a

Relevant in a type argument means that every data value of such a type must contain a value of the argument type. For example a value of type Tree Int must contain a integer value. This is only true if we talk about values with finite pathes i.e if a value of type Tree Int must use the Leaf data constructor. Discardability looks like the dual notion (but this fits not exactly). In our example discardability of List in its first argument means a value of type List Int need not to contain a integer value, here Nil is such a value. Now look at the following example T a b = DA a | DB b. In the example the type arguments a and b are discardable by using the data constructors DB or DA. But this didcardability is structured as either or so that both type arguments can’t be discarded. If we add data constructor D with no arguments to the definition of type T a b we get discardability of both type arguments. Obviously for every definition of an algebraic data type there exist infinite data values. We speak about cyclic type constructors if all data values to such a type are infinite.

Here follow two formal characterisations of the properties of type constructors. Both characterisations extent the notions to types and pathes in types. In the following let V ⊆ V be a set of type variables and \overline{α} = α_{1} … α_{n} a sequence of different type variables. Here is the logical characterisation based on the a semantic of algebraic data types.

\begin{aligned}τ term & ⇔ & ∃v ∈ fval(τ) \\ τ ↑ V & ⇔ & ∃v ∈ fval(τ) ∀α ∈ V ¬α occ v \\ τ ↓ α & ⇔ & τ term and ∀v ∈ fval(τ) α occ v \\ T term & ⇔ & T \overline{α} term \\ T ↑ V & ⇔ & T \overline{α} ↑ V \\ T.i ↓ & ⇔ & T \overline{α} ↓ α_{i} \end{aligned}

The second characterisation is a system of recursive set equations which are related to the definition A = (T , a, D, arg, t) of an algebraic data type. The existence, decidability and the uniqueness of a solution to this equation system is an open problem in the general setting. For certain restriction in the generality of algebraic data types exist reduction to well-understood problems.

relevant  must use
T ↓ i  iff ∀D ∈ D_{T} arg(D) ↓ α_{i}
T \overline{τ} ↓ i.p  iff T ↓ i and \overline{τ}.i ↓ p
τ ↓ α  iff α ∈ tv(τ) and ∀p ∈ uses(τ, α) τ ↓ p
discardable may not use
T ↑ V  iff ∃D ∈ D_{T} arg(D) ↑ V
T \overline{τ} ↑ V  iff ∃V′ ⊆ V_{a(T)} and V ⊆ ⋂\{V_{i} | α_{i} ∈ V_{a(T)} \ V′ and \overline{τ}.i ↑ V_{i}\}
τ ↑ V  if tv(τ) ∩ V = ∅
cyclic  no values in a strict language
T ⟲  iff ∀D ∈ D_{T} for \overline{τ} = arg(D) ∃p ∈ pth(\overline{τ}) with
\overline{τ} ↓ p and \overline{τ}.p = T′ and T′ ⟲

Let’s define the structure of a solution for the problem above. A filter F on a set V is a system of subsets of V which is subset closed i.e V ∈ F and V′ ⊆ V ⟹ V′ ∈ F. We denote with F (V) the set of filters for a set V. The sets of discardable type variables to a type constructor obviously form a filter.

A assignment to the type constructor termination problem is a tuple (C, r, d) where C ⊂ T is the set of cyclic type constructors and r : T → P(V) assigns the set of relevant type variables to every type constructor and d : T → F (V) assigns the filter of discardable type variables to every type constructor. A solution to the type constructor termination problem is a assignment satisfying the equations above.

4.4 Termination results

We get the following properties for data values:

• T.i ↓ and T \overline{τ}.i ∈ V_{b} ⟹ fval(∀V_{b}.T \overline{τ}) = ∅

• ∀v ∈ val(∀V_{b}.τ) ∀f : ∀\overline{α}.τ → τ′.∃α ∈ V_{b}.α ∈ \overline{α} and α relocc τ′ ⟹ fv ↑ .

5 A presentation in Martin Löf type theory

The pure types can be presented by use of the wellorder set constructor W. The arguments of W are the set A of type constructors and indexed set B(x) : set [x : A] of selectors for the constructors. In the following we will use the set T (A, B) ≡ W (A, B) to denote the set of pure types. By reuse of notation a pure data type will be written as sup(a, b) : T(A, B) where a : A is the head constructor of the type and the aguments to this constructor are given by b(x) : T(A, B)[x : B(a)]. The value b can be seen as a substitution so we introduce the short form b : Sub(A, B, x) ≡ b(x) : T(A, B)[x : B(a)].

A-formation

\frac{A : set B(x) : set [x : A] C(x) : set [x : A] D(x, y) : set [x : A, y : C(x)] d(x, s, y, z) : T(A, B)[x : A, s : Sub(A, B), y : C(x), z : D(x, y)]}{A(A, B, C, D, d)(t) : set [t : T(A, B)]}

The different parts have the following meaning as parts of an algebraich data type :

• So C(x) is the set of data constructors to each type constructor x.

• D(x, y) is the set of selctors for each data constructor y : C(x).

• The selctors z : D(x, y) are typed by d(x, s, y, z) which gives the type of each selector z of a data constructor y which is instance is given by substitution s : Sub(A, B).

• We introduce the short form A(t) to denote the set of algebraic data values A(A, B, C, D, d)(t) for a pure data type t.

A-introduction

\frac{\begin{matrix}x : A \\ s : Sub(A, B) \\ y : C(x) \\ z(w) : A(d(x, s, y, w))[w : D(x, y]] \end{matrix}}{av(x, s, y, z) : A(sup(x, s))}

The arguments of an data constructor y need to be filled to form a value in an algebraic data type. The arguments z(w) have to be type correct for every selector w which is achieved by use of the typing d.

A-elimination

\frac{E(t, x) : set [t : T(A, B), x : A(t)] t : T(A, B) a : A(t) f(x, s, y, z, w) : E(sup(x, s), av(x, s, y, z)) [x : A, s : Sub(A, B), y : C(x) z(w) : A(d(x, s, y, w))[w : D(x, y] w(v) : E(d(x, s, y, v), z(v))[v : D(x, y)]}{arec(a, f) : E(t, a)}

The non-canonical arec has the following computation rule:

arec(av(a, b, c, e), f) → f(a, b, c, e, (x)arec(e(x), f))

This is reflected in the equality rule.

A-equality

\frac{E(t, x) : set [t : T(A, B), x : A(t)] a : A b : Sub(A, B) c : C(a) e(v) : A(da, b, c, v)[v : D(a, c)] f(x, s, y, z, w) : E(sup(x, s), av(x, s, y, z)) [x : A, s : Sub(A, B), y : C(x) z(w) : A(d(x, s, y, w))[w : D(x, y] w(v) : E(d(x, s, y, v), z(v))[v : D(x, y)]}{arec(av(a, b, c, e), f) = f(a, b, c, e, (x)arec(e(x), f)) : E(sup(a, b), av(a, b, c, e)y)}