Syntactic Considerations on Recursive Types

Martín Abadi

                    ma@pa.dec.com

Systems Research Center Digital Equipment Corporation Marcelo P. Fiore^{∗}

                                                mf@dcs.ed.ac.uk

LFCS University of Edinburgh

Abstract

We study recursive types from a syntactic perspective. In particular, we compare the formulations of recursive types that are used in programming languages and formal systems. Our main tool is a new syntactic explanation of type expressions as functors. We also introduce a simple logic for programs with recursive types in which we carry out our proofs.

1 Introduction

Recursive types are common in both programming languages and formal systems. By now, there is a deep and well-developed semantic theory of recursive types. The syntactic aspects of recursive types are also well understood in some special cases. In particular, there is an important body of knowledge about covariant recursive types, which include datatypes like natural numbers, lists, and trees.

Beyond the covariant case, however, the syntactic understanding of recursive types becomes rather spotty. Consequently, the relations between various alternative formulations of recursive types are generally unclear. Furthermore, the syntactic counterparts to some of the most basic semantic results are unknown.

In this paper we study some syntactic properties of recursive types. Our main purpose is to understand the common rules for recursive types, rather than to invent new ones. We examine the formulations of recursive types as they appear in programming languages and in formal systems; there are two main approaches:

• The first approach relies on a notion of type equality (e.g., see [16, 3]). A recursive type is equal to its expansions, and if a term has a type then it has all equal types. For example, one may define a type D equal to D → D, and hence equal also to (D → D) → (D → D); any term that has one of these types has all the other types.

• The second approach relies on an explicit isomorphism between a recursive type and its expansions (e.g., see [12, 13]). For example, one may introduce a type D isomorphic to D → D; the isomorphism between these types is represented explicitly by two terms, one of type D → (D → D) and the other of type (D → D) → D. A term of type D does not have type D → D, but can be mapped to a term of that type via the isomorphism.

We relate these two formulations in the setting of a first-order λ-calculus. Specifically, we show that any typing that can be achieved with one formulation can also be achieved with the other, possibly by inserting some explicit coercion functions. This result could seem obvious, but it turns out to be fairly difficult and its details depend on a number of sound but significant assumptions.

The proof of this result requires the development of a theory of type expressions as functors. In semantics, it is by now common to view functions on types as functors; the substantial difficulties that arise for contravariant types can be surmounted with a variety of techniques (categories of embeddings, involutory categories, etc.) [21, 10, 11]. Our explanation of type expressions as functors, although based on semantic ideas, is purely syntactic. It is perhaps more elementary and compelling than its semantic counterparts.

We also introduce a simple logic for the first-order λ-calculus with recursive types. It is a logic of partial terms [4, 18]; because of partiality, we avoid the inconsistencies connected with recursive types. Alternatively, we could have reasoned in the models of the logic, possibly doing without the logic altogether. We have preferred to use the logic because of the syntactic character of our enterprise.

∗Research supported by EPSRC project Frameworks for Programming Language Semantics and Logic (grant RR29300) and by HCM project Typed Lambda-Calculus (grant ERBCHRXCT 92-0046).

The logic serves as an ambiance for our work. For example, we use the logic for proving that certain coercion functions establish isomorphisms, and for checking the functoriality of our functorial interpretation of type expressions. The logic is too weak for the verification of realistic programs, but it may constitute the core of a useful logic for that purpose.

Our work draws on many previous developments in semantics and in logics of programs. It also has affinities with previous syntactic work, particularly that of Amadio and Cardelli [3]. Amadio and Cardelli have shown how to replace subtypings with coercion functions in the presence of recursive types (see also [6]). Our work is complementary to theirs; roughly, their coercion interpretation reduces a calculus with subtyping to one with type equality, and our coercion interpretation reduces one with type equality to one with isomorphism. Another relevant syntactic investigation is that of Plotkin [19], who developed a second-order intuitionistic linear type theory with a fixed-point operator at the level of terms, showed how to encode recursive types, and derived some reasoning principles for them. While it would be interesting to build on Plotkin’s theory, we have preferred to avoid type quantification and linear types. Finally, Urzyczyn has studied typability in several systems with covariant recursive types [22]; some of our results are similar to his.

The next section is mostly a review of the formulations of recursive types; we compare them formally in sections 4 and 6.5. In section 3, we define the functorial interpretation of type expressions. In section 5 we describe our logic of programs, and in section 6 we show some of its applications.

2 Formulations of recursive types

In this section we review the main formulations of recursive types in the context of a first-order λ-calculus. The resulting systems are versions of FPC [13].

2.1 Core FPC

We start by briefly describing the part common to all systems; it is rather standard, so we list its rules in the appendix.

A type context is a list of distinct type variables. We write O ⊢ ⋄ to indicate that O is a well-formed type context. As types, we have type variables, product types, function types, sum types, and recursive types.

We use the notation μX.F for a recursive type (the “solution” of X = F, where X may occur free in F). We write O ⊢ A to indicate that A is a well-formed type in the type context O.

A term context is a list of distinct variables with types. We write O ⊢ E to indicate that E is a wellformed term context in the type context O. As terms, we have variables, pairs, functions, and sums; in section 2.2, below, we introduce additional terms that correspond to recursive types. We write O; E ⊢ e : A to indicate that term e has type A in the type context O and the term context E.

Convention. We let O range over type contexts; X, Y, Z over type variables; A, B, C, F, G over types; E over term contexts; x, y, z, f, g, h, u, v over term variables; and e, s, t over terms. We write A[X] to indicate that X may occur free in A, and then write A[B/X] or simply A[B] to represent the result of replacing X with B (avoiding capture of bound variables). Similarly, we write e[x], e[t/x], and e[t].

2.2 FPC with isomorphism

One standard way to complete the definition of FPC is to introduce an explicit isomorphism between a recursive type and its (one-step) expansion. The (one-step) expansion of the recursive type μX.F is F [μX.F/X]. The constructs fold and unfold represent that isomorphism; they have the rules:

\frac{O, X ⊢ F [X] O; E ⊢ e : F [μX.F]}{O; E ⊢ fold_{μX.F} (e) : μX.F}

\frac{O; E ⊢ e : μX.F [X]}{O; E ⊢ unfold(e) : F [μX.F]}

Recursive definitions. In the remainder of the paper we often need to give recursive definitions of functions. FPC does not have any primitive facilities for such definitions but, as is well known, one can construct a call-by-value fixed-point operator in FPC. In its definition, which we give next, we write a =^{Δ} e : A to mean that a equals e by definition and has type A, leaving implicit the context for the typing. Assuming that X does not occur free in A or B, we define fix_{A→B} by:

fix_{A→B} =^{Δ} λf: (A → B) → A → B.
V_{A→B} (fold_{μX.X→A→B} V_{A→B})
: ((A → B) → A → B) → A → B
V_{A→B} =^{Δ} λx: μX.X → A → B.λy: A.
f (unfold(x)(x)) y
: (μX.X → A → B) → A → B

Similarly, we can code mutually recursive definitions. For such definitions, we construct a term ffix_{A×B}, à la Beckič:

ffix_{A×B} =^{Δ} λΦ: A × B → A × B.

(ϕ^{†}[fix_{B} ψ], fix_{B} ψ) : (A × B → A × B) → A × B

where

ϕ =^{Δ} λz: A × B. fst(Φz)
φ =^{Δ} λz: A × B. snd(Φz)
ϕ^{†}[x] =^{Δ} fix_{A}(λy: A. ϕ(y, x))
ψ =^{Δ} λx: B. φ(ϕ^{†}[x], x)

Omitting type information, we write λ(x, y). e[x, y] for λz. e[fst(z), snd(z)] and

ffix \{ \begin{matrix}y & = & ϕ[y, x] \\ x & = & φ[y, x] \end{matrix} \}

for ffix_{A×B}(λ(y, x): A × B. (ϕ[y, x], φ[y, x])). This is the pair of solutions to the equations y = ϕ[y, x] and x = φ[y, x].

2.3 FPC with equality

Another possible way to complete the definition of FPC is to introduce a notion of type equality, and to say that if a term has a type then it has all equal types:

(Retyping) \frac{O; E ⊢ e : A O ⊢ A = B}{O; E ⊢ e : B}

There are at least two possible axiomatisations of type equality, and they induce two variants of FPC with equality. In the first variant, the type μX.F equals its expansion F [μX.F]. In the second, very roughly, the type μX.F equals its “infinite” expansion. The first variant includes the following rules for type equality:

(Symm) \frac{O ⊢ A = B}{O ⊢ B = A}

(Trans) \frac{O ⊢ A = B O ⊢ B = C}{O ⊢ A = C}

(X) \frac{O ⊢ ⋄}{O ⊢ X = X} X ∈ O

(⋆) \frac{\begin{matrix}O ⊢ A = A′ \\ O ⊢ B = B′ \end{matrix}}{O ⊢ A ⋆ B = A′ ⋆ B′} ⋆ ∈ \{×, →, +\}

(μ) \frac{O, X ⊢ F = G}{O ⊢ μX.F = μX.G}

(Fold/Unfold) \frac{O, X ⊢ F [X]}{O ⊢ F [μX.F] = μX.F}

We follow the approach of Amadio and Cardelli for formulating the second variant. We say that a type F [X] is contractive in X (and write F [X] ≻ X) if every occurrence of X in F [X] is under an operator ×, →, or +. More precisely, F [X] is contractive in X if X does not occur free in F [X]; if F [X] is of the form F_{1}[X] ⋆ F_{2}[X] for ⋆ ∈ {×, →, +}; or if F [X] is of the form μY.F_{1}[X] where F_{1}[X] is contractive in X. The second variant extends the first variant with one rule:

(Contract) \frac{\begin{matrix}O ⊢ C[A] = A \\ O ⊢ C[B] = B \end{matrix}}{O ⊢ A = B} C[X] ≻ X

2.4 Isomorphism versus equality

From now on, whenever we mention FPC without qualification, we mean the formulation of FPC with isomorphism; we refer to the first variant of FPC with equality as FPC_{=} and to the second as FPC_{=+}. When there could otherwise be ambiguity, we use ⊢, ⊢_{=}, and ⊢_{=+} to indicate provability in these systems.

Each variant of FPC has advantages. FPC with isomorphism has a somewhat simpler proof theory and semantics; it can also be argued that it is clearer. On the other hand, the notion of type equality can be appealing for programming, particularly in the presence of a subtyping relation (e.g., as in Modula-3 [16]); hence we may prefer FPC_{=} or FPC_{=+}. Of these, FPC_{=} is easier to formulate and to understand, while FPC_{=+} is more liberal. We know advocates of at least two variants of FPC. We do not suggest that one variant of FPC is “right”; rather, we aim to clarify the relations between the variants.

We start with some observations:

• First, FPC_{=} is strictly weaker than FPC_{=+}, as discussed by Amadio and Cardelli. For example, we obtain ∅ ⊢_{=+} μX.μY.(X → Y) = μX.(X → X) but not ∅ ⊢_{=} μX.μY.(X → Y) = μX.(X → X).

• FPC can be embedded into FPC_{=} by deleting all occurrences of the fold and unfold constructs. This embedding preserves provability.

• There are typings of FPC_{=} that cannot be obtained in FPC. For example, the self-application xx can be typed in FPC_{=} (with x : μX.(X → X)) but not in FPC.

id_{A} =^{Δ} (λx: A. x) : A → A
∘_{A,B,C} =^{Δ} (λ(g, f): (B → C) × (A → B). λx: A. g(f(x)))

: (B → C) × (A → B) → A → C

fd_{μX.F} =^{Δ} (λf: F [μX.F/X]. fold_{μX.F} (f)) : F [μX.F/X] → μX.F
ud_{μX.F} =^{Δ} (λx: μX.F. unfold(x)) : μX.F → F [μX.F/X]
×_{(A_{1},A_{2}),(B_{1},B_{2})} =^{Δ} λ(f, g): (A_{1} → B_{1}) × (A_{2} → B_{2}). λ(x, y): A_{1} × A_{2}. (f(x), g(y))

: (A_{1} → B_{1}) × (A_{2} → B_{2}) → (A_{1} × A_{2}) → (B_{1} × B_{2})

→_{(A_{1},A_{2}),(B_{1},B_{2})} =^{Δ} λ(f, g): (B_{1} → A_{1}) × (A_{2} → B_{2}). λh: A_{1} → A_{2}. λx: B_{1}. g(h(f(x)))

: (B_{1} → A_{1}) × (A_{2} → B_{2}) → (A_{1} → A_{2}) → (B_{1} → B_{2})

+_{(A_{1},A_{2}),(B_{1},B_{2})} =^{Δ} λ(f, g): (A_{1} → B_{1}) × (A_{2} → B_{2}). λz: A_{1} + A_{2}.

case z of l(x).inl_{B_{1},B_{2}}(f(x)) or r(y).inr_{B_{1},B_{2}}(g(y)) : (A_{1} → B_{1}) × (A_{2} → B_{2}) → (A_{1} + A_{2}) → (B_{1} + B_{2})

Figure 1. Auxiliary term definitions

Y_{\overline{A},\overline{B}}(\overline{t, s}) =^{Δ} id_{Y} for Y ≠ X_{1}, …, X_{n}
X_{i}_{\overline{A},\overline{B}}(\overline{t, s}) =^{Δ} s_{i}
(G × G′)_{\overline{A},\overline{B}}(\overline{t, s}) =^{Δ} G_{\overline{A},\overline{B}}(\overline{t, s}) × G′_{\overline{A},\overline{B}}(\overline{t, s})
(G → G′)_{\overline{A},\overline{B}}(\overline{t, s}) =^{Δ} G_{\overline{B},\overline{A}}(\overline{s, t}) → G′_{\overline{A},\overline{B}}(\overline{t, s})
(G + G′)_{\overline{A},\overline{B}}(\overline{t, s}) =^{Δ} G_{\overline{A},\overline{B}}(\overline{t, s}) + G′_{\overline{A},\overline{B}}(\overline{t, s})
(μX_{n+1}.G)_{\overline{A},\overline{B}}(\overline{t, s}) =^{Δ} snd(ffix \{ \begin{matrix}v & = & fd_{A_{n+1}} ∘ G_{\overline{B};B_{n+1},\overline{A};A_{n+1}}(\overline{s, t}; u, v) ∘ ud_{B_{n+1}} \\ u & = & fd_{B_{n+1}} ∘ G_{\overline{A};A_{n+1},\overline{B};B_{n+1}}(\overline{t, s}; v, u) ∘ ud_{A_{n+1}} \end{matrix} \})

where A_{n+1} = (μX_{n+1}.G)[A_{1}, …, A_{n}] and B_{n+1} = (μX_{n+1}.G)[B_{1}, …, B_{n}]

Figure 2. Definition of functors In section 4, we show that in fact it is possible to embed FPC_{=} and FPC_{=+} into FPC by inserting coercion functions (for example, rewriting xx as unfold(x)(x)).

3 Type expressions as functors

In this section we develop a syntactic interpretation of type expressions as functors. Despite the categorical source of our method, we do not discuss categorical ideas until late in this section, in order to emphasize that our results, though suggested by category theory, may be understood without it.

Definitions. For types F [X], A, and B, and terms s : A → B and t : B → A, we define a term F [X]_{A,B}(t, s) : F [A] → F [B]. As we show in a later section, F _{,} ( , ) has useful properties (such as functoriality). Here we are not yet concerned with the exact nature of those properties, but we try to give a non-trivial definition. For example, we try to avoid defining F_{A,B}(t, s) so that it is a constant function, and instead try to put all inputs (A, B, s, t) to good use.

In order to be more precise, we introduce some auxiliary notation. We write \overline{A} for A_{1}; …; A_{n} and \overline{B} for B_{1}; …; B_{n}, and \overline{t, s} for t_{1}, s_{1}; …; t_{n}, s_{n}. We also write λ(x, y) : A × B. e[x, y] for λz : A × B. e[fst(z), snd(z)], and make the definitions given in Figure 1. We use the operators ∘, ×, →, and + of Figure 1 as infix operators on terms, omitting type subscripts. We write O; E ⊢ s : A \overleftarrow{→} B : t for O; E ⊢ s : A → B and O; E ⊢ t : B → A.

Definition 3.1 Let O, X_{1}, …, X_{n} ⊢ F [X_{1}, …, X_{n}], and O; E ⊢ s_{i} : A_{i} \overleftarrow{→} B_{i} : t_{i} for i = 1, …, n. We define F_{\overline{A},\overline{B}}(\overline{t, s}) so that:

O; E ⊢ F_{\overline{A},\overline{B}}(\overline{t, s}) : F [A_{1}, …, A_{n}] → F [B_{1}, …, B_{n}]

The definition is by induction on the structure of F, and is given in Figure 2. □

The definition of F_{\overline{A},\overline{B}}(\overline{t, s}) is the basis for other useful definitions, such as the following definition for iterators and coiterators, which we need in the rest of the paper:

Definition 3.2 For O, X ⊢ F [X] and O ⊢ A, we define coit : (A → F [A]) × (F [A] → A) → A → μX.F and it : (A → F [A]) × (F [A] → A) → μX.F → A:

coit  =^{Δ} λ(g, f): (A → F [A]) × (F [A] → A).

fst(ffix \{ \begin{matrix}v & = & fd ∘ F (u, v) ∘ g \\ u & = & f ∘ F (v, u) ∘ ud \end{matrix} \})

it  =^{Δ} λ(g, f): (A → F [A]) × (F [A] → A).

snd(ffix \{ \begin{matrix}v & = & fd ∘ F (u, v) ∘ g \\ u & = & f ∘ F (v, u) ∘ ud \end{matrix} \})

We write it ( \begin{matrix}t \\ s \end{matrix} ) for it(t, s) and coit ( \begin{matrix}t \\ s \end{matrix} ) for

coit(t, s). □

Categorical ideas. The category-theoretic solution of recursive type equations is based on the following, by now standard, ideas: types constitute objects of a category, and type constructors are functors on the category of types. Those ideas are the origin of the definition of types as functors that we have given.

The treatment of type constructors as functors is difficult because of contravariance. A solution is to take the category of types to be involutory (i.e., isomorphic to its dual via an involution) [8]. Given a category C there are various approaches to constructing an involutory category I(C). In the context of orderenriched categories one can exploit the duality embedding/projection [21]. There are also canonical choices, namely C̆ = C^{op} × C [11] or its subcategory C^{D} [1, 10] consisting of all those objects on the diagonal. In any case type constructors with n free type variables are viewed as symmetric functors I(C)^{n} → I(C), induced by functors I(C)^{n} → C.

In our definitions, we are constrained by syntax. Interestingly, the syntax seems to steer us away from the approach based on C̆, and towards that based on C^{D}. Within this latter approach, there are two possible ways to proceed, which correspond respectively to viewing type constructors as symmetric functors (C^{D})^{n} → C^{D} or as functors (C^{D})^{n} → C. For instance, given F [X], to every s : A → B and t : B → A we could either associate a term F^{D}(t, s) : (F [A] → F [B]) × (F [B] → F [A]), or a term F (t, s) : F [A] → F [B]. We have essentially taken the second approach, which is more concise.

4 Formulations of recursive types, revisited

We now return to the problem of relating the formulations of FPC. In short, we obtain:

1. For every equality A = B provable in either FPC_{=} or FPC_{=+} there is a corresponding pair of coercion functions s : A \overleftarrow{→} B : t. The definition of these functions is based on similar definitions used for the syntactic treatment of functors in section 3.

(Symm) \frac{O; ∅ ⊢ s : A \overleftarrow{→} B : t}{O; ∅ ⊢ t : B \overleftarrow{→} A : s}  (Trans) \frac{O; ∅ ⊢ s : A \overleftarrow{→} B : t O; ∅ ⊢ s′ : B \overleftarrow{→} C : t′}{O; ∅ ⊢ s′ ∘ s : A \overleftarrow{→} C : t ∘ t′}

(X) \frac{O ⊢ ⋄}{O; ∅ ⊢ id_{X} : X \overleftarrow{→} X : id_{X}} X ∈ O (⋆) \frac{O; ∅ ⊢ s : A \overleftarrow{→} A′ : t O; ∅ ⊢ s′ : B \overleftarrow{→} B′ : t′}{O; ∅ ⊢ s ⋆ s′ : A ⋆ B \overleftarrow{→} A′ ⋆ B′ : t ⋆ t′} ⋆ ∈ \{×, +\}

(→) \frac{O; ∅ ⊢ s : A \overleftarrow{→} A′ : t O; ∅ ⊢ s′ : B \overleftarrow{→} B′ : t′}{O; ∅ ⊢ t → s′ : (A → B) \overleftarrow{→} (A′ → B′) : s → t′}

(μ) \frac{O, X; ∅ ⊢ s[X] : F \overleftarrow{→} G : t[X]}{O; ∅ ⊢ coit ( \begin{matrix}s[μX.F] ∘ ud_{μX.F} \\ fd_{μX.F} ∘ t[μX.F] \end{matrix} ) : μX.F \overleftarrow{→} μX.G : it ( \begin{matrix}s[μX.F] ∘ ud_{μX.F} \\ fd_{μX.F} ∘ t[μX.F] \end{matrix} )}

(Contract) \frac{O; ∅ ⊢ s : C[A] \overleftarrow{→} A : t O; ∅ ⊢ s′ : C[B] \overleftarrow{→} B : t′}{O; ∅ ⊢ it(t′, s′) ∘ coit(t, s) : A \overleftarrow{→} B : it(t, s) ∘ coit(t′, s′)} C[X] ≻ X

Figure 3. Definition of coercion functions

2. This easily implies that for any typing e : C of either FPC_{=} or FPC_{=+} we can construct a corresponding typing e′ : C in FPC, where e′ is obtained from e by inserting coercion functions.

The construction of the coercion functions is fairly difficult, particularly because of the possibility of nested recursion. For example, the equality

\begin{matrix}μX.μY.(Z + (Y → X)) \\ = μX.(Z + ((μY.(Z + (Y → X))) → X)) \end{matrix}

is provable in FPC_{=} by expanding the inner recursive type; the proof in FPC_{=} is straightforward, but the corresponding coercion functions are rather sophisticated.

Formally, we proceed as follows. For every proof of an equality O ⊢_{=} A = B or O ⊢_{=+} A = B we construct a pair of terms s and t such that O; ∅ ⊢ s : A \overleftarrow{→} B : t. The construction of s and t is by induction on the proof of the equality A = B; we give it in Figure 3.

Using the pairs of terms of Figure 3, we deduce that for every derivation of O; E ⊢_{=} e : C or O; E ⊢_{=+} e : C there exists a corresponding derivation O; E ⊢ e′ : C. This derivation is obtained by replacing applications of the rule (Retyping) (from O; E ⊢ e : A and O ⊢ A = B to O; E ⊢ e : B) with applications of → elimination (from O; E ⊢ e : A and O; E ⊢ s : A → B to O; E ⊢ s(e) : B).

Now that we have defined and used coercion functions, we face the problem of proving that they are reasonable (e.g., that they do not simply diverge). The equational rules β and η do not suffice for this proof, and we cannot use Scott induction directly (since the predicates in which we are interested are not admissible). Instead, we rely on a logic, which we introduce in section 5; we derive properties of the coercion functions in section 6.5.

5 A basic logic for FPC

We introduce a logic for reasoning about FPC programs. The logic is suggested by a call-by-value interpretation of FPC. It is a logic of definedness in the sense of Feferman [7] (or a logic of partial terms [4, 5]); it enables us to reason about terms which may or may not have a value. The use of a logic of definedness is important for two reasons:

1. In FPC, one can write terms that do not normalize.

2. Our main means for reasoning about recursion is Freyd’s Principle of Versality (or PV) [11]. This principle is compatible with the theory of the typed partial λ-calculus [15] formalisable within a logic of definedness, but is inconsistent with the equational theory of the simply-typed λ-calculus. This inconsistency arises because μX.X becomes a zero object (i.e., both initial and terminal), and then is isomorphic to every type.

Next we define the logic, and in section 6 we show some of its applications.

The language of the logic consists of the manysorted term algebra given by FPC types and terms, and the positive fragment of propositional calculus extended with equality (=_{A}) and a definedness predicate (↓_{A}). More precisely, the following rules define the well-formed formulas of the logic:

\frac{O; E ⊢ e : A O; E ⊢ e′ : A}{O; E ⊢ e =_{A} e′ wff}

\frac{O; E ⊢ e : A}{O; E ⊢ e ↓_{A} wff}

\frac{O; E ⊢ P wff O; E ⊢ Q wff}{O; E ⊢ P ∧ Q wff}

\frac{O; E ⊢ P wff O; E ⊢ Q wff}{O; E ⊢ P ⊃ Q wff}

Officially, the axioms and rules of the logic deal with judgments of the form O; E ⊢ P, which means that P is true given O and E. In what follows, we omit O and E; the axioms apply for any O and E such that O; E ⊢ P wff. We also omit types for free variables and in subscripts. The axioms and rules are:

I. Natural-deduction rules for ∧ and ⊃ :

\begin{matrix}\frac{P Q}{P ∧ Q} & \frac{P ∧ Q}{P} & \frac{P ∧ Q}{Q} \\ \frac{[P] ; ⋮ ; Q}{P ⊃ Q} & \frac{P P ⊃ Q}{Q} \end{matrix}

II. In logics of definedness, free variables are thought of as ranging over terms that exist (or denote a value). Hence, from a general assertion P [x] we can infer the assertion P [e] for a particular term e provided e exists:

e ↓ P [x] P [e] x not free in assumptions above P [x]

III. The assertion of an equality implicitly carries the assertion of the existence of the equated terms:

s = t ⊃ s ↓ ∧ t ↓

IV. The axioms for equality are as usual, except for substitutivity which holds only for the weaker notion of equality ≃_{A} (Kleene equality) that does not assert the existence of the equated terms. Formally, s ≃_{A} t stands for (s ↓_{A} ⊃ s =_{A} t) ∧ (t ↓_{A} ⊃ s =_{A} t). x = x x = y ⊃ y = x x = y ∧ y = z ⊃ x = z ⋀_{1≤i≤n}(s_{i} = t_{i}) ⊃ e[s_{1}, …, s_{n}] ≃ e[t_{1}, …, t_{n}]

V. For products, we have:

(s, t) ↓ ⊃ s ↓ ∧ t ↓ fst(e) ↓ ⊃ e ↓ snd(e) ↓ ⊃ e ↓ fst(x, y) = x snd(x, y) = y (fst(z), snd(z)) = z

VI. For exponentials, the axioms are those of the typed partial λ-calculus [18, 14, 15]:

(λx. e) ↓ s(t) ↓ ⊃ s ↓ ∧ t ↓ λx. e[x] = λy. e[y] (λx. e[x])(y) ≃ e[y] λx. fx = f

s[x] ≃ t[x] λx. s[x] = λx. t[x] x not free in assumptions above s[x] ≃ t[x]

Since the substitutivity axiom applies only to terms that are known to exist, the law for β equality is not equational but conditionally equational; we can derive: t ↓ ⊃ (λx. e[x])(t) ≃ e[t]. This is in accordance with the call-by-value interpretations of FPC. (Similar remarks apply to products and sums.)

VII. For sums, we have:

inl(e) ↓ ⊃ e ↓ inl(x) ↓ inr(e) ↓ ⊃ e ↓ inr(y) ↓ (case e of l(x).s or r(y).t) ↓ ⊃ e ↓ (case z of l(x).s[x] or r(y).t[y])

≃ (case z of l(x′).s[x′] or r(y′).t[y′]) (case inl(z) of l(x).s[x] or r(y).t) ≃ s[z] (case inr(z) of l(x).s or r(y).t[y]) ≃ t[z] (case z of l(x).e(inl(x)) or r(y).e(inr(y)))

≃ e(z) x, y not free in e

\frac{x, y not free in assumptions above s[x] ≃ s′[x] t[y] ≃ t′[y]}{(case z of l(x).s[x] or r(y).t[y]) ≃ (case z of l(x).s′[x] or r(y).t′[y])}

VIII. For recursion, we have:

fold(e) ↓ ⊃ e ↓

     fold(x) ↓

unfold(e) ↓ ⊃ e ↓

     unfold(x) ↓
     unfold(fold(x)) = x
     fold(unfold(x)) = x

it(ud_{μX.F} , fd_{μX.F}) = id_{μX.F} coit(ud_{μX.F} , fd_{μX.F}) = id_{μX.F}

PV: for f : F [A] \overleftarrow{→} A : g, v : A \overleftarrow{→} μX.F [X] : u, (v = fd ∘ F_{A,μX.F} (u, v) ∘ g) ∧ (u = f ∘ F_{μX.F,A}(v, u) ∘ ud)

⊃ v = coit(g, f) ∧ u = it(g, f)

This logic is essentially an extension of that of Plotkin [18] with new axioms for recursion. Three minor differences are worth noting. First, Plotkin works with a logic of existence [7] (or a logic of partial elements [20, 9]), where free variables are thought of as ranging over a domain of possibly non-existing elements. Second, he axiomatises approximation (⊑, ⊏ ∼) rather than equality. Finally, as here we are interested only in the minimal framework in which our results hold, we have adopted a weaker axiomatisation for sums which allows us to remain within the positive fragment of the propositional calculus.

The standard model of FPC, pCpo (the category of cpos and partial continuous functions), gives rise to a model of the logic; equality and existence have their usual meanings (see [18]).

6 Applications of the logic

In this section we develop several applications of our logic. We have two goals at once: (i) to explain the logic, and in particular the Principle of Versality; (ii) to prove that the definitions given in other sections (e.g., that of functors) yield desirable properties. Throughout, we reason rather informally; we often omit types, and when we assert an equality, we mean that it is provable in the logic.

6.1 Basic category theory

The first results are monoidal laws for identities and composition: e ∘ id_{A} ≃ e, id_{B} ∘ e ≃ e, and t ∘ (s ∘ e) ≃ (t ∘ s) ∘ e are provable (for appropriate A and B).

In addition, ×, →, and + are functorial in the following sense. We have id_{A} ⋆ id_{B} = id_{A⋆B} for ⋆ ∈ {×, →, +}, and (s′ × t′) ∘ (s × t) ≃ (s′ ∘ s) × (t′ ∘ t) and (s′ + t′) ∘ (s + t) ≃ (s′ ∘ s) + (t′ ∘ t), while (s′ → t′) ∘ (s → t) ≃ (s ∘ s′) → (t′ ∘ t).

6.2 Fixed-point operators

The operators of section 2.2 are provably fixed-point operators; moreover, coiterators and iterators satisfy the equations used for their recursive definitions:

fix = λf. λy. f (fix f) y
ffix = λf. (λy. fst (f(ffix f)) y,
λx. snd (f(ffix f)) x)
coit = λ(g, f). fd ∘ F (it(g, f), coit(g, f)) ∘ g
it = λ(g, f). f ∘ F (coit(g, f), it(g, f)) ∘ ud

6.3 Functoriality

Crucially, our functorial interpretation of type expressions does define functors:

Theorem 6.1 (Functoriality) Let O, X_{1}, …, X_{n} ⊢ F [X_{1}, …, X_{n}].

1. Existence: If O; E ⊢ f_{i} : A_{i} \overleftarrow{→} B_{i} : g_{i}, then F_{\overline{A},\overline{B}}(\overline{g, f}) ↓.

2. Identities are preserved: If O ⊢ A_{i} for i = 1..n, then F_{\overline{A},\overline{A}}(\overline{id_{A}, id_{A}}) = id_{F [\overline{A}]} where (id_{A})_{i} =^{Δ} id_{A_{i}}.

3. Composition is preserved: If O; E ⊢ f_{i} : A_{i} \overleftarrow{→} B_{i} : g_{i} and O; E ⊢ f′_{i} : B_{i} \overleftarrow{→} C_{i} : g′_{i}, for i = 1..n, then F_{\overline{B},\overline{C}}(\overline{g′, f′})∘F_{\overline{A},\overline{B}}(\overline{g, f}) = F_{\overline{A},\overline{C}}(\overline{g ∘ g′, f′ ∘ f})

where (g ∘ g′)_{i} =^{Δ} g_{i} ∘ g′_{i} and (f′ ∘ f)_{i} =^{Δ} f′_{i} ∘ f_{i}. □

The proof of this theorem relies on the Principle of Versality.

6.4 Example applications of the Principle of Versality

We show three additional consequences of the Principle of Versality.

Example 6.2 (PV for Nat) Let 0 =^{Δ} μX.X, 1 =^{Δ} 0 → 0, Nat =^{Δ} μX.1 + X, and then let * =^{Δ}

                                                 λx: 0. x, zero =^{Δ} fold_{Nat}(inl_{1,Nat}(*)), and succ(x) =^{Δ}

fold_{Nat}(inr_{1,Nat}(x)). For f : 1 + A \overleftarrow{→} A : g, we have the coiterator coit(g, f) : A → Nat such that

coit(g, f)(z) ≃ case g(z) of l(x).zero
or r(y).succ(coit(g, f)(y))

so that, roughly, whenever it is defined, coit(g, f)(z) is the least n for which g^{n+1}(z) = inl(*). We have also the iterator it(g, f) : Nat → A for which

it(g, f)(z) ≃ case unfold(z) of l(x).f(inl(*))
or r(y).f(inr(it(g, f)(y)))

so it(g, f)(zero) ≃ f(inl(*)) and it(g, f)(succ(x)) ≃ f(inr(it(g, f)(x))). Thus coiterators allow definitions by minimisation (in the sense of recursion theory), while iterators provide definitions by primitive recursion. □

Example 6.3 (PV for 0) Let 0 =^{Δ} μX.X. By PV, for g, f : A → A, the type 0 comes equipped with a unique coiterator and iterator characterised by:

[figure: 0; fd; 0; A; it(g, f); f; A; it(g, f)]

                0 ^{ud}     0

[figure: A; coit(g, f); g; A; coit(g, f)]

With A = 0, g = ud, f = fd, we deduce fd =

it(ud, fd) = id_{0} = coit(ud, fd) = ud. Then, for

v : A \overleftarrow{→} 0 : u, we obtain v = fd ∘ v ∘ id_{A} and u = id_{A} ∘ u ∘ ud, and hence v = coit(id_{A}, id_{A}) and u = it(id_{A}, id_{A}). Thus, 0 is a zero object. □

Example 6.4 (PV and retracts) For h : μX.F → μX.F, by PV we have

h = fd ∘ F (h, h) ∘ ud ⊃ h = it(ud, fd) = id

Further, for f : F [A] \overleftarrow{→} A : g such that g ∘ f = id_{F [A]} (that is, F [A] is provably a retract of A), we have that coit(g, f) ∘ it(g, f) = id_{μX.F} (that is, μX.F is provably a retract of A), since coit(g, f) ∘ it(g, f) = fd ∘ F (it(g, f), coit(g, f)) ∘ v ∘ u ∘ F (coit(g, f), it(g, f)) ∘ ud and then = fd ∘ F (coit(g, f) ∘ it(g, f), coit(g, f) ∘ it(g, f)) ∘ ud. □

6.5 Properties of coercion functions

We return once more to the problem of relating the formulations of FPC. In section 4 we have seen that for every equality A = B provable in either FPC_{=} or FPC_{=+} there is a corresponding pair of coercion functions s : A \overleftarrow{→} B : t; and for every typing e : C there is a corresponding typing e′ : C. Now we study some properties of s and t, showing that e and e′ are equivalent. In the case where O ⊢_{=} A = B, we can prove that s and t define an isomorphism. This means that O; ∅ ⊢ t∘ s = id_{A} and O; ∅ ⊢ s∘t = id_{B} are both provable in the logic of section 5. We write this as O; ∅ ⊢ s : A ≅ B : t. We further write O ⊢ A ≅ B when O; ∅ ⊢ s : A ≅ B : t for some s and t.

Theorem 6.5 For every derivation of

O, X_{1}, …, X_{n} ⊢_{=} F = G

with associated terms

O, X_{1}, …, X_{n}; ∅ ⊢ s : F \overleftarrow{→} G : t

we have that

O, X_{1}, …, X_{n}; ∅ ⊢ s : F ≅ G : t

In addition, for O; E ⊢ f_{i} : A_{i} \overleftarrow{→} B_{i} : g_{i}, the following naturality condition holds:

[figure: F [\overline{A}]; s[\overline{A}]; G[\overline{A}]; F [\overline{B}]; F (\overline{g, f}); s[\overline{B}]; G[\overline{B}]; G(\overline{g, f})]

[figure: F [\overline{A}]; t[\overline{A}]; G[\overline{A}]; F [\overline{B}]; F (\overline{f, g}); t[\overline{B}]; G[\overline{B}]; G(\overline{f, g})]

□

It follows that it is sound to interpret type equalities in FPC_{=} as isomorphisms in FPC:

Corollary 6.6 If O ⊢_{=} A = B then O ⊢ A ≅ B. □

Furthermore, whenever we transform O; E ⊢_{=} e : C into O; E ⊢ e′ : C, the terms e and e′ are equivalent. In order to make this claim precise, we consider a formalism where both e and e′ are legal terms; we extend the logic for FPC to the union of FPC and FPC_{=}, with the following new axioms and rules:

I. The constructs fold and unfold are computationally irrelevant:

fold_{μX.F} (x) =_{μX.F} x unfold(x) =_{μX.F} x II. Equal types can be used interchangeably: when-

ever A = B, x =_{A} y ⊃ x =_{B} y

We believe that the extended logic is sound for a per model, a call-by-value version of existing ones [2, 1].

With this extended logic, we obtain:

Lemma 6.7 If a proof of O ⊢_{=} A = B yields the coercion functions s and t such that O; ∅ ⊢ s : A \overleftarrow{→} B : t (according to Figure 3), then O; ∅ ⊢ s = id_{A} and O; ∅ ⊢ t = id_{B} are provable in the extended logic. □

Theorem 6.8 If O; E ⊢_{=} e : C and e′ is obtained from e by inserting coercion functions so that O; E ⊢ e′ : C (as described in section 4), then O; E ⊢ e ≃ e′ is provable in the extended logic. □

We cannot proceed identically for FPC_{=+}, because the rule (Contract) which distinguishes FPC_{=+} from FPC_{=} is not even sound when we interpret equality as natural isomorphism. For example, let C[X] = X × 1; clearly C[X] is contractive in X, and any A and B are naturally isomorphic to C[A] and C[B] respectively; the rule (Contract) would tell us that A and B are themselves isomorphic. This observation does not mean that FPC_{=+} is unsound, only that the isomorphism interpretation of the rule (Contract) is.

Still, whenever we transform O; E ⊢_{=+} e : C into O; E ⊢ e′ : C, the terms e and e′ are equivalent. Analogues of Lemma 6.7 and Theorem 6.8 hold for FPC_{=+}.

7 Conclusions

This paper explores some syntactic and logical issues for type systems with recursive types. Some of our results may be usually taken for granted. However, as we have found, they are rather delicate, and not easy reproductions of semantic results.

Much further work is possible. For example, it should be simple to extend our results to type systems with polymorphism. In a more logical direction, it may be interesting to revisit Pitts’ relational approach to reasoning with recursive types, and in particular his treatment of nested recursion [17].

Acknowledgments

We thank Roberto Amadio, Luca Cardelli, John Mitchell, Andy Pitts, and Gordon Plotkin for discussions on the subject of this work.

References

[1] Martín Abadi and Gordon Plotkin. A per model of polymorphism and recursive types. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 355–365, 1990.

[2] Roberto M. Amadio. Recursion over realizability structures. Information and Computation, 91(1):55–85, 1991.

[3] Roberto M. Amadio and Luca Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575–631, September 1993.

[4] M. Beeson. Formalizing constructive mathematics: why and how? In Constructive Mathematics, volume 873 of Lecture Notes in Mathematics, pages 146–190. Springer-Verlag, 1981.

[5] M. Beeson. Foundations of Constructive Mathematics. Springer-Verlag, 1985.

[6] Val Breazu-Tannen, Thierry Coquand, Carl A. Gunter, and Andre Scedrov. Inheritance as implicit coercion. Information and Computation, 93(1):172–222, July 1991.

[7] S. Feferman. Definedness. Manuscript (Lecture for mini-conference on Partial Functions and Programming: Foundational Questions), May 1995.

[8] M.P. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. PhD thesis, University of Edinburgh, 1994. To be published by Cambridge University Press in the Distinguished Dissertations Series.

[9] M.P. Fourman. The logic of topoi. In J. Barwise, editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic. North Holland, 1977.

[10] P.J. Freyd. Recursive types reduced to inductive types. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 498–507, 1990.

[11] P.J. Freyd. Algebraically complete categories. In A. Carboni, M.C. Pedicchio, and G. Rosolini, editors, Category Theory, volume 1488 of Lecture Notes in Mathematics, pages 131–156. Springer-Verlag, 1991.

[12] M.H. Gordon, R.M. Milner, and C. Wadsworth. Edinburgh LCF, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.

[13] Carl Gunter. Semantics of Programming Languages: Structures and Techniques. Foundations of Computing Series. The MIT Press, Cambridge, Massachusetts, 1992.

[14] E. Moggi. Categories of partial morphisms and the partial lambda-calculus. In Proceedings Workshop on Category Theory and Computer Programming, Guildford 1985, volume 240 of Lecture Notes in Computer Science. Springer-Verlag, 1986.

[15] E. Moggi. The Partial Lambda-Calculus. PhD thesis, University of Edinburgh, 1987.

[16] Greg Nelson, editor. Systems Programming in Modula-3. Prentice Hall, 1991.

[17] A.M. Pitts. Relational properties of recursively defined domains. In Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science, pages 86–97, 1993. An expanded version will appear in Information and Computation.

[18] G.D. Plotkin. Denotational semantics with partial functions. Lecture at C.S.L.I. Summer School, 1985.

[19] G.D. Plotkin. Type theory and recursion (extended abstract). In Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science, page 374, 1993.

[20] D.S. Scott. Identity and existence in intuitionistic logic. In M.P. Fourman, C.J. Mulvey, and D.S. Scott, editors, Applications of Sheaves, volume 753 of Lecture Notes in Mathematics. Springer-Verlag, 1979.

[21] M.B. Smyth and G.D. Plotkin. The categorytheoretic solution of recursive domain equations. SIAM Journal of Computing, 11(4):761–783, 1982.

[22] P. Urzyczyn. Positive recursive type assignment. In Mathematical Foundations of Computer Science, volume 969 of Lecture Notes in Computer Science. Springer-Verlag, 1995.

Appendix: review of core FPC

These are basic rules for FPC. Additional rules for recursive types appear in section 2.

Type contexts. A type context is a list of distinct type variables. We write O ⊢ ⋄ to indicate that O is a well-formed type context. The rules for this judgment are:

\overline{∅ ⊢ ⋄} \frac{O ⊢ ⋄}{O, X ⊢ ⋄} X ∉ O

Types. As types, we have type variables, product types, function types, sum types, and recursive types. We write O ⊢ A to indicate that A is a well-formed type in the type context O:

\begin{matrix}\frac{O ⊢ ⋄}{O ⊢ X} X ∈ O \\ \frac{O ⊢ A O ⊢ B}{O ⊢ A ⋆ B} ⋆ ∈ \{×, →, +\} \frac{O, X ⊢ F}{O ⊢ μX.F} \end{matrix}

Term contexts. A term context is a list of distinct variables with types. We write O ⊢ E to indicate that E is a well-formed term context in the type context O:

\frac{O ⊢ ⋄}{O ⊢ ∅} \frac{O ⊢ E O ⊢ A}{O ⊢ E, x: A} x ∉ dom(E)

Terms. As terms, we have variables, products, functions, and sums. We write O; E ⊢ e : A to indicate that term e has type A in the type context O and the term context E.

\frac{O ⊢ E}{O; E ⊢ x : A} (x: A) ∈ E

\frac{O; E ⊢ s : A O; E ⊢ t : B}{O; E ⊢ (s, t) : A × B}

\frac{O; E ⊢ e : A × B}{O; E ⊢ fst(e) : A}

\frac{O; E ⊢ e : A × B}{O; E ⊢ snd(e) : B}

\frac{O; E, x: A ⊢ e : B}{O; E ⊢ λx: A. e : A → B}

\frac{O; E ⊢ s : A → B O; E ⊢ t : A}{O; E ⊢ s(t) : B}

\frac{O; E ⊢ e : A O ⊢ B}{O; E ⊢ inl_{A,B}(e) : A + B}

\frac{O ⊢ A O; E ⊢ e : B}{O; E ⊢ inr_{A,B}(e) : A + B}

\frac{\begin{matrix}O; E ⊢ e : A + B \\ O; E, x: A ⊢ s : C \\ O; E, y: B ⊢ t : C \end{matrix}}{O; E ⊢ case e of l(x).s or r(y).t : C}