Higher Order Algebraic Data Types (Full Paper)

Martin Wehr University of Edinburgh, Department of Computer Science (LFCS) Mayfield Road, Edinburgh EH9 3JZ, Scotland U.K.

       email:  wehr@dcs.ed.ac.uk web:  http://www.ed.ac.uk/home/wehr

July 28, 1998

Abstract

We investigate a natural hierarchy of free Lawvere theories. Algebraic data types turn out to live at the second level of this hierarchy. This is the basis for the main two applications presented here : We solve the problem of finding a general fold algorithm and we introduce the novel programming feature of higher order algebraic data types. These data types are presented with a general type inference method. Further we identify the known program schemes of pattern matching, map, simple fold and general fold in higher order.

1 Introduction

This paper might have also been entitled either “Bananas in Higher Dimensions” following [MFP91, MH95] or “Higher order Polytypic Programming” related to [Mee96]. At the foundation of this paper is the opinion that typeful programming is the righteous way to go. Typeful programming should increase the reuse of software (through all sorts of “poly” type disciplines) and it should also increase the reliability of software (by extending Milner’s slogan “well-typed programs can’t go wrong”). Further as type systems grow more and more complex the programmer should not be bothered with type annotations. This burden should be carried by a type inference system. With these goals in mind the paper develops a hierarchy of type systems with a type inference algorithm and the basic iteration schemes map and fold.

The Idea

First we analyse the structure of algebraic data types (adt’s). This program construct is well known from languages like ML or Haskell. Have a look at the following examples:

                                                List a   =   Nil | Cons a * List a
                                                Tree a   =   Leaf a | Br Tree a * Tree a
                                                Brkt a   =   Opn Brkt (Brkt a) | Cls a

The ingredients of the above adt specification A can be put into an quintuple A = (T , a, D, t, ag). The specification introduces two kinds of new names firstly the type constructors T = { List, Tree, Brkt } and secondly the data constructors D =

                                              { Nil, Cons, Leaf, Brnch, Opn, Cls }. Each of

the type constructors comes with a string of type variables. The number of variables is called the arity of the type constructor and is represented by the function a : T → ℕ. Types are constructed by type variables and type constructors respecting the arity. In a similar way values are constructed by term variables and data constructors respecting the typing. For type correctness we have to consider that every data constructor belongs to a type constructor

     mapList f Nil  = Nil
     mapList f (Cons(a, la))  = Cons(f a, mapList f la)
     mapTree f (Leaf a)  = Leaf (f a)
     mapTree f (Brnch( ta, ta'))  = Brnch (mapTree f ta, mapTree f ta')
     mapBrkt f (Opn bba)  = Opn (mapBrkt (mapBrkt f) bba)
     mapBrkt f (Cls a)  = Cls (f a)
     foldList v f Nil  = v
     foldList v f (Cons(a, la))  = f(a, foldList v f la)
     foldTree f1 f2 (Leaf a)  = f1 a
     foldTree f1 f2 (Br (ta, ta'))  = f2(foldTree f1 f2 ta, foldTree f1 f2 ta')

Figure 1: Iteration schemes for the examples

expressed by a function t : D → T . In our example t( Nil ) = List , t( Leaf ) = Tree , etc. Further each data constructor has a type for its arguments. In our example ag( Cons ) = a * List a , ag( Cls ) = a , etc. The precise formalisation of an adt is the subject of section 3.1.

The point is that we have two sets of constructors living in the specification A, that is the type constructors and the data constructors. In the work [SOW98] of Odersky, Sulzmann and the author we analysed the use of constraint type systems. These kind of type systems use a third level language of constraints on types (examples are: overloading, subtyping, dimensions). In this paper we present constraint adt’s. A constraint adt specification B contains three sets of constructors where the third set deals with constraint names. Of course this can be identified as a step in a hierarchy of adt’s. We define the n^{th}-order adt consisting of n + 1 constructors glued together in a typeful way (section 3.3 and overview figure 4). Type inference and the minimal typing property can be extended to this hierarchy (see section 4).

Iteration Schemes

For each adt there exist the iteration schemes map and fold. See figure 1 for the iteration schemes corresponding to our example adt’s. The algebraic programming approach promotes the iteration schemes as similar to structured programming. While arbitrary recursive functions are considered as harmful like “spaghetti code”.

The careful reader may have noticed that the definition of foldBrkt is missing. To the knowledge of the author fold algorithms of this kind have not been defined to date. Fold was defined for the subset of regular adt’s. In our examples the type List a is regular because it is defined recursively by use of the type List a. Whereas Brkt is not regular because it is define by recursive use of the type constructor Brkt in argument type Brkt (Brkt a). In section 7 we present the general map and fold algorithm and we extend these algorithms to the n^{th}order.

The iteration schemes are also examples for polymorphic functions. The typing discipline used in ML introduces difficulties in case of the Brkt-type which is an example of a non-regular type. For instance the Opn-branch of function mapBrckt would not be accepted by type inference because the two recursive uses of mapBrckt have different types. The general fold algorithm which we present can’t be typed in impredicative polymorphism.

2 Background

This section gives a background on strings and free theories. Most of this material can be found in [Wag] so we mainly introduce notation here. The structures in strings will be used in the definition of free theories.

We will see in section 3 that the structure of free theories will be used to define algebraic data types (adt). Formalising this use of simple structures for defining complex structures will eventually lead to the hierarchy of higher order adt’s.

2.1 Strings

For each set (alphabet) T we can construct the free monoid T^{∗} of strings ranged over by u and v. The associative multiplication of this monoid is the concatenation of strings and the unit is the empty string ϵ. We denote by |u| ∈ ℕ the length of a string u. We call the obvious function ū : [|u|] → T the representation of the string where we use notation [n] := {1, …, n} for n ∈ ℕ. So u_{i} = ū(i) is the i-th letter occuring in the string. A function on alphabets f : T → S induces a function on strings f^{∗} : T^{∗} → S^{∗} by defining f^{∗}(u)_{i} := f(u_{i}). Notice that, since 1^{∗} ≃ ℕ, the length function | | : S^{∗} → ℕ is the string function !_{T}^{∗} for the unique function !_{T} : T → 1 to a singleton set 1.

2.1.1 String Morphisms

There is a one-to-one correspondence between a string u and its representation \overline{u}. Likewise we define a string morphism m : u → v by explaining its representation \overline{m}. A string morphism is representation is a map m̄ : [|u|] → [|v|] with property ū = v̄ ∘ m̄, that is u_{i} = v_{m̄(i)} for each i ∈ [|u|]. So the string u is built by letters occurring in v and m keeps track of the position of the used letters. Given string morphisms m : u → v, m : u′ → v and m′′ : u′′ → v′′ there are two construction on morphisms :

mm′ : uu′ → v with

\overline{mm′}(n) = \{ \begin{matrix}m(n) iff n ∈ [|u|] \\ m′(n − |u|) iff |u| < n \end{matrix}

m × m′ : uu′′ → vv′′ with

\overline{m × m′′}(n) = \{ \begin{matrix}m(n) iff n ∈ [|u|] \\ m′′(n − |u|) + |v| iff |u| < n \end{matrix}

The string morphism are generated by the trivial morphisms null_{t} : ϵ → t and id_{t} : t → t for each letter t ∈ T of the alphabet and the juxtaposition mm′ and the multiplication m × m′′ of morphisms. We denote the set of string morphisms by Mor_{T}.

2.1.2 Operation on Families

Strings u ∈ T^{∗} operate on families of sets {A_{t}}_{t∈T} by defining A^{u} := A_{u_{1}} × ⋯ × A_{u_{|u|}}. Given a family of functions {f_{t} : A_{t} → B_{t}}_{t∈T} we can define a function f^{u} : A^{u} → B^{u} by the mapping (a_{u_{1}}, …, a_{u_{|u|}}) ↦ (f_{u_{1}}(a_{u_{1}}), …, f_{u_{|u|}}(a_{u_{|u|}})).

2.2 Trees

For every alphabet S we define S^{#} := S^{∗} × S. Its elements (u, s) ∈ S^{#} will be used as a sorting of a generator.

2.2.1 Signatures

A S-sorted signature Σ consists of a set |Σ| of generators ranged over by f and a sorting f : (u, s) for each generator. If we take the singleton 1 as sort set S then we get a signature Σ with arity 1^{#} = 1^{∗} ×1 ≃ ℕ. So a 1-sorted signature looks like Σ = {f : n | f ∈ |Σ|}. We call the elements of |Σ| sometimes constructors.

2.2.2 Terms

Each S-sorted signature specifies a set of terms T m_{Σ}. In more detail for a string u ∈ S^{∗} we define X^{(u)} := {x_{i} : u_{i} | i ∈ [|u|]} to be the set of variables associated to the string u. For each sort s ∈ S we define the set T m_{Σ}^{s}(u) of terms consists of the elements :

(var) x_{i} : u_{i} ∈ X^{(u)} with u_{i} = s.

(constr) ft_{1} … t_{n} for f : (u′, s) ∈ Σ with |u′| = n and t_{i} ∈ T m_{Σ}^{u′_{i}}(u) for i ∈ [n]

We denote an element by either t ∈ T m_{Σ}^{s}(u) by t : s or u ⊢ t : s.

2.2.3 Free Theories

We define the set T_{Σ} which is called the free S-sorted theory (or Lawvere theory). The sorted terms define a family {T m_{Σ}^{s}}_{s∈S} so we are able to use the operation of strings u ∈ S^{∗} on the family. We define the set T_{Σ}(u, v) for u, v ∈ S^{∗} by T_{Σ}(u, v) := (T m_{Σ}(u))^{v} = T m_{Σ}^{v_{1}}(u) × ⋯ × T m_{Σ}^{v_{|v|}}(u). So each free term

tt′  juxtaposition or pairing of terms
t • t′ composition of terms
t ⊑ t′ instance relation on terms
t × t′ Pairing without sharing of variables
t ⊲ t′ Substitution witnessing the instance relation
t ↑ t′ upper boundedness in instance relation
t ⊔ t′ most general unification of terms
twt′ substitution witnessing the mgu

Figure 2: structures in the free theory T_{Σ}

t ∈ T_{Σ}(u, v) (in short u ⊢ t : v) is a string of sorted terms u ⊢ t_{i} : v_{i}.

Further we define the set u ↓ T_{Σ} := ⋃_{v∈S^{∗}} T_{Σ}(u, v) caring just for the sorting of the variables and the set T_{Σ} ↓ v := ⋃_{u∈S^{∗}} T_{Σ}(u, v) caring just for the sort of the term.

The free theory has more structure (T_{Σ}, •, ⊑) with a partially defined composition • : T_{Σ} × T_{Σ} ⇀ T_{Σ} and a partial order ⊑⊆ T_{Σ} × T_{Σ} called the instance order. For sorted terms u ⊢ t : v and w ⊢ t′ : u the composition t • t′ is defined by substituting the variables x_{i} : u_{i} occuring in t by the terms t′_{i} ∈ T m_{Σ}^{u_{i}}(w). Note that the result of the composition is sorted as w ⊢ t • t′ : v. This defines the instance order by t ⊑ t′′ iff there is a term t′ with t • t′ = t′′. This unique term t′ := t ⊲ t′′ is called the witness of the instance relation. The least upper bound t ⊔ t′ of two term in this order is known as their unification.

2.2.4 Theory Morphisms

A function of signatures f : Σ → Σ′ from a S-sorted signature Σ to a T -sorted signature Σ′ consists of an alphabet map f_{a} : S → T and a sort-compatible constructor map f_{c} : |Σ| → |Σ′|. That is for all constructors f : (u, s) ∈ Σ we get result sorting f_{c}(f) : (f_{a}^{∗}(u), f_{a}(s)) ∈ Σ′.

A function of signatures f : Σ → Σ′ induces a function on terms f^{tm} : T m_{Σ} → T m_{Σ′} . Yhe function is define by structural induction on the two cases :

(var) f^{tm}(x_{i}) = x_{i}

(constr) f^{tm}(ft_{1} … t_{n}) = f_{c}(f)f^{tm∗}(t_{1} … t_{n})

More specifically we get a sort compatible map on the terms f^{tm} : T m_{Σ}^{t}(u) → T m_{Σ′}^{f_{a}(t)}(f_{a}^{∗}(u)). By using the the equality T_{Σ} = T m_{Σ}^{∗} we extend function from terms to theories by setting f^{t} := (f^{tm})^{∗} : T_{Σ} → T_{Σ′}.

2.2.5 Sub-Theories

A sub-theory is a subset T′ ⊆ T_{Σ′} where t, t′ ∈ T′ implies tt′, t • t′ ∈ T′ if juxtaposition and composition is defined in T_{Σ′}. So the length function | | : T′ → ℕ and the T -sorting discipline T′(u, v) (by assumption Σ′ is a T -sorted signature) are just restrictions according to the subset relation T′ ⊆ T_{Σ}. Obviously the image T′ := img(f^{t}) of the theory morphism f^{t} induces a sub-theory. In this case we have a Ssorting of terms t ∈ T′ by u ⊢ t : v if there is a term t′ ∈ T_{Σ}(u, v) with f^{t}(t′) = t. Note that the T - sorting to term t is unique while the S-sorting is not necessary so.

2.2.6 Linear Terms

A term t ∈ u ↓ T_{Σ} is called linear iff every variable x_{i} : u_{i} occurs exactly once in t. We define the multiplication t×t′ of terms as the pairing without sharing variables. So for u ⊢ t : v and u′ ⊢ t : v′ we get sorting uu′ ⊢ t × t′ : vv′. Linear terms are closed under multiplication.

Note that for each string morphism m : v → u with representation m̄ : [|v|] → [|u|] we have an element \underline{m} := x_{m̄(1)} … x_{m̄(|v|)} ∈ T_{Σ}(u, v) built as a string of variables. We denote by \underline{u} the term associated to the identity string morphism id_{u} : u → u.

For a type string τ = τ_{1} … τ_{n} ∈ T y_{A}(n, )

right of typing  τ ⊢ …  typotheses  x_{1} : τ_{1}, …, x_{n} : τ_{n}
left of typing  … ⊢ v : τ cartesian product type τ_{1} × ⋯ × τ_{n}
right of composition … τ′ • τ … substitution  {α_{1} ↦ τ_{1}, …, α_{n} ↦ τ_{n}}

Figure 3: interpretation of type strings

Given a term u ⊢ t : v the linear representation to the term is given by a linear term u′ ⊢ t′ : v and a string morphism m : u′ → u such that t = t′ • \underline{m}. So in the linear term t′ each variable x_{i} : u′_{i} for i ∈ [|u′|] occurs exactly once. We will name the string u′ as the frontier of the term t and the morphism m will be called the frontier representation.

If we order the variables according to their occurrence from left to right we get a function lin : T_{Σ} → LT_{Σ} × Mor_{S} where LT_{Σ} is the set of linear terms of a S-sorted signature Σ. The first projection lt : T_{Σ} → LT_{Σ} extracts the linear term associated to a term. The second projection gives the frontier representation of any term frnt : T_{Σ} → Mor_{S}.

If we add the constants {⊥_{s} | s ∈ S} to the signature Σ we get the free theory P T_{Σ} of partial terms. We define the matching order t ⊑^{m} t′ on partial term by the axiom ∀t ∈ P T_{Σ} ↓ s.⊥_{s} ⊑^{m} t and structural induction. Obviously there is an reflective order homomorphism between linear terms with the instance order (LT_{Σ}, ⊑^{i}) and partial ground terms with the matching order (ϵ ↓ P T_{Σ}, ⊑^{m}).

3 Algebraic data types (adt)

First we define algebraic data types. Next we will explicitly define second order adt’s. Both definitions consists in a definition of a specification (similar to the signatures of free theories) and the definition of the values induced by this specification (similar to the terms of a free theory). In the definition of free theories we used the structure of strings as the sorting. Something very similar will happen with the structure of the types used in in the definition of an adt. The observation that the types of an adt are the values of an adt of previous order will lead to the hierarchy of adt’s.

Method

The main result in this section is the general construction of values starting from a specification. To this end we define two signatures: firstly the untyped signature giving the free theory of pre-values, secondly the explicitly typed signature giving the the free theory of explicitly typed values. We will see that the erasure of type annotations is a theory morphism between these free theories. Finally the image of the erasure morphism defines the implicitly typed values of an adt. So the values are a sub-theory of the prevalues.

3.1 First Order ADT’s

3.1.1 Specifications

The specification of an adt is a quintuple A = (T , a, D, t, ag) where T is the set of type constructors and D is the set of data constructors. The function a : T → ℕ is the arity in the signature ΣT with |ΣT | = T and ΣT := {T : a(T) | T ∈ T }. We call the free theory T y_{A} := T_{ΣT} the types of the adt A. The function t : D → T gives the sort of a data constructor. The function ag : D → T y_{A} gives the argument type of a data constructor. The argument type of a data constructor C ∈ D can use only the n = a(T) type variables of its sort T = t(C). So for all constructors C ∈ D the restriction ag(C) ∈ a(t(C)) ↓ T_{Σ} is needed.

Order Specification Generators Values Types

Constraints

n = 0  Σ  |Σ|  T_{Σ}  arities 1^{∗} ≃ ℕ  trivial 1
n = 1  A  T , D  V al_{A} = img(∥ ∥)  T y_{A} = T_{ΣT}  arities 1^{∗} ≃ ℕ
n = 2  B  C, T , D  V al_{B} = img(∥ ∥) cT y_{B} = V al_{B_{tadt}} Cnst_{B} = T_{ΣC}

⋮

n − 2  S^{−−}
n − 1  S^{−}
n S GS_{0}, …, GS_{n} V al_{S} = img(∥ ∥) T y_{S} = V al_{S^{−}} Cnst_{S} = T y_{S^{−}}
= V al_{S^{−−}}

where ∥ ∥: T_{Σ^{exp}} → T_{Σ^{pre}} is the erasure function and Σ^{exp} is the explictly typed signature and Σ^{pre} is the untyped pre-value signature

Figure 4: Structures in higher order algebraic data types

3.1.2 Values

We define the T y_{A}-sorted signature ΣD^{exp} of explicitly typed data constructors by :

\begin{aligned}ΣD := & \{Cτ : (τ_{C} • τ, T τ) | C ∈ D with \\ & ag(C) = τ_{C}, t(C) = T, τ ∈ T y_{A} ↓ a(T)\} \end{aligned}

We further get the untyped arity signature ΣD^{pre} for pre-values by |ΣD^{pre}| = D and ΣD^{pre} := {C : |ag(C)| | C ∈ D}

Remember that the length function | | : T y_{A} = T_{ΣT} → ℕ ≃ 1^{∗} is the string function (!_{T y_{A}})^{∗} induced by the unique function !_{T y_{A}} : T y_{A} → 1 to the singleton 1. So we get a function of signatures f^{impl} : ΣD^{exp} → ΣD^{pre}. This is a function from a T y_{A}-sorted signature to a 1-sorted signature : The alphabet part is defined as f_{a}^{impl} :=!_{T y_{A}} and the constructor part f_{c}^{impl} : |ΣD^{exp}| = D × T y_{A} → |ΣD^{pre}| = D is just defined by the first projection f_{c}^{impl}(Cτ) = C. So we get a morphism on free theories ∥ ∥:= (f^{impl})^{t} : T_{ΣD^{exp}} → T_{ΣD^{pre}} called the erasure. The elements of the image image of the erasure V al_{A} := img(∥ ∥) are called the values of the adt A or the implicitly typed data terms.

3.1.3 Composition

A value v ∈ V al_{A} has a typing τ ⊢ v : τ′ (alternative notation v ∈ V al_{A}(τ, τ′)) iff there is an explicitly typed value v′ ∈ T_{ΣD^{exp}}(τ, τ′) with erasure ∥ v′ ∥= v. The meaning of implicit typedness is the universal instanciation property.

Proposition 1 (Universal Instanciation) Given a value v with a typing τ ⊢ v : τ′ and a any type τ′′ so that composition ττ′ • τ′′ is well defined then we get a new typing of the same value τ • τ′′ ⊢ v : τ′ • τ′′.

3.1.4 Composition

The values v, v′ ∈ V al_{A} ⊆ T_{Σ^{pre}} live in a free theory. So there is a partial defined composition v • v′. The composition is defined for instance if the values coincide on a type τ like τ ⊢ v and v′ : τ. The erasure guaratees in that case that the composite v • v′ is a value v • v′ ∈ V al_{A}. But composition of implicitly typed values is more flexible. If the typing τ ⊢ v and v′ : τ′ is unifyable (τ ↑ τ′) then by universal instanciation there exists typings τ ⊔ τ′ ⊢ v and v′ : τ ⊔ τ′ resulting in a well-typed composite v • v′ ∈ V al_{A}. If we know just the typing τ ⊢ v then exactly the values v′ ∈ V al_{A}( , ↑ τ) compose, where we define V al_{A}( , ↑ τ) := ⋃_{typ⊑τ′} V al_{A}( , τ′).

3.2 Second Order ADT’s

3.2.1 Specification

A second order adt specification is a 7-tuple B = (C, ac, T , tt, tag, D, td, dag). As a synonym we use the name constraint adt. We have three sets of generators; the constraint names C, the type constructors T and the data constructors D. The quintuple B_{tadt} = (C, ac, T , tt, tag) must be an adt. We call the free theory D ∈ Cnst_{B} := T_{ΣC} = T y_{B_{tadt}} the constraints of B. We call τ ∈ cT y_{B} := V al_{B_{tadt}} the constrained types of B. We use the formula D ⇒ τ :: D as the alternative denotation for for τ ∈ cT y_{B}(D, D′) = V al_{B_{tadt}}(D, D′) to state that the type variables α_{i} :: D_{i} occuring in type τ are constrained and the types τ_{j} :: D′_{j} are constrainedy. So types compose τ • τ′ only iff there is a constraint D on the types D ⇒ τ and τ′ :: D

3.2.2 Second Order Values

The function td : D → T gives the sorting of data constructors and the function dag : D → cT y_{B} gives the constrained type of a data constructor. Given a data constructors C ∈ D then only the constrained type variables α_{i} :: D_{i} can occur in the argument type τ_{C} = dag(C). Where D is the type constructor constraint argument D = tag(T) associated to the type constructor that is T = td(C). So the specification satisfies for any data constructor C ∈ D the property dag(C) ∈ tag(td(C)) ↓ cT y_{B}.

Again (as in section 3.1.2) we define the signature of explicitly typed data constructors :

\begin{matrix}ΣD^{exp} := \{Cτ : (τ_{C} • τ, T τ) | C ∈ D, τ_{C} = dag(C), \\ T = td(C), τ ∈ cT y_{B} ↓ D, tag(T) ⊑ D\} \end{matrix}

Note that we have to restrict the instantiation type τ :: D to a well constrained type. We get the usual pre-value signature ΣD^{pre} and the erasure ∥ ∥: T_{ΣD^{exp}} → T_{ΣD^{pre}} as before. So we define the values of B as the image of the erasure V al_{B} := img(∥ ∥) and get again the notion of a typing τ ⊢ v : τ′. If the types in the typing are constrained like D ⇒ τ and D ⇒ τ′ :: D′ then we denote a constrained typing by D ⇒ τ ⊢ v : τ′ :: D′.

3.3 Higher Order ADT’s or The Full Hierarchy

We will now define the notion of n^{th}-order adt. for every adt specification S of n^{th}-order we will define the set of values V al_{S} of n^{th}-order. The set of values of n^{th}-order will be a sub-theory of a free theory where the sorts are values of order n − 1. This subtheory will be induced by the image of an erasure-like theory morphism.

3.3.1 Specification

We define the specification of an n^{th}-order adt inductively. The specification of order 0 consists just of an arity signature ΣS. So the values of order 0 are just the free terms T_{ΣS} and the types are the arities 1^{∗} ≃ ℕ.

In the case n ≥ 1 a specification S consist of a specification S^{−} of order n − 1 extended by a triple (GS_{n}, st_{n}, agt_{n}), where : GS_{n} is a set of generators, st_{n} is the sorting of generators and agt_{n} is the argument typing of generators. The generator sorting is a function st_{n} : GS_{n} → GS_{n−1} where GS_{n−1} is the generator set of the extension for S^{−} in case n > 1 or the set of constructors |ΣS| in the case n = 1 so we set GS_{o} := |ΣS|.

The argument typing is a function agt_{n} : GS_{n} → V al_{S^{−}}. We call the values of specification S^{−} the types of specification S (in short T y_{S} := V al_{S^{−}}). Again we have to restrict the sorting D ⊢ τ of an argument type τ = agt_{n}(f) to an generator f ∈ GS_{n}. We restrict the variables D used in τ such that D = agt_{n−1}(st_{n}(f)). In short the argument type agt_{n} has to statisfy the restriction for all generators f ∈ GS_{n}.agt_{n}(f) ∈ T y_{S} ↓ agt_{n−1}(st_{n}(f)). As mentioned above, the types for the adt of order zero are the arities 1^{∗} ≃ ℕ. So we define agt_{0} : GS_{o} = |ΣS| → ℕ to be the arity of the constructors f ∈ |ΣS|.

3.3.2 Values

We will now define the explicitly typed signature ΣS^{exp} and the arity signature of pre-values ΣS^{pre}. We will see that ΣS^{exp} is a T y_{S}-sorted signature.

With this at hand we define the erasure ∥ ∥: T_{ΣS^{exp}} → T_{ΣS^{pre}} and define the values of S as the image of the erasure V al_{S} := img(∥ ∥) which we call the set of implicit typed values of n^{th}-order.

To define the arity signature ΣS^{pre} we use the fact that T y_{S} is a sub-theory so we can apply the length function | | : T y_{S} → ℕ and get a definition ΣS^{pre} := {f : |agt_{n}(f)| | f ∈ GS_{n}} by use of the argument typing function agt_{n} : GS_{n} → T y_{S}.

To define the T y_{S}-sorted signature ΣS^{exp} we use the fact that the specification S^{−} consists of specification S^{−−} of order n − 2 and an extension (GS_{n−1}, st_{n−1}, agt_{n−1}) with agt_{n−1} : GS_{n−1} → V al_{S^{−−}} = T y_{S^{−}}. We will define the constraints of specification S as Cnst_{S} := V al_{S^{−−}} = T y_{S^{−}}. We need further that T y_{S} = V al_{S^{−}} is a sub-theory so there exists a partially defined composition τ •_{S^{−}} τ′ for types τ, τ′ ∈ T y_{S}. Now V al_{S^{−}} is a free T y_{S^{−}}- sorted theory or by synonyms this means T y_{S} is a Cnst_{S}-sorted theory. We abbreviate type τ ∈ T y_{S}(D, D′) with constraints D, D′ ∈ Cnstr_{S} as D ⇒ τ :: D′. Now composition τ •_{S^{−}} τ′ is defined if D ⇒ τ and τ′ :: D′ with D ⊑_{S^{−−}} D′ where we denote by ⊑_{S^{−−}} the instance order in the theory of constraints Cnstr_{S}.

Altogether we can define the explicitly typed signature as :

ΣS^{exp} := {fτ : (τ_{f} •_{S^{−}} τ, T τ) | f ∈ GS_{n}, agt_{n}(f) = τ_{f} ∈ T y_{S}, st_{n}(f) = T ∈ GS_{n−1}, τ ∈ T y_{S} ↓ D, agt_{n−1}(T) ⊑_{S^{−−}} D}

4 Type Inference

4.1 Well-Typedness

Now we use our notation to state some well known fact about the well typed values of algebraic data types.

Proposition 2 (Typing Completion) Given a value v ∈ V al_{A} which is typed v : τ then there is exactly one type τ′ with τ′ ⊢ v : τ. Further for any type τ′′ such that v : τ • τ′′ we get the typing τ′ • τ′′ ⊢ v : τ • τ′′

In the same way any incomplete typing τ ⊢ v for a value v ∈ V al_{A} can be uniquely completed to τ ⊢ v : τ′. And composition from right τ • τ′′ ⊢ v acts as before τ • τ′′ ⊢ v : τ′ • τ′′.

Corollary 1 (Composition of Values) Given a typing τ ⊢ v • v′ : τ′ there is a unique type τ′′ w such that τ′′ ⊢ v : τ′ and τ ⊢ v′ : τ′′.

Definition 1 (Minimal Typing) A typing τ ⊢ v : τ′ is called minimal iff any other typing τ_{1} ⊢ v : τ_{2} of the value v is a super instance ττ′ ⊑ τ_{1}τ_{2} of the original typing. (We assume w.o.l.g. that |τ| = |τ_{1}|)

For example α ⊢ x : α is a minimal typing. A non-trivial minimal typing is τ_{C} ⊢ C\underline{m} : T \underline{n} where the specification of the adt gives the data τ_{C} = ag(C), T = t(C), m = |τ| and n = a(T).

Proposition 3 (Construction of Minimal Typings) If τ_{1} ⊢ v : τ_{2} and τ_{1}′ ⊢ v′ : τ_{2}′ are minimal typings, then we can construct new minimal typings by :

composition if τ_{1} and τ_{2}′ unifiable then τ_{1}′ • (τ_{1}wτ_{2}′) ⊢ v • v′ : τ_{2} • (τ_{1}wτ_{2}′)

juxtaposition if τ_{1} and τ_{1}′ unifiable then (τ_{1} ⊔ τ_{1}′) ⊢ vv′ : τ_{2}τ_{2}′ • (τ_{1}wτ_{1}′)

Proposition 4 (Minimal Typing) For each value v ∈ V al_{A} there exists a minimal typing τ ⊢ v : τ′.

4.2 Unification Algorithm

For two terms n ⊢ t and m ⊢ t′ we define the most general unification without sharing variables n+m ⊢ t ⊔^{⊲} t′. In order to do this we have to rename the occuring variable in t so that they are disjoint to the variables occuring in t′ as follows : m+n ⊢ sh_{m}t. So we get the definition of the most general unification without sharing by setting t ⊔^{⊲} t′ := (sh_{m}t) ⊔ (inj_{n}t′). We define the left witness t w^{⊲} t′ and the right witness t w^{⊳} t′ by setting t w^{⊲} t′ := sh_{−m}((sh_{m}t) ⊲ (t ⊔^{⊲} t′)) and

t w^{⊳} t′ := (inj_{n}t′) ⊲ (t ⊔^{⊲} t′). As a result the following

equations hold t • (t w^{⊲} t′) = t′ • (t w^{⊳} t′) = t ⊔^{⊲} t′. In the figure 5 the algorithm producing nshun(t, t′) =

(t w^{⊳} t′)(t w^{⊲} t′) is given.

sh_{m} : T_{Σ}(n, k) → T_{Σ}(m + n, k)

sh_{m}t = rename occuring variables x_{i} ↦ x_{m+i} for i ∈ [n] inj_{m} : T_{Σ}(n, k) → T_{Σ}(m + n, k)

inj_{m}t = do nothing: each term n ⊢ t is also a term m + n ⊢ t

nshun_{Σ} : T_{Σ}(n, k) × T_{Σ}(m, k) ⇀ T_{Σ}(n + m, n + m)

nshun(t, t′) = unify(sh_{m}t, inj_{n}t′) unify_{Σ} : T_{Σ}(n, k) × T_{Σ}(n, k) ⇀ T_{Σ}(n, n)

unify(t, t′) = unfh(t, t′, \underline{n})

unfh(x_{i}, t′, t′′)  = unfh(t′, x_{i}, t′′)
unfh(t, x_{i}, t′′)  = if x_{i} occurs in t then error “occur failure”

else if t′′_{i} = x_{i} then (t′′|x_{i} ↦ t) else (t′′|x_{i} ↦ unify(t, t′′_{i}))

unfh(ft, ft′, t′′)  = unfh(t, t′, t′′)
unfh(t_{1}t_{2}, t′_{1}t′_{2}, t′′) = for |t_{1}| = |t′_{1}| ≥ 1 and |t_{2}| = |t′_{2}| ≥ 1

unfh(t_{1}, t′_{1}, unfh(t_{2}, t′_{2}, t′′))

Figure 5: unification algorithm

4.3 Inference Algorithm

The non-sharing unification is used to define a type inference algorithm for adt’s.

The algorithm in figure 6 takes a pre-value v ∈ T_{ΣD} as argument and terminates iff it is a value v ∈ V al_{A} otherwise it will raise an error. The result in case of termination tinf(v) = (τ, τ′) will be the minimal typing τ ⊢ v : τ′.

4.4 Constrained Type Inference

Given  a  constrained  adt  B  =

(C, ac, T , tt, tag, D, td, dag) we can extract two adt’s living in that specification. There are the type adt B_{tadt} = (C, ac, T , tt, tag) and the data adt B_{dadt} = (T , ab, D, td, dag) with ab = | | ∘ tag : → ℕ. Previous paragraph 4.3 presented a type inference procedure with minimal typing result for each adt. We use the algorithms tinf_{B_{tadt}} and tinf_{B_{dadt}} to define a constrained type inference algorithm ctinf_{B} see figure 7

Constrained inference algorithm can be applied to a pre-value v ∈ T_{ΣD}. In case of termination the result ctinf_{B}(v) = (D, τ, τ′, D′) gives a minimal constrained typing D ⇒ τ ⊢ v : τ′ :: D′. The minimality property is just a corollary which follows by application of minimality for adt’s B_{tadt} and B_{dadt}.

4.4.1 Counterexample

The following example shows that constraint checking is necessary. Because even if two types τ and τ′ are well constrained we cannot expect that the unified type τ ⊔τ′ is again well constrained. Take for example the type constructors D ⇒ T, T′ :: D′ and T′′ of arity two. The following two types are well constrained D ⊢ T′′(T α)α and e ⊢ T′′βT′ with β :: e unconstrained by a constraint variable e. The types are unifiable to the resulting unified type T′′(T T′)T′ by the witnessing substitution {α ↦ T′, β ↦ T T′}. But the result is not well-constraint because the variable α :: D is bound to the type T′ :: D′ so the constraint clash occurs in T T′ with D ⇒ T and T′ :: D′. tinf_{A} : T_{ΣD}(n, m) ⇀ T y_{A}(k, n) × T y_{A}(k, m) tinf(v) = tinfh(\underline{n}, v)

tinfh(τ, x_{i}) = (τ, τ_{i})
tinfh(τ, v_{1}v_{2}) = with |v_{1}| ≥ 1 and |v_{2}| ≥ 1

(τ_{1}, τ_{1}′) := tinfh(τ, v_{1}); (τ_{2}, τ_{2}′) := tinfh(τ, v_{2}); return(τ_{1} ⊔ τ_{2}, τ_{1}′τ_{2}′ • (τ_{1}wτ_{2}))

tinfh(τ, Cv) = let T = t(C) and τ′ = ag(C)

(τ_{1}, τ_{1}′) := tinfh(τ, v);

return(τ_{1} • (τ′ w^{⊳} τ_{1}′), T (τ′ w^{⊲} τ_{1}′))

Figure 6: type inference for adt’s

ctinf_{B} : T_{ΣD} ⇀ Cnst_{B} × cT y_{B} × cT y_{B} × Cnst_{B}

ctinf(v) = (τ, τ′) := tinf_{B_{tadt}}(v); (D, D′′D′) := tinf_{B_{dadt}}(ττ′);

so that D ⇒ τ :: D′′ and D ⇒ τ′ :: D′ return(D, τ, τ′, D′);

Figure 7: algorithm for constrained type inference

4.5 General Type Inference

The general type inference algorithm for adt’s of n^{th}- order is built by following observation. The quintuple S_{adt} = (GS_{n−1}, sa_{n−1}, GS_{n}, st_{n}, agt_{n}) with sa_{i} = | |∘ agt_{i} : GS_{i} → ℕ for i ∈ [n] forms an adt. So in case n = 1 we can define the type inference algorithm as tp_{S} = tinf_{S_{adt}} : T_{ΣS^{pre}} ⇀ T y_{S} × T y_{S}. In case n > 1 we define the general algorithm as :

tp_{S} : T_{ΣS_{n}} ⇀ lT p_{S} × rT p_{S} with lT p_{S} := lT p_{S^{−}} × T y_{S} and rT p_{S} := T y_{S} × rT p_{S^{−}} tp_{S}(v) = (τ, τ′) := tinf_{S_{adt}}(v); (t, t′_{1}t′_{2}) := tp_{S^{−}}(ττ′);

with |t′_{1}| = |τ| and |t′_{2}| = |τ′| return((t, τ), (τ′, t′_{2})); Note that type inference on the adt S_{adt} is in fact the following partial function tinf_{S_{adt}} : T_{ΣS^{pre}} ⇀ T_{ΣS_{n−1}} × T_{ΣS_{n−1}} with the signature ΣS_{n} := {f : sa_{n}(f) | f ∈ GS_{n}}. So tinf_{S_{adt}} works on pre-values v ∈ T_{ΣS^{pre}} and results in case of termination in a pre-typing τ ⊢ v : τ′ using pre-types τ, τ′ ∈ T_{ΣS_{n−1}}. To form a typing from this pre-typing we have to infer the well-constrainedness of the pre-types τ, τ′. But well-constrainedness inference is just tp_{S^{−}} the type inference of lower order. By n applications of the minimal typing property of adt’s we get then in case of termination tp_{S}(v) = (t, t′) a minimal typing t ⊢ v : t′.

5 Program schemes

Along with the definition of an adt come some program schemes which define functions on the values of the adt. We will look at the following schemes :

• pattern matching

• map

• simple fold

• general fold

Fold functions for simple case as the data types as List or Tree are well known in the functional programming community. But the general construction of a fold associated to any adt was to date an open problem. Here we will define such a fold as a term transform on pre-values which can be polymorphically typed.

In a next step we look at the program schemes of higher order adt’s.

5.1 Algebraic Functions

We deal with well-typed functions f : V al_{A} ⇀ V al_{A} of algebraic values. A function is well-typed (in short: f : τ → τ′) if its well defined as a map of sets f : V al_{A}(ϵ, τ) → V al_{A}(ϵ, τ′). A function f : τ → τ with n ⊢ ττ′ is polymorphic iff the restrictions fτ′′ : τ • τ′′ → τ′ • τ′′ for types τ′′ : n is well defined. In that case it satisfies the invariant fτ_{1}v = f(τ_{1}•τ_{2})v for all values v : τ • τ_{1}. Any value τ ⊢ v : τ′ with n ⊢ ττ′ induces a polymorphic function \underline{v} : τ → τ′ by composition from the left \underline{v}(v′) := v • v′

5.2 Pattern Matching

Pattern matching is a programming scheme which is another source of polymorphic functions. Given a type constructor T ∈ T we define the associated set of data constructors D_{T} := {C ∈ D | t(C) = T }. Further we use the argument type τ_{C} as a short form for τ_{C} = ag(C).

Given a result type n ⊢ τ with arity n = a(T) of type constructor T and a family of polymorphic functions f⃗ := {f_{C} : τ_{C} → τ}_{C∈D_{T}} we get the polymorphic pattern function T [f⃗] : T \underline{n} → τ by defining :

T [f⃗](Cv) := f_{C}v

5.3 General Pattern Matching

A set of patterns P ⊆ LT_{ΣD} ↓ 1 is a set of linear pre-values with a type τ such that all patterns p ∈ P can be typed p : τ (in short: P : τ). The linearity of a pattern p gives a typing τ_{p} ⊢ p of its frontier. We are interested in two properties of a pattern set P :

P non-overlapping ⇔ ∀v : τ|{p | p ⊑ v}| ≤ 1
P covering  ⇔ ∀v : τ|{p | p ⊑ v}| ≥ 1

Given a non-overlapping covering pattern set P : τ and a family of functions f⃗ := {f_{p} : τ_{p} → τ′}_{p∈P} we define the general pattern matching function P [f⃗] : τ → τ′. To a value v : τ we get the result by P [f⃗]v := f_{p}(p ⊲ v) where p ∈ P is the unique pattern p ⊑ v given by uniqness and covering. The general pattern matching is polymorphic iff the family of functions f⃗ is polymorphic.

5.4 General Map

Here we will define the map function for each type τ ∈ T y_{A} in an adt A.

Recall that we denote with \underline{n} the term α_{1} … α_{n} ∈ T y_{A}(n, n). Note that a string morphism m : u → v in the monoid 1^{∗} is just a string w ∈ [|v|]^{∗} with |w| = |u|. So the term \underline{m} is just \underline{w} = α_{w_{1}} … α_{w_{|w|}} ∈ T y_{A}(|v|, |w|). Any implicitly typed value v ∈ τ ↓ V al_{A} is also an arity term v ∈ |τ| ↓ T_{ΣD} so we have the notion of the frontier of this term frnt(v) = w ∈ [|τ|]^{∗} (recall paragraph 2.2.6).

Proposition 5 (Unique Decomposition) Given a type n ⊢ τ and a minimal typing \underline{n} ⊢ v : τ then for any type τ′ ⊑ τ with m ⊢ τ′ there is a unique typed value \underline{m} ⊢ v′ : τ′. We take the linear representation lin(v′) = (v′′, w) of value v′. Then we get v′′ ⊑ v and minimal typing \underline{n} ⊢ (v′′ ⊲ v) : \underline{w} • (τ′ ⊲ τ).

We use the notion of unique decomposition to define some operations in adts. We define the restriction

T [f⃗] : T \underline{n} → τ  pattern matching

for a family of functions f⃗:= {f_{C} : τ_{C} → τ}_{C∈D_{T}} on argument types τ_{C}

P [f⃗] : τ → τ′  general pattern matching

for a non-overlapping covering pattern set P : τ and a family of functions f⃗:= {f_{p} : τ_{p} → τ′}_{p∈P}

m_{τ′′} f⃗: τ′′ • τ → τ′′ • τ′ map

for a family of functions f⃗:= {f_{i} : τ_{i} → τ′_{i}}_{i∈[n]} and a type n ⊢ τ′′

sf_{T,τ} f⃗: T \underline{n} → τ  simple fold

for a family of functions f⃗:= {f_{C} : τ_{C}^{s} → τ}_{C∈D_{T}} on simple reduced argument types τ_{C}^{s}

f_{T,τ} f⃗: T \underline{n} → τ  general fold

for a family of functions f⃗:= {f_{C} : τ_{C}^{r} → τ}_{C∈D_{T}} on reduced argument types τ_{C}^{r}

Figure 8: program schemes on algebraic data types

of a value by types as a operation v| : τ ↓→ τ ↓ which sends a minimal types value \underline{n} ⊢ v : τ and a type τ′ ⊑ τ to the unique subvalue τ′ ↦ v|τ′ ∈ V al_{A}(\underline{m}, τ′) in case of m ⊢ τ′. We get the minimal typing for the restricted value \underline{m} ⊢ v|τ′ : τ′. We define the type of the right factor in th eunique decomposition by the operation |v : τ ↓→ T y_{A} by τ′ ↦ \underline{frnt(v|τ′)} • (τ′ ⊲ τ). This type implies another typing for the restricted value τ′|v ⊢ v : τ. Finaly we define the witnes of the value restriction ⊲ v : τ ↓→ V al_{A} by τ′ ⊲ v := lt(v|τ′) ⊲ v where we used the linear term associated by function lt toe the restricted value (see section 2.2.6). We get a minimal typing for the witnes by \underline{n} ⊢ τ′ ⊲ v : τ′|v.

Given an adt A to any type τ′′ ∈ n ↓ T y_{A} we define a map function m_{τ}. The map function takes a family of functions f⃗ = {f_{i} : τ_{i} → τ′_{i}}_{i∈[n]} as arguments. The application m_{τ′′} f⃗ results in a function of type τ • τ → τ • τ. This function works on a closed value ϵ ⊢ v : τ′′•τ as follows. By unique decomposition we get v = v^{1} • v^{2} with v^{1} := lt(v|τ′′) and v^{2} := τ′′ ⊲ v. So we have a linear value \underline{w} ⊢ v^{1} : τ′′ with w ∈ [n]^{∗} and ϵ ⊢ v^{2} : \underline{w} • τ. We can apply the operation of strings on the family of function f and get a function f^{w} : \underline{w} • τ → \underline{w} • τ′. Application of function f^{w} gives the typing ϵ ⊢ f^{w}v^{2} : \underline{w} • τ′. Finally we define the result as :

ϵ ⊢ m_{τ′′} f⃗v := v^{1} • (f^{w}v^{2}) : τ′′ • τ′

In terms of the unique decomposition operation we get the formula :

m_{τ′′} f⃗v = lt(v|τ′′) • (f^{frnt(v|τ′′)}(τ′′ ⊲ v)

Applying the linear term extraction lt to all minimal typed values \underline{n} ⊢ v : τ′′ result in a pattern set P ⊆ LT_{Σ} which is obviously non-overlapping and covering. We define the family of fucntions :

g⃗ := \{f^{frnt(v)} : \underline{frnt(v)} • τ → \underline{frnt(v)} • τ′\}_{lt(v)∈P}

We get another representation of the map function by general pattern matching :

m_{τ′′} f⃗ = P [g⃗]

Proposition 6 (Polyfun Representation) Each polymorphic function f : τ → τ′ with n ⊢ ττ′ can be represented by general pattern matching. More explicitly we get two pattern sets P_{f} : τ and P′_{f} : τ′. The typings of the pattern are of form \underline{w_{p}} ⊢ p with w_{p} ∈ [n]^{∗} for all pattern p ∈ P_{f} or p ∈ P′_{f}. Further we get a function on pattern sets f^{p} : P_{f} → P′_{f} and string morphisms f^{s} : P_{f} → Mor_{[n]} such that f^{s}(p) : w_{f^{p}(p)} → w_{p} for p ∈ P_{f}. So we get values v_{p} := f^{p}(p) • \underline{f^{s}(p)} which are typed as \underline{w_{p}} ⊢ v_{p} : τ′. Using these values to represent a family of polymorphic functions g⃗ := \{\underline{v_{p}} : \underline{w_{p}} → τ′\} gives the representation of the polymorphic function f = P_{f}[g⃗].

5.5 Simple Fold

A type constructor T is called simple recursive iff each occurrence of T in an argument types τ_{C} with C ∈ D_{T} is of the simple form T \underline{n}. We define the prereduction of an argument type τ_{C}^{p} by substituting all occurrences of T \underline{n} by type variable α_{n+1}. So we get n + 1 ⊢ τ_{C}^{p}.

Given a result type τ, the simple reduced argument type is defined by τ_{C}^{s} := τ_{C}^{p}[τ/α_{n+1}]. Further given a family of functions f⃗ := {f_{C} : τ_{C}^{s} → τ}_{C∈D_{T}} we define the simple fold sf_{T,τ} f⃗: T \underline{n} → τ by :

sf_{T,τ} f⃗:= T [… f_{C} ∘ g_{C} …] where

g_{C} := m_{τ_{C}^{p}} i⃗d(sf_{T,τ} f⃗) : τ_{C} = τ_{C}^{p}[T \underline{n}/α_{n+1}] → τ_{C}^{p}[τ/α_{n+1}] = τ_{C}^{s}

5.6 General Fold

If the type constructor T is not simple we get a set of recursion arguments ra := {τ′ | T τ′ occurs in τ_{C} with C ∈ D_{T} } other than the empty set or the simple set \{\underline{n}\}. Let us assume in the following the number m = |ra| of different recursion arguments. We will use the recursion arguments as a family {τ^{j}}_{j∈[m]} of types.

5.6.1 Type Reduction

We define the pre-reduction of types τ_{C}^{p} by substituting the occurrence of T τ^{j} by the type variable α_{n+j}. So we get n + m ⊢ τ_{C}^{p}. The constructor T can also occur in the recursive arguments τ^{j} so pre-reduction τ^{jp} is also defined on these types. For a string u ∈ [m]^{∗} we denote by u ⊢ (τ′)^{p} that the type variables α_{n+u_{k}} for k ∈ [|u|] occur in prereduced type (τ′)^{p}. If we have further a type τ : |u| then the composition τ′^{p} •^{p} τ is defined by substituting the type variables α_{n+u_{k}} by the types τ_{k} for k ∈ [|u|].

Through substitution of type constructor T with arity n = a(T) by a type n ⊢ τ : 1 we get the notion of a reduced type. We define reduction on a type u ⊢ (τ′)^{p} inductively by :

τ′^{r} := τ′^{p} •^{p} (τ • (τ^{u_{1}})^{r}) … (τ • (τ^{u_{|u|}})^{r})

So type reduction substitutes the type constructor T by left application of the type τ.

5.6.2 Value Reduction

We define the polymorphic general fold f_{T,τ} f⃗: T \underline{n} → τ given a family of polymorphic functions f⃗:= {f_{C} : τ_{C}^{r} → τ}_{C∈D_{T}}.

To this end we define reduction functions r^{j} : T τ^{j} → τ • τ^{jr} for each j ∈ [m]. If we assume u ⊢ τ^{jp} we can use the general map to define h^{j} := m_{T τ^{jp}} i⃗d r^{u_{1}} … r^{u_{|u|}} : T τ^{j} = T τ^{jp}[… T τ^{u_{k}}/α_{n+u_{k}} …] → T τ^{jp}[… τ • (τ^{u_{k}})^{r}/α_{n+u_{k}} …] = T τ^{jr} where the map function used identity associated to each type variable in \underline{n + m} except the type variables α_{n+u_{k}} with k ∈ [|u|] where reduction ru_{k} is used. Using the fold function recursively leads to the needed reduction function

r^{j} := (f_{T,τ} f⃗) ∘ h^{j} : T τ^{j} → τ • τ^{jr}

With a similar construction we get a reduction for each data constructor C ∈ D_{T} with u ⊢ τ_{C}^{p} :

g_{C} := m_{τ_{C}^{p}} i⃗d r^{u_{1}} … r^{u_{|u|}} : τ_{C} → τ_{C}^{r}

It is crucial for well-typedness of the reduction function r^{j} that the family f⃗ is polymorphically typed. So by pattern matching we finalise our definition of the general fold algorithm:

f_{T,τ} f⃗:= T […, f_{C} ∘ g_{C}, …] : T \underline{n} → τ

5.7 Higher Order Schemes

In the last section we defined the program schemes pattern matching T [f⃗], general pattern matching P [f⃗], map m_{τ}, simple fold sf_{T,τ} and general fold f_{T,τ} for each adt A. We know that in each second order adt B live two adt’s : the type adt B_{tadt} and the data adt B_{dadt}.

So we get all the program schemes on the data level B_{dadt}. All we have to do is just a check that the types involved are well constrained. A natural question is: What is the algorithmic meaning of the program schemes on level of types B_{tadt} ?

5.7.1 Type Disciplines

Given an adt A we have defined to sets of function on adt’s. Firstly the set F un_{A}(τ, τ′) of well typed functions f : τ → τ′. Secondly the set P F un_{A}(τ, τ′) of polymophic functions f : τ → τ′ for types with n variables n ⊢ ττ′. In fact the well typed functions are just the polymoprhic functions with ground types.

The picture for constraint adt’s B = (C, ac, T , tt, tag, D, td, dag). is a bit more complex. We saw in section 3.2 that values are typed and types are constrained. When dealing with functions living in second order adt’s we get four interconnected notion of typing.

5.7.2 Higher Order Pattern Matching

Given a constraint name E ∈ C with arity n = ac(E) and the type constructors associated to the constraint name T_{E} := {T ∈ T | tt(T) = E}. Further given a family of well constrained polymorphic functions f⃗ := \{f_{T} : T \underline{n} → τ_{T} \}_{T ∈T_{E}} with constraint D_{T} = tag(T) and the result types a well constrained family {D_{T} ⇒ τ_{T} :: D}_{T ∈T_{E}} with n ⊢ D. Then we can define a poly constrained function E[f⃗] : E\underline{n} → D.

5.7.3 Higher Order Map

Given a constraint Dwith arity n ⊢ D and a type \underline{m} ⇒ τ : D ↑ (t.i. a minimal constrained type τ : D′ with D ⊑ D′). The unique decomposition operation on adt B_{tadt} gives a subinstance type lt(τ|D) ⊑ τ with minimal constraining \underline{n} ⇒ τ|D :: D and decomposition τ = lt(τ|D) • (D ⊲ τ) with minimal constraining D|τ ⇒ D ⊲ τ :: D′. Now assume further that we have a family f⃗ := {f_{i} : D_{i}^{1} → D_{i}^{2}}_{i∈[n]} of well-constrained functions. We define the operation of string w ∈ [n]^{∗} on families of functions by f⃗^{w} := {f_{w_{i}} : D_{w_{i}}^{1} → D_{w_{i}}^{2}}_{i∈[|w|]}. We define the wellconstrained second order map

2m_{D}f⃗v := m_{τ|D}f⃗^{w}v

This deinition is well constrained typed because by definition of the unique decomposition v : τ = lt(τ|D) • \underline{w} • (D ⊲ τ) :: D • D^{1} so the result has type m_{τ|D}f⃗^{w}v : (τ|D)•τ′ : D •D^{2} with a type τ′ :: \underline{w} •D^{2} given by application of family f⃗^{w}.

For a value v ∈ V al_{B} with constrained typing v : τ :: D we define the second order unique decomposition operations :

v|| : D ↓→ v ↓  by v||D′ = v|(τ|D)
||v : D ↓→ Cnst_{B}  by D′||v = \underline{frnt(v||D′)}
•(D′ ⊲ D)
⊲ ⊲v : D ↓→ V al_{B} by D′ ⊲ ⊲v = lt(v||d′) ⊲ v

With the same ingredients as above we get an alternative presentation of the map function in terms of unique decomposition operations. The operation on a value v : τ :: D • D^{1} is defined as

2m_{d}f⃗v = lt(v||D) • (f^{frnt(v||D)}D ⊲ ⊲v)

Note that function 2m_{D}f⃗: D•D^{1} → D•D^{2} is a wellconstrainedtype respecting function iff each member of the family f⃗ is type respecting.

6 Term Transformations

We call a partial function f : T_{Σ} ⇀ T_{Σ} on free theories a term transformation iff there is a sorting restriction so that the function f : T_{Σ}(u, v) → T_{Σ}(u′, v′) is total.

In the following we define a series of term transforms. These term transforms on free theories are used to define algebraic functions on adt’s. Eventually we get a representation of maps and folds (section 7). Finally we will see that this is the right generalisation which extends to iterations schemes of n^{th}order (section 8).

6.1 Occurrences

The generators f ∈ |Σ| of a tree t ∈ T m_{Σ} occur at certain places in the tree. In order to name these places we introduce the set of occurrences O := 1^{∗∗} ≃ ℕ^{∗}. We will use o for an occurrence and O ⊆ O for sets of occurrences. Note that occurrences are strings so the prefix order ⊑^{p} is defined. Because of the isomorphy O ≃ ℕ^{∗} we can define the lexicographic (subtree substitution)

for o ∈ occ(t) with u ⊢ t|o : s and term u ⊢ t′ : s

\overline{(t|_{m}o ↦ t′)}(o′) := \{ \begin{matrix}\overline{t′}(o′′) & if o′ = oo′′ \\ \overline{t}(o′) & else \end{matrix}

(constructor substitution) for o ∈ cocc(t) with t@o = f : (w, s) and term w ⊢ t′ : s

\overline{(t|_{f}o ↦ t′)}(o′) := \{ \begin{matrix}\overline{t′}(o′′) & if o′ = oo′′ with o′′ ∈ cocc(t′) \\ \overline{t}(oio_{2}) & if o′ = oo_{1}o_{2} with t′@o_{1} = x_{i} \\ \overline{t}(o′) & else \end{matrix}

Figure 9: substitutions at occurrences

order ⊑^{lex} on occurrences by:

o ⊑^{lex} o′ iff \{ \begin{matrix}true & if o = o′′i and o′ = o′′j \\ & with i ≤ j \\ o ⊑^{p} o′ & else \end{matrix}

We call a set of occurrences O is a tree domain or lexical ideal iff it is lexical down-closed that is if o ∈ O and o′ ⊑^{lex} o implies o′ ∈ O. A set of occurrences O is called a frontier or prefix anti-chain if it is prefix incompatible that is for o, o′ ∈ O holds neither o ⊑^{p} o′ nor o ⊒^{p} o′.

6.2 Tree Representation

Given a S-sorted tree t ∈ T m_{Σ} the representation of a tree is a partial function \overline{t} : O ⇀ |Σ|∩X. The representation is defined by \overline{ft′}(ϵ) = f, \overline{x}(ϵ) = x and \overline{ft′}(io) is defined as \overline{t′_{i}}(o) iff i ∈ [|t′|]. We write t@o := \overline{t}(o) as short form for the constructor or variable occuring at place o.

So the domain of a representation occ(t) := {o ∈ O | t@o is defined } has the property of a tree domain to be prefix closed. The constructor occurrences of a term are defined by cocc(t) := {o ∈ O | t@o ∈ |Σ|}. A representations of a term string t ∈ T_{Σ} is defined by setting \overline{t}(io) := \overline{t_{i}}(o) iff i ∈ [|t|].

There is a one-to-one correspondence between trees and their representation. So in the following we define operations on trees by explaining the operation on representations. The notion of a subterm at an occurrence t|o is defined by the representation \overline{t|o}(o′) = \overline{t}(oo′).

6.3 Substitutions

Given a term u ⊢ t : v we define two notions of sort compatible substitution at place o ∈ O (see figure 9)

6.3.1 Substitution at Occurrence Sets

Given a term t and a set of occurrences O ⊆ occ(t) we say t|O : s is well sorted iff for all occurrences o ∈ O the induced subterms t|o have sort s. Obviously we can extend the notion of subtree substitution on well sorted occurrence sets. Especially if we denote the set of occurrences of variable x_{i} : s by occ(x_{i}, t) := {o ∈ O | t|o = x_{i}}. We introduce the short form (t|_{m}x_{i} ↦ t′) := (t|_{m}occ(x_{i}, t) ↦ t′).

Given a set of constructor occurrences O ⊆ cocc(t) we say t@O : (u, s) is a sorting of set O iff for all occurrences o ∈ O the constructors t@o coincide on their sorting (u, s). Obviously we can extend the notion of constructor substitution on occurrence sets with sorting. Especially if we denote the set of occurrences of constructor f ∈ |Σ| by occ(f, t) := {o ∈ O | t@o = f}. We introduce the short form (t|_{f}f ↦ t′) := (t|_{f}occ(f, t) ↦ t′).

6.3.2 Evaluation Order

The above definitions of substitutions (t|O ↦ t′) on occurrence sets O are only well defined if we assume a certain order in the evaluation of substitutions on occurrences o ∈ O. In any case of two occurrences o, o′ ∈ O with o ⊑^{p} o′ substitution on o′ has to be done before substitution on o. This is necessary because substitution on o might change the representation on all superfixes (for example o′). So we define that substitution on occurrence sets have to be evaluated in a bottom up manner. Note that in case of a frontier O there is no restriction on the performance order. Note further to any variable x the occurrence set occ(x, t) has frontier property.

6.3.3 Term Transformation at an Occurrence

Instead of substitution at an occurrence o ∈ occ(t) in a term t we can apply a term transformation g : T_{Σ} ⇀ T_{Σ} at the occurrence. Given term u ⊢ t : v the function g must satisfy certain sort restrictions. In case of a subterm sorted like t|o : s we need a restriction g : T_{Σ}(u, s) → T_{Σ}(u, s) and we denote the application as (t|_{m}o ↦ g). In case of constructor substitution and the generator t@o = f : (w, s) we need a restriction g : T_{Σ}(u, w) → T_{Σ}(u, s) and denote the application as (t|_{f}o ↦ g).

6.4 Family Substitutions

Given a term u ⊢ t : v, a family of term transforms f⃗ := {f_{i} : T_{Σ} → T_{Σ}}_{i∈I} and a set of occurrences O ⊆ occ(t). We want to apply at each occurrence o ∈ O a certain transform f_{i}. To this end we define partial functions called either occurrence index function oindx : O ⇀ I or constructor index function cindx : |Σ| ⇀ I.

6.4.1 M-Family Substitution

The tuple (f⃗, oindx) is a m-compatible family iff for each occurrence o ∈ O the index oindx(o) = i ∈ I is defined and the associated transform is sorted as f_{i} : T_{Σ}(u, s) → T_{Σ}(u, s) in case of t|o : s. This leads to the m-family substitution (t|_{m}O ↦ (f⃗, oindx)). In case of the equation O = {o ∈ O | oindx(o) defined } we denote in short (t|_{m}(f⃗, oindx)).

6.4.2 F-Family Substitution

We restrict the occurrence set O to constructor occurrences O ⊆ cocc(t). The tuple (f⃗, cindx) is a fcompatible family iff for each occurrence o ∈ O the index cindx(t@o) = i ∈ I is defined and the associated transform is sorted as f_{i} : T_{Σ}(u, w) → T_{Σ}(u, s) in case of sorting t@o : (w, s). This leads to the ffamily substitution (t|_{f}O ↦ (f⃗, cindx)).

7 Representation of Iteration Schemes

In the above section we defined the notion of term transformations in free theories. Here we will extend this notion to adt’s. First we need the right notion of occurrence in adt’s. We will relate value occurrences to type occurrences (section 7.1). This will eventually lead to a representation of map by a m-family substitution and to the representation of fold by a f-family substitution (section 7.2). Well-sorting preservation of the substitutions will imply well-typedness of the iteration schemes.

The full paper[Weh98] contains a zoo of program schemes on adt’s following a more traditional presentation in form of typed combinators.

7.1 Associated Occurrences

Given a typed value v : τ we explain how an occurrence in the type o ∈ occ(τ) induces a set of occurrences O ∈ occ(v) in the value. To this end we define to a occurrence set O ⊆ O and a natural number j ∈ ℕ the set j.O := {jo | o ∈ O}. We define :

{v||o} ⊆ occ(v) where

{v||ϵ} := {ϵ}
{Cv||io} := ⋃_{j∈[|v|]} ⋃_{o′∈occ(α_{i},(τ_{C})_{j})} j.{v_{j}||o′o}

{v@@o} ⊆ cocc(v) where

{Cv@@ϵ} := {ϵ}∪ ⋃_{j∈[|v|]} ⋃_{o′∈occ(t(C),(τ_{C})_{j})} j.{v_{j}@@o′o}

{Cv@@io} := ⋃_{j∈[|v|]} ⋃_{o′∈occ(α_{i},(τ_{C})_{j})} j.{v_{j}@@o′o}

Proposition 7 (Occurrence Separation) Different occurrences o ≠ o′ induce disjoint value occurrence sets. That is {v||o} ∩ {v||o′} = ∅ and {v@@o} ∩ {v@@o′} = ∅

7.1.1 Well-Typed Occurrences

Given a typed value v : τ and a type occurrence o ∈ occ(τ) the the set of associated value occurrences is well typed {v||o} : τ|o that is for each value occurrence o′ ∈ {v||o} the sub-value v|o′ has type τ|o. Obviously we can extend the notion of value occurrences {v||O} associated to a set of type occurrences O ⊆ occ(τ). The set of occurrences O has to coincide on the induced types that is all occurrences o ∈ O induce the same type τ|o. Note that the map O ↦ {v||O} is frontier preserving. This is a slight generalisation of the unique decomposition proposition.

7.1.2 Well-Sorted Occurrences

We denote the sort of a data constructor by C :^{s} T in case of t(C) = T. Given a typed value v : τ and a constructor occurrence o ∈ cocc(τ) then the associated data constructors at the occurrences are well sorted {v@@o} :^{s} τ@o that is for each value occurrence o′ ∈ {v@@o} the associated constructor v@o′ has sort τ@o. We define the notion {v@@O} of data constructor occurrences associated to type constructor occurrences O ⊆ cocc(τ). The set of occurrences O has to coincide on the induced sorts that is all occurrences o ∈ O induce the same type constructor τ@o.

7.2 First order Schemes

With the above connection of occurrences and adt’s we are able to state the definition of program schemes for adt’s.

7.2.1 Map

We give a definition of a map m_{τ′′} for a type n ⊢ τ′′ and a family of functions f⃗ := {f_{i} : τ_{i} → τ′_{i}}_{i∈[n]}. The short forms τ = τ_{1} … τ_{n} and τ′ = τ′_{1} … τ′_{n} are used. The operation on a value v : τ′′ • τ is defined by :

m_{τ′′} f⃗v := (v|_{m}(f⃗, oindx))

where we apply the notion of m-family substitution from paragraph 6.4.1. In order to apply this notion we have to define an occurrence index function oindx : O → [n]. We define the sets O_{i} := {v||occ(α_{i}, τ′′)} for i ∈ [n] containing the value associated to the type occurrences of type variable α_{i}. As short notation we introduce (v|α_{i} ↦↦ f_{i}) := (v|_{m}O_{i} ↦ f_{i}). Finally we define O := O_{1} ∪ ⋯ ∪ O_{n} with a canonical occurrence index oindx(o) = i iff o ∈ O_{i}. The occurrence index is well defined because occurrence separation implies disjointness i ≠ i′ ⇒ O_{i} ∩ O_{i′} = ∅.

In order to prove well-typedness of map we have to interpret the operations of map on explicitly typed values. Well-typedness of the occurrence sets O_{i} is interpreted as well-T y_{A}-sortedness. Well-sort preservation of m-family substitution gives explicit typability of map results. By application of erasure we get the implicitly typed result m_{τ′′} f⃗v : τ′′ • τ′.

7.2.2 Fold

We give a definition of a general fold f_{T,τ} with arity n = a(T) a type n ⊢ τ : 1 and a family of polymorphic functions f⃗ := {f_{C} : τ_{C}^{r} → τ}_{C∈D_{T}}. The argument type associated to a data constructor in set D_{T} := {C ∈ C | t(C) = T } is give by the specification through τ_{C} := ag(C). The reduced type τ_{C}^{r} is defined by a constructor substitution (see 6.3.1)τ_{C}^{r} := (τ_{C}|_{f}T ↦ τ). Given a typed value v : T τ′ we define the result a fold application by :

f_{T,τ} f⃗v := (v|_{f}{v@@ϵ} ↦ (f⃗, id_{D_{T}}))

where we apply the notion of f-family substitution from paragraph 6.4.2.

Applying well-sortedness of the occurrence set {v@@ϵ} and well-sort preservation of f-family substitution implies well-typedness of result f_{T,τ} f⃗v : τ • τ′.

8 n^{th}-Order Iteration Schemes

8.1 Out most Constraints

We define a sorting function srt_{k} : GS_{n} → GS_{k−1} for k ∈ [n]. by setting srt_{n} := st_{n} and srt_{k} := st_{k} ∘ srt_{k+1}. Given a generator f ∈ GS_{n} we define the associated out most constraint as D_{f} := agt_{1}∘str_{2}(f) and the number of used variables in that constraint is n_{f} := agt_{0} ∘ str_{1}(f) ∈ ℕ so we have D_{f} ∈ n_{f} ↓ T_{ΣS}. To each value v ∈ V al_{S} exists a typing t ⊢ v : t′. Recall that t is a sequence of values of ascending order and t′ is a sequence of values of descending order. So any typing has form t ⊢ v : t′′D for a value of order zero D ∈ T_{ΣS}. We will denote the above fact as v :: D and say value v is out most constraint by D.

8.2 Constrained Functions

We say a function f : V al_{S} ⇀ V al_{S} is out most constrained like f :: D → D′ if each out most constrained closed value ϵ ⊢ v :: D is mapped to an out most constrained value ϵ ⊢ fv :: D′. If we know the used variables n ⊢ DD′ in the constraints we call the function f outer poly constrained if it is outer constrained fD′′ : D • D′′ → D′ • D′′ for each constraint D′′ : n. These restrictions imply the invariant fD_{1}v = f(D_{1} • D_{2})v holds for values v :: D • D_{1} and constraints D_{1}, D_{2}.

8.3 Associated Occurrences

Each value v ∈ V al_{S} is a pre-value v ∈ T_{ΣS^{pre}} so we define the set of value occurrences associated to a occurrence in an out most constraint.

{v|^{n}o} ⊆ occ(v) where

{v|^{n}ϵ} := {ϵ}
{fv|^{n}io} := is defined iff i ∈ [n_{f}]
⋃_{j∈[|v|]} ⋃_{o′∈occ(x_{i},(D_{f})_{j})} j.{v_{j}|^{n}o′o}

{v@^{n}o} ⊆ cocc(v) where

{fv@^{n}ϵ} := {ϵ}∪
⋃_{j∈[|v|]} ⋃_{o′∈occ(srt_{1}(f),(D_{f})_{j})} j.{v_{j}@^{n}o′o}
{fv@^{n}io} := is defined iff i ∈ [n_{f}]
⋃_{j∈[|v|]} ⋃_{o′∈occ(x_{i},(D_{f})_{j})} j.{v_{j}@^{n}o′o}

8.3.1 Well-Constrained Occurrences

Given an out most constrained value v :: D and an occurrence o which is a place in the constraint o ∈ occ(D). In this case the sub-values at the occurrences o′ ∈ {v|^{n}o} are out most constraint such as (v|o′) :: (D|o). We naturally extend the notion {v|^{n}O} of value occurrences associated to a set of constraint occurrences O ⊆ occ(D) iff for each two occurrences o_{1}, o_{2} ∈ O induce the same constraints D|o_{1} = D|o_{2}.

8.3.2 Well-Sorted Occurrences

Given an out most constrained value v :: D and a constructor f ∈ GS_{n}. We call the constructor E := srt_{1}(f) ∈ GS_{0} = |ΣS| the outer sort of the constructor f (in short f ::^{s} E). Given a constructor occurrence o ∈ cocc(D) then the associated constructor occurrences o′ ∈ {v@^{n}o} are outer sorted such as (v@o′) ::^{s} (D@o). We extend the notion {v@^{n}O} of value constructor occurrences associated to outer constraint constructor occurrences for a set O ⊆ occ(E, D) with E ∈ GS_{0}.

8.4 n^{th}-Order Map

A general map m_{D′′} can be defined for a outer constraint D′′ ∈ n ↓ T_{ΣS} and a family of out most constrained functions f⃗ := {f_{i} :: D_{i} → D′_{i}}_{i∈[n]} We get a out most constrained function m_{D′′} f⃗ : D′′ • D → D′′•D′ which operates on values v :: D•D′ as follows by m-family substitution (see 6.4.1) :

m_{D′′} f⃗v := (v|_{m}(f⃗, oindx))

We define occurrence sets associated to the variables occuring in constraint D′′ by setting O_{i} := {v|^{n}occ(x_{i}, D′′)}. So we get the canonical occurrence index function oindx : O_{1} ∪ ⋯ ∪ O_{n} → [n].

8.5 n^{th}-Order Fold

To define a general fold we need as ingredients a constraint constructor E : n ∈ ΣS an outer constraint D ∈ T_{ΣS}(n, 1) and a family of outer poly constrained functions g⃗ := {g_{T} :: D_{T}^{r} → D}_{T ∈GS_{1}^{E}} where GS_{1}^{E} := {T ∈ GS_{1} | st_{1}(T) = E} and D_{T} = agt_{1}(T) for T ∈ GS_{1}. Further the reduced constraint D_{T}^{r} is given by definition D_{T}^{r} := (D_{T} |_{f}T ↦ D). We get a outer poly constrained function f_{E,D}f⃗ : E\underline{n} → D which operation of a value v :: ED′ is given by ffamily substitution (see 6.4.2) :

f_{E,D}g⃗v := (v|_{f}{v@^{n}ϵ} ↦ (g⃗, srt_{2}))

The sorting function srt_{2} : GS_{n} → GS_{1} is used as the constructor index. We know for each constructor occurrence o′ ∈ {v@^{n}ϵ} the outer sorting v@o′ = fv′ :^{s} E. This sorting implies srt_{2}(f) ∈ GS_{1}^{E} which guarantees well-definedness.

9 Conclusion

9.1 Related Work

The ideas of this paper are clearly initiated on the functional programming side by the work of Bird [Bir87]. The generalisation in notions of cata-, ana-, hylo- and para-morphisms in [MFP91] make the connection to category theory and domain theory explicit. While the above work promotes the discipline of algebraic programming encouraging to write programs using only the provided iteration schemes, functorial ML [BJM96] introduces categorical notions into languages such as ML. In functorial ML general algorithms for fold and map are introduced but just for regular adt’s. We were able to state general algorithms working also with non-regular adt’s.

The strand of work on polytypic programming [Mee96] emphasises that some functions can be written for all types. Map and fold are examples for polytypic functions. The results of this paper can be seen as first examples of higher order polytypic programming.

On the mathematical side the paper was inspired by Baez and Dolan’s program of higher dimensional algebra [BD95]. The foundation of this work is a hierarchy of weak n-categories, the definition of which is current research [BD98, HMP98, Bat98]. The free theories used in this paper are instances of the topological motivated notion of operads which are central structures in above work. The formal connection with these structures is current research of the present author.

9.2 Results

We presented the novel programming construct of higher order algebraic data types. This new construct is presented as the hierarchy of n^{th}-order adt’s. At level zero live signatures and free theories. At the first level live the adt’s known from ML and Haskell. At the second level we introduced constraint adt’s which are an instance of constraint type systems [SOW98]. Associated with the hierarchy of adt’s we were able to present a type inference algorithm together with a minimal typing property. Further we defined the general map and fold algorithms living in this hierarchy. In order to define these algorithms the non-regular fold has been invented.

9.3 Future Work

The above results raise naturally a range of questions about extending the new programming construct introduced here : How to extend adt’s to allow use of function types in specifications ? How to mix higher order functions and adt’s (that is the introduction of lambda abstraction) ? Introduction of firstorder (synonym predicative) poly-n-morphism with associated let-constructs would also be nice. Finally the introduction of impredicative polymorphism in the style of Läufer, Odersky [OL96] or Jones [Jon97] would lead to a nice general picture of typefull programming.

Acknowledgements

I want to thank my colleagues who helped to improve the presentation and my poor English. Thanks to Daniele Turi, Martin Sulzmann, Alex Simpson, Ralf Schweimeier, Samson Abramsky, Martin Odersky and Julo Chroboczek.

References

[Bat98] M.A. Batanin. Monoidal globular categories as a natural environment for the theory of weak n-categories. Adv. Math., 136:39– 103, 1998.

[BD95] J. Baez and J. Dolan. Higher-dimensional algebra and topological quantum field theory. Jour. Math. Phys., 36:6073–6105, 1995.

[BD98] J. Baez and J. Dolan. Higher dimensional algebra iii: m-categories and the algebra of opetopes. Adv. Math., 135:145–206, 1998.

[Bir87] Richard S. Bird. An introduction to the theory of lists, volume F36 NATO ASI Series of Logic of Programming and Calculi of Discrete Design, pages 5–42. Springer-Verlag, 1987.

[BJM96] G. Bellè, C.B. Jay, and E. Moggi. Functorial ML. In K. Herbert and S.D. Swierstra, editors, Programming Languages: Implementations, Logics, and Programs, volume 1140 of Lecture Notes in Computer Science. Springer-Verlag, 1996. TR SOCS-96.08.

[HMP98] C. Hermida, M. Makkai, and J. Power. Higher dimensional multigraphs. In LICS ’98 Proceedings, volume 13, pages 207–213, Indianapolis, Indiana, June 1998. IEEE, ieee press.

[Jon97] Mark P. Jones. First-class polymoprhism with type inference. In POPL, pages 483– 496. acm press, 1997.

[Mee96] Lambert Meertens. Calculate polytypicaly! In H. Kuchen and S. Swierstra, editors, Proceedings of PLIP ’96, pages 1–16, Aachen, September 1996. LNCS 1140.

[MFP91] Erik Meijer, Maarten Fokkinga, and Ross Paterson. Functional programming with bananas, lenses, envelopes, and barbed wire. In John Hughes, editor, Proceedings Functional Programming Languages and Computer Architecture, 5th ACM Conference, Cambridge, MA, USA, pages 124– 144. ACM, Lecture Notes in Computer Science 523, August 1991.

[MH95] Erik Meijer and Graham Hutton. Bananas in space: Extending fold and unfold to exponential types. In FPCA ’95, pages 324–333, La Jolla, California, June 1995. ACM.

[OL96] Martin Odersky and Konstantin Läufer. Putting type annotations to work. In Proc. 23rd ACM Symposium on Principles of Programming Languages, pages 65–67, January 1996.

[SOW98] Martin Sulzmann, Martin Odersky, and Martin Wehr. Type inference with constrained types. Theory and Practice of Object Systems, pages 75–103, to appear 1998.

[Wag] Eric G. Wagner. Handbook of Logic in Computer Science, volume 3, chapter Algebraic Semantics, pages 323–393.

[Weh98] Martin Wehr. Higher order algebraic data tyeps (full paper). Technical report, University of Edinburgh, URL

http://www.dcs.ed.ac.uk/home/wehr,

July 1998.