Metatheorems about Convertibility in Typed Lambda Calculi: Applications to CPS transform and ”Free Theorems”

by

Jakov Kučan

B.S.E., University of Pennsylvania (1991) M.A., University of Pennsylvania (1991) Submitted to the Department of Mathematics in partial fulfillment of the requirements for the degree of Doctor of Philosophy at the MASSACHUSETTS INSTITUTE OF TECHNOLOGY February 1997 \begin{matrix}c \\ ◯ \end{matrix} Massachusetts Institute of Technology 1997. All rights reserved.

Author . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Department of Mathematics October 10, 1996

Certified by . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Albert R. Meyer

Hitachi America Professor of Engineering Thesis Supervisor

Accepted by . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Hung Cheng

Chairman, Applied Mathematics Committee Metatheorems about Convertibility in Typed Lambda Calculi: Applications to CPS transform and ”Free Theorems” by Jakov Kučan

Submitted to the Department of Mathematics on October 10, 1996, in partial fulfillment of the requirements for the degree of Doctor of Philosophy

Abstract

In this thesis we present two applications of using types of a typed lambda calculus to derive equation schemas, instances of which are provable by convertibility.

Part 1: Retraction Approach to CPS transform: We study the continuation passing style (CPS) transform and its generalization, the computational transform, in which the notion of computation is generalized from continuation passing to an arbitrary one. To establish a relation between direct style and continuation passing style interpretation of sequential callby-value programs, we prove the Retraction Theorem which says that a lambda term can be recovered from its continuationized form via a λ-definable retraction. The Retraction Theorem is proved in the logic of computational lambda calculus for the simply typable terms.

Part 2: Another look at ”Theorems for Free!”: We reexamine Wadler’s “free theorems”

— theorems about polymorphic functions derivable from the type of the function — in an extension of Mairson’s syntactic treatment of logical relations. Logical relations are defined as formulas in second (and higher) order logic over untyped lambda terms, from which we can instantiate equations involving a given term. As a consequence we can formulate a free theorem as an equation schema, each instance of which is provable by convertibility, given typing conditions on the terms involved are met. In our framework datatypes are represented as free algebras generated by constants, and we define sufficient conditions which a representation of a datatype must satisfy to preserve free theorems. As a special case we prove examples of free theorems, as equations by convertibility, using Böhm-Berarducci representation of datatypes.

Thesis Supervisor: Albert R. Meyer Title: Hitachi America Professor of Engineering

Thanks

I would like to thank to all who, in one way or another, helped and inspired me in this work: to my advisor, Albert Meyer, for bearing with me over the years and teaching me how to say what I think (I’m still learning); to Lotus Development for the “real world” experience; to Harry Mairson for saving me from bankruptcy in the last moment; to fellow students and officemates.

Lastly, thanks to my wife Jadranka, just for being a wife of a graduate student.

Contents

1 Retraction Approach to CPS Transform 9 1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.2 Setup and Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

1.2.1 Lambda Calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 1.2.2 Monads and computational effects . . . . . . . . . . . . . . . . . . . 19 1.2.3 Computational lambda calculus . . . . . . . . . . . . . . . . . . . . . 21 1.2.4 Monadic metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . 26 1.2.5 Calculi λ_{n}, λ_{n∀}, λ_{cp∀}, etc. . . . . . . . . . . . . . . . . . . . . . . . . 27

1.3 Source to Source Transforms . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1.3.1 The computational transform . . . . . . . . . . . . . . . . . . . . . . 30 1.3.2 The modified computational transform . . . . . . . . . . . . . . . . . 31 1.3.3 The CPS transform . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 1.3.4 The modified CPS transform . . . . . . . . . . . . . . . . . . . . . . 34

1.4 Retractions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 1.5 The Retraction Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36

1.5.1 Interpretation of terms and types . . . . . . . . . . . . . . . . . . . . 36 1.5.2 The Retraction Theorem for the modified computational transform . 39 1.5.3 Back to CPS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 1.5.4 The state passing style transform . . . . . . . . . . . . . . . . . . . . 44 1.5.5 Extensions of the main results . . . . . . . . . . . . . . . . . . . . . 46

1.6 Applications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 1.7 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 1.8 Some Open Questions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 1.9 Appendix . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57

1.9.1 Monads . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 1.9.2 Extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59

1.10 Acknowledgments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64

2 Another Look at “Theorems for Free!” 65 2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 2.2 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67

2.2.1 Untyped λ-calculus and λ-theories . . . . . . . . . . . . . . . . . . . 67 2.2.2 Type Inference System F_{ω}+𝔗𝔥 . . . . . . . . . . . . . . . . . . . . . 68 2.2.3 Data Structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 2.2.4 Programs over λ-terms . . . . . . . . . . . . . . . . . . . . . . . . . . 70 2.2.5 Type Theory over λ-terms . . . . . . . . . . . . . . . . . . . . . . . . 71 2.2.6 Semantics of Type Theory . . . . . . . . . . . . . . . . . . . . . . . . 73 2.2.7 Models of Type Inference . . . . . . . . . . . . . . . . . . . . . . . . 74 2.2.8 Logical Relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75

2.3 The Fundamental Theorem of Logical Relations . . . . . . . . . . . . . . . . 76 2.4 Deriving the Free Theorems . . . . . . . . . . . . . . . . . . . . . . . . . . . 81 2.5 Representation of Constants . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 2.6 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91 2.7 Acknowledgments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92

Chapter 1

Retraction Approach to CPS Transform

Abstract: We study the continuation passing style (CPS) transform and its generalization, the computational transform, in which the notion of computation is generalized from continuation passing to an arbitrary one. To establish a relation between direct style and continuation passing style interpretation of sequential call-by-value programs, we prove the Retraction Theorem which says that a lambda term can be recovered from its continuationized form via a λ-definable retraction. The Retraction Theorem is proved in the logic of computational lambda calculus for the simply typable terms.

1.1 Introduction

The notions of a continuation and a continuation passing style (CPS) transform have been introduced by a number of authors (see [Rey93] for a historical overview). The main motivation for the independent developments of these concepts seemed to be twofold: explaining the behavior of imperative features in functional languages, and compilation of programs with higher order procedures. Further research led to development of CPS denotational semantics [SW74] (see also [Sto77]), and later categorical semantics of computations [Mog89], as well as compilers based on the CPS transform [Ste78] (see also [App92]). In both kinds of applications one of the central goals of the research has been to establish a relationship between original terms and their images under the transform.

Motivation: Plotkin [Plo75] has shown that the CPS transform^{1} preserves equalities between lambda terms provable in call-by-value calculus λ_{v}.

Theorem 1.1.1 (Plotkin). For any two lambda terms M and N,

λ_{v} ⊢ M = N implies λ_{n} ⊢ \overline{M} = \overline{N},

1Unless otherwise stated, we are referring to a call-by-value variant of the CPS transform.

where \overline{M} and \overline{N} denote the CPS transforms of M and N, and λ_{v} and λ_{n} are call-by-value and call-by-name equational logics. ^{2}

He has also shown that the converse of this theorem is not true by presenting several examples of equations which ought to hold in a sequential call-by-value language, but are not provable in λ_{v}. Sabry and Felleisen [SF92] strengthened Plotkin’s result by extending the logic of λ_{v} to what turns out to be Moggi’s computational lambda calculus λ_{cp}^{3}, to prove the equational correspondence result.

Theorem 1.1.2 (Sabry-Felleisen). For any two lambda terms M and N,

λ_{cp} ⊢ M = N iff λ_{n} ⊢ \overline{M} = \overline{N}.

Sabry-Felleisen’s result says that the CPS transform is a function mapping lambda terms to lambda terms that preserves λ_{cp}-equality, as well as distinctions. To state the problem we are trying to solve precisely, we observe that left-to-right implication of the theorem says that the CPS transform defines a function, call it B, mapping λ_{cp}-equivalence classes to λ_{n}-equivalence classes of terms. In fact Sabry and Felleisen’s proof of the above theorem is based on a construction of such a function. The right-to-left implication says that B is injective and therefore has a left inverse B^{−1}. To strengthen Sabry-Felleisen’s result we ask whether B or B^{−1} are lambda definable. More precisely we ask the following questions:

• Is there as lambda term P, such that

λ_{n} ⊢ (P M) = \overline{M}?

• Is there a lambda term R, such that

λ_{cp} ⊢ (R \overline{M}) = M?

The answer to the first question, as shown by Meyer and Riecke [MR], is “no”. The Retraction Theorem, which is the main result of this work, answers the second question affirmatively. However, instead of giving a single lambda term R that defines the inverse of the CPS transform, we will show there is a type indexed family of terms, R_{σ}, such that for every closed term M of type σ, λ_{cp} ⊢ M = (R_{σ} \overline{M}).

A version of the Retraction Theorem was first presented by Meyer and Wand [MW85] in the following form.

Theorem 1.1.3 (Meyer-Wand). For any simple type σ, there is a term R_{σ}, such that for a closed term M, of type σ

λ_{n} ⊢ M = (R_{σ} \overline{M}).

2In Plotkin’s work, λ_{v} denotes β_{v}-convertibility, while λ_{n} denotes β-convertibility. In this paper, we assume λ_{v} and λ_{v} also contain axioms (η_{v}) and (η) respectively.

3We use λ_{cp} to denote the pure segment of Moggi’s calculus, while λ_{c} denotes the complete calculus.

While certainly true, as the authors have pointed out to us, this theorem is somewhat misleading. The variant of the CPS transform is the call-by-value transform which makes the computational structure of the term M explicit, but under assumption that M is to be evaluated under a call-by-value evaluation strategy. The transform does not tell us anything about how M would behave under a call-by-name evaluation. Therefore, we expect the equality M = (R_{σ} \overline{M}) to tell us something about the term M and its CPS form in a context of call-by-value evaluation. In Meyer-Wand Theorem, this equality is an equality in λ_{n}, which is a call-by-name logic and is not sound for call-by-value reasoning. This limits the applications of the theorem to setting in which call-by-name and call-by-value coincide (e.g. for pure simply typed terms). To apply the theorem in a wider range of settings, we need to weaken the logic in which the conclusion of the theorem is proved.

The main contribution of this paper is a stronger and, by above considerations, correct version of the Retraction Theorem where provability in λ_{n} is replaced with provability in Moggi’s λ_{cp}. Note that, while stronger than λ_{v}, the logic of λ_{cp} is still sound for call-by-value reasoning, that is, a closed term is equivalent to a value (a variable or a lambda abstraction) under λ_{cp} if and only if it is equivalent to a value under λ_{v} [Mog88]. Our version of the Retraction Theorem reads as follows.

Theorem 1.1.4 (Retraction). For any simple type σ, there is a term R_{σ}, such that for a closed term M, of type σ

λ_{cp} ⊢ M = (R_{σ} \overline{M}).

Moreover, we will show that this is the strongest possible version of the Retraction Theorem, meaning λ_{cp} is the weakest logic in which the conclusion of the theorem holds.

Lambda calculi: Before we go any further, to make our exposition easier to read we summarize some of the key concepts and explain the notation we use. A more detailed treatment is given in Section 1.2. The phrase lambda calculus refers to a set of terms — the language of the calculus — and a set of provable equations — the logic (or the theory) of the calculus.^{4} We will consider several different calculi whose languages will consist of terms closed under lambda abstraction and application, with possible extensions specific to each calculus. The logic of a calculus is intended to model specific computational behavior of the terms of the calculus.

We view the CPS transform, and its generalization, the computational transform, as interpretations of a sequential call-by-value functional programming language with possible “impure” features (continuations, mutable store, exceptions, nondeterminism, etc.). For the programming language we choose Moggi’s λ_{cp} calculus for the following reasons: the logic of λ_{cp} is sound for call-by-value reasoning, and it is complete with respect to a class of models in which most commonly used “impure” features can be represented. We concentrate on the the pure simply typed terms first, and later discuss possible extensions that would make λ_{cp} a more realistic programming language.

4We also consider a type system to be a part of the calculus, but we postpone the discussion of type systems to Section 1.2.

The language of λ_{cp} consist of terms formed by abstraction, application and letexpressions. However, the let-expressions can be treated as syntactic sugar. The logic of λ_{cp} contains (β_{v}) and (η_{v}), and additional axioms that allow proving equations like ((λx.x) M) = M. The complete definition of λ_{cp} is given in section 1.2.3.

For the codomains of the transforms, we define calculi λ_{n}, λ_{ml}, and λ_{c}. Calculus λ_{n} is a call-by-name calculus, the language of which consists only of terms formed by application and abstraction. The logic of λ_{n} is the βη-theory. We use λ_{n} as the codomain of the CPS transform. Calculus λ_{ml} is what Moggi calls a “monadic metalanguage”. We define it as an extension of λ_{n} with monadic constructs [M]_{T} and (let_{T} x⇐M in N). The axioms of λ_{ml} extend those of λ_{n} with axioms corresponding to monad laws (see sections 1.2.2 and 1.2.4). λ_{ml} is the codomain of the computational transform. Finally we define calculus λ_{c} as an extensions of λ_{cp} with constructs [M] and μ(M) satisfying axioms [μ(V)] = V and μ([M]) = M, where M is an arbitrary term, and V is a value (a variable, an abstraction, or a term of the form [M]). λ_{c} will serve as a codomain of the modified computational transform.

In our discussion, we also refer to the calculus λ_{v}. The language if λ_{v} contains terms formed by application and abstraction, and its logic is defined by (β_{v}) and (η_{v}) axioms.

We say a calculus λ′ is an extension of a calculus λ if the theory of λ is a subset of the theory of λ′. In such cases we write λ ⊆ λ′. Since we assume reflexivity is an axiom in every lambda theory, this implies that the language of λ is contained in the language of λ′ whenever λ ⊆ λ′.

The five calculi described above are related as follows:

λ_{v} ⊆ λ_{cp} ⊆ λ_{n} ⊆ λ_{ml}  and  λ_{cp} ⊆ λ_{c} .

Transforms: In addition to the CPS transform, we study its generalization, the computational transform mapping λ_{cp} to λ_{ml}. As we explain below, it is not possible to generalize the Retraction Theorem to the computational transform. Thus, we will define the modified computational transform mapping λ_{cp} to λ_{c}. We also study the modified CPS transform that can be viewed as a special case of the modified computational transform. If M is a λ_{cp} term, we write \overline{M} to denote the CPS transform of M, \overline{\overline{M}} to denote the computational

transform of M, \overline{\overline{M}}^{♯} to denote the modified computational transform of M, and \overline{M}^{♯} for the modified CPS transform of M. Figure 1-1 gives an intuitive picture of the transforms we study. We use symbols T_{ml}, T_{ml♯}, T_{cps}, and T_{cps♯} to denote the computational, modified computational, CPS, and modified CPS transform respectively. Transforms T_{♯} and T_{♯}^{K} are the auxiliary transforms modifying T_{ml} and T_{cps}.

The CPS transform can be viewed as a function mapping lambda terms to lambda terms. However, we believe that this view is overly simplistic and undermines essential properties of the CPS transform. Even though, languages of λ_{v}, λ_{cp} and λ_{n} coincide, the logics of these calculi are very different. Looking at the CPS transform as a function mapping a lambda terms to lambda terms, while forgetting associated logic of the calculus, can be confusing and lead to misleading results. To get things straight we define the CPS transform as a function form one calculus to another. In other words, we make a distinction between languages of different calculi even though they may contain exactly the same terms. For example, if a term M is considered in a context of λ_{cp} calculus it will be regarded as a λ_{cp}

[figure: λ_{cp}; T_{ml}; T_{ml♯}; λ_{ml}; T_{♯}; λ_{cp}; T_{cps}; T_{cps♯}; λ_{cp} λ_{n}; T_{♯}^{K}; λ_{c}; λ_{cp}]

Figure 1-1: Summary of the transforms.

term, but the same term in the context of λ_{n} calculus will be regarded as a λ_{n} term. The problem of defining the correct domain and codomain of the CPS transform does not have a unique solution. For instance, Plotkin defined the CPS transform mapping λ_{v} into λ_{n}. The precise question we are trying to answer in this work is whether there is a λ_{cp} term R_{σ} such that for each λ_{cp} term of type σ, the equality M = (R_{σ} \overline{M}) is provable in λ_{cp}. This formulation requires that we view the CPS transform as a mapping from λ_{cp} to λ_{cp}. We now justify it is correct to do so.

One of the main features of the CPS transform is that it makes the computational structure of a term explicit in terms of continuations. More precisely, the control of how to evaluate the rest of the program is encoded in a continuation which is passed to each function as an explicit argument. In particular we consider the call-by-value variant of the CPS transform which encodes the call-by-value order of evaluation. The logic of λ_{cp} is sound for call-by-value reasoning and, in fact, the CPS transform preserves λ_{cp}-equality, so λ_{cp} is a correct domain for the CPS transform. To show that λ_{cp} is a correct codomain of the transform, consider Plotkin’s indifference result:

Theorem 1.1.5 (Plotkin). For any two lambda terms M and N,

λ_{v} ⊢ \overline{M} = \overline{N} iff λ_{n} ⊢ \overline{M} = \overline{N}.

This theorem, as shown in [SW96] can be extended to λ_{cp}.

Theorem 1.1.6 (Sabry-Wadler). For any two lambda terms M and N,

λ_{cp} ⊢ \overline{M} = \overline{N} iff λ_{n} ⊢ \overline{M} = \overline{N}.

By these results, λ_{n} restricted to the image of the CPS transform is a conservative extension of λ_{cp} restricted to the same set of terms. Therefore on terms in the image of the CPS transform logics of λ_{n} and λ_{cp} coincide. Combined with Theorem 1.1.2, we conclude that

λ_{cp} ⊢ M = N iff λ_{cp} ⊢ \overline{M} = \overline{N}.

Hence, without loss of generality, the CPS transform can be viewed as a transform from λ_{cp} into λ_{cp}.

The CPS transform gives purely functional interpretation of the control of the execution of a program. Similarly, one can give a functional interpretation of a program that manipulates mutable store by passing the state of the store explicitly in every function call, yielding a state passing style transform. As pointed out by Moggi [Mog88], many other computational effects, such as nondeterminism, divergence, interactive I/O, etc., can be treated in a similar way. Abstracting away from particular properties of each computational effect we arrive at what we call the computational transform. However, the codomain of the computational transform is λ_{ml} calculus, which makes it impossible to obtain a desired generalization of the Retractions Theorem. For this reason we will modify the computation transform to obtain a transform from λ_{cp} to λ_{c}, for which we prove the Retraction Theorem in the logic of λ_{c}.

Results: We have already stated the main result of this work, the Retraction Theorem for the CPS transform (Theorem 1.1.4). We also prove versions of the Retraction Theorem for the modified computational transform and the modified CPS transform. We now discuss these results.

Since our version of the Retraction Theorem for the CPS transform is provable in the logic of λ_{cp}, it is valid in all models of Moggi’s computational lambda calculus, which can model sequential programming languages that include a variety of common features like mutable store, exceptions, nondeterminism, etc.

We also claim that our version of the Retraction Theorem is the strongest possible, in the sense that it cannot be proven in a logic, extending λ_{v}, that is weaker than λ_{cp}. More formally,

Proposition 1.1.7. Let λ be an extension of λ_{v} in which we can prove the Retraction Theorem,

λ ⊢ M = (R_{σ} \overline{M}).  (1.1)

Then, λ is an extension of λ_{cp}.

Proof: Let σ be a simple type and let M and N be closed terms of type σ such that λ_{cp} ⊢ M = N. By Sabry-Felleisen’s equational correspondence we have that λ_{n} ⊢ \overline{M} = \overline{N}, and by Plotkin’s indifference result λ_{v} ⊢ \overline{M} = \overline{N}, and therefore λ ⊢ \overline{M} = \overline{N}. This, by equation (1.1) and congruence, implies that λ ⊢ M = N, so λ_{cp} ⊆ λ.

Viewing the computational transform as a generalization of the CPS transform, a natural question arises whether the Retraction Theorem generalizes to the computational transform T_{ml}. In order to answer this question, that is, to find a definable inverse of T_{ml}, we need to make clear in which calculus the inverse should be definable. As explained in Section 1.3.1, T_{ml} is a transform from λ_{cp} into λ_{ml}. We want to formulate the retraction theorem in a logic that is sound for call-by-value reasoning. The analysis presented for the CPS transform, in which we show the codomain of the CPS transform is λ_{cp}, does not generalize, since the computational transform, \overline{\overline{M}}, of a term M is not a term in the language of λ_{cp}. On the other hand, while it is possible to formulate the Retraction Theorem in the logic of λ_{ml} (since λ_{cp} ⊆ λ_{ml}) to obtain the version below, the logic of λ_{ml} is a call-by-name logic which is not sound for call-by-value reasoning. In fact, the Meyer-Wand formulation of the Retraction Theorem is a special case of the following theorem.

Theorem 1.1.8. For any simple type σ there is a term R_{σ}, such that for every closed term M of type σ,

λ_{ml} ⊢ M = (R_{σ} \overline{\overline{M}}).

To get a more meaningful generalization of the Retraction Theorem we use the modified computational transform T_{ml♯}. The modified transform maps λ_{cp} to λ_{c}. We prove the Retraction Theorem for the modified computational transform in the logic of λ_{c}, which is conservative over λ_{cp}, and is sound for call-by-value reasoning. Namely we show:

Theorem 1.1.9. For any simple type σ there is a λ_{c} term R_{σ}, such that for every closed term M of type σ,

λ_{c} ⊢ M = (R_{σ} \overline{\overline{M}}^{♯}).

Even though the Retraction Theorem for the CPS transform will not follow as a corollary of the above theorem, we feel that we benefit from studying the modified transform by abstracting away from particulars of the CPS transform in the more general setting.

Our results are pictured in Figure 1-2. Arrows R_{σ} and R_{σ}^{K} denote the definable retractions for the modified computational transform, T_{ml♯}, and the CPS transform, T_{cps}, respectively. Note that R_{σ}^{K} is also a retraction of the modified CPS transform T_{cps♯}. The first diagram presents a general case, and the second diagram can be viewed as a special case for the CPS transform. One could also consider the state passing style transform, as another special case.

[figure: λ_{cp}; T_{ml}; T_{ml♯}; λ_{ml}; T_{♯}; λ_{cp}; T_{cps}; T_{cps♯}; λ_{cp} λ_{n}; T_{♯}^{K}; R_{σ}^{K}; λ_{c}; R_{σ}; λ_{cp}; R_{σ}^{K}]

Figure 1-2: Summary of the results.

Outline of the proof: Our proof method is a generalization of the evaluation semantics developed by McAllester et al. [MKO95], which in turn can be viewed as defining a Mitchell’s model of type inference [Mit88]. The method also has roots in Girard’s method of Candidats de Reducibilité [Gir71, Gir72]. However, it must be pointed out that fore mentioned proof methods are tuned for proving properties of lambda terms in the βη-logic. Since our results hold in the weaker logic of λ_{cp} (and λ_{c}), we take a somewhat less structured approach.

We define define interpretations of terms and types and show that the two interpretations are related. More precisely, the meaning of a term is defined to be its CPS transform (or modified CT), while types are interpreted as sets of certain terms in the image of the transform which represent effect-free computations. The meanings of terms and types are related by an ε-relation, the purpose of which is to separate the meaning of a term into a part representing its effect-free computation and a part containing its computational effects (if any). The meaning of a term is said to be ε-related to a type set, interpreting the corresponding type, if its effect-free part is an element of the type set.

Remark. There are several flavors of the CPS transform. With respect to evaluation strategy we have call-by-value and call-by-name variants of the transform, and with respect to evaluation order, we have left-to-right and right-to-left variants. In this paper we focus on call-by-value CPS transform, and assume left-to-right evaluation order. Assuming the proper adjustments, viz. axioms of λ_{c} need to be modified slightly, all of the results apply when right-to-left evaluation order is assumed. We could also consider call-by-name evaluation strategy to obtain analogous results.

1.2 Setup and Definitions

In this section we will review the definitions of the elementary concepts used in this paper.

1.2.1 Lambda Calculi

From a computer scientist’s point of view, the simply typed lambda calculus represents the essence of sequential functional programming. In simply typed lambda calculus functions are represented by lambda abstractions, and evaluation is represented by a reduction relation. In programming languages, there are different strategies of evaluating function application (function can be evaluated before of after its argument, the argument may or may not be evaluated before it is passed to a function, etc.). In lambda calculus formulation, these strategies are represented by different variants of reduction relation (e.g. β, β_{v}, etc.), thus giving us different lambda calculi. Instead of reduction relation, in this work, we study its symmetric closure, i.e. an equivalence relation on lambda terms. Therefore, for our purposes, a lambda calculus is defined by the following parts:

• the language of the calculus defined by a grammar for forming untyped terms,

• the equational logic of the calculus given by a set of axioms, and

• the type system consisting of set of types and a deductive system for proving typing sequents.

Different lambda calculi will be denoted by the symbol λ with subscripts. We will often use the term calculus and the symbol λ to refer to any part of the calculus.

Language: For each calculus we give a grammar defining the set of terms of the calculus. In call-by-value calculi (for example, λ_{cp} and λ_{c}), we define a distinguished subset of the terms called values. Typically, variables and lambda abstractions will be considered values. Throughout this paper, unless indicated otherwise, letters M, N, P and Q are assumed to range over arbitrary terms, while letters U, V and W range over values.

Terms are defined over an infinite set of variables (we use letters x, y and z to range over variables). A number of constructs are said to bind a variable within a given scope. In particular, in term λx.M, λx binds variable x in M. Similarly, in term (let x=M in N), x is bound in N, but not in M, and likewise for (let_{T} x⇐M in N). If a variable x, occurring in M, is not bound we say it is free in M, denoted by x ∈ FV(M). We consider two terms the same if they are identical up to the names of bound variables.

A substitution is a function mapping variables to terms. In call-by-value calculi we only consider substitutions mapping variables to values. A substitution ρ is often applied to a term M, yielding the term ρM which is equal to M with ρ(x) substituted in M for all free occurrences of a variable x. We assume the substitution is done in the standard way to avoid incorrect capture of free variables in the term being substituted (renaming bound variables if necessary).

If ρ is a substitution we write ρ{V/x} for the substitution that coincides with ρ at all variables, except possibly x where it equals V. We will also write M{V/x} for the term obtained by substituting V for all free occurrences of x in M.

For notational convenience we will also use contexts. A context can be viewed as a term with a singe free occurrence of a special variable, called a hole, denoted by ⟨[·]⟩. The hole in a context C⟨[·]⟩ can be replaced by a term M to obtain the term C⟨[M]⟩. The difference between substituting a term for a variable, and replacing a term for the hole is that in the latter case, no renaming of bound variables is done to avoid capture of free variables in the term being substituted. Consequently, free variables in M can become bound in C⟨[M]⟩.

Note that while we define the language without any reference to types, in our work, we assume all terms as typable in the appropriate type inference system.

Type inference system: To define a type system of a calculus we first give a grammar for forming types. The type systems we consider consist of simple types with appropriate extensions. Thus types will generally include a base type ı and functional types σ→τ, where both σ and τ are types. We use letters σ and τ to range over types.

A type assertion is an expression of the form M: σ, where M is a term and σ is a type. A typing hypothesis, Γ, is a set of type assertions of the form x: σ, such that no variable occurs in two assertions in Γ. We write Γ, x: σ for the typing hypothesis Γ ∪ {x: σ}, and assume that x does not occur in Γ. Finally, a typing sequent is an expression of the form Γ ▷ M: σ, where Γ is a typing hypothesis, M is a term, and σ is a type.

For each calculus we will give a set of axioms and rules for deriving typing sequents. If not specified otherwise, we only consider derivable typing sequents. We will often subscript the symbol ▷ to disambiguate in which system, the sequent is derivable.

Equational logic: There are two ways of defining the equational logic of the calculus. In first, one considers equations in context, i.e. sequents of the form Γ▷M=N : σ, where Γ is a typing hypothesis, M and N are terms, and σ is a type. Whenever we write Γ ▷ M=N : σ, we assume that typing sequents Γ ▷ M: σ and Γ ▷ N: σ are derivable in the type system of the calculus.

On the other hand, one can consider untyped equations, i.e. formulas of the form M = N, where M and N are untyped terms.

We point out that these two approaches give different theories, since the untyped theory proves equations between terms that may not be typable. If an equation in context Γ ▷ M=N : σ is provable, then the corresponding untyped equation, M = N, is provable as well. Conversely, if M and N are terms such that Γ ▷ M: σ and Γ ▷ N: σ, and M = N is an equation of the untyped theory, the equation Γ ▷ M=N : σ is also provable provided the Church-Rosser property^{5} and subject reduction property^{6} hold for the calculus. For the calculi we study in this work, both properties hold, so the untyped theory does not prove any new equations between terms typable with the same type. Moreover, we only prove equations between terms of the same type, so we can omit the type information from the equations, keeping in mind that all terms in the equations are appropriately typable.

A lambda congruence is a set of equations derivable using axioms and rules in Table 1.1. Note that in all the rules and axioms, the terms are assumed to range over the language of a particular calculus.

M = M  (refl)_{\frac{M = N}{N = M}  (sym)} \frac{M = P, P = N}{M = N}  (trans)

\frac{M = N}{C⟨[M]⟩ = C⟨[N]⟩}  (congr)

Table 1.1: Axioms and rules of lambda congruence.

With every calculus we associate a set of axioms (in addition to those of lambda congruence) to define the equational logic of the calculus. If an equation is provable form the set of axioms λ, using the axioms and rules of lambda congruence, we write

λ ⊢ M = N,

or just M = N when it is understood that the equation is provable.

Notational conventions: When writing terms and types, we use parentheses freely to make expressions easier to read. In doing so we assume application of terms associates to the left, so that ((M N) P) can be written as (M N P), and the function space type constructor, →, associates to the right, so that σ→(τ→υ) can be written σ→τ→υ. We may also write M(N) for (M N), etc.

5A reduction relation ↠^{∗} is said to be Church-Rosser if whenever M ↠^{∗} M_{1} and M ↠^{∗} M_{2}, there is a term M_{3} such that M_{1} ↠^{∗} M_{3} and M_{2} ↠^{∗} M_{3} (cf. [Bar84]).

6The subject reduction property says that the reduction relation preserves typing sequents, i.e. if Γ▷M: σ and M ↠^{∗} N, then Γ ▷ N: σ.

Nested let-expressions (let x_{1}=M_{1} in (let x_{2}=M_{2} ⋯ in N)) may be abbreviated as (let x_{1}=M_{1}, x_{2}=M_{2}, … in N).

The identity function λx.x is denoted by id, and for two terms M and N, the composition λx.(M (N x)) is abbreviated as M ∘ N.

1.2.2 Monads and computational effects

Denotational semantics is a powerful tool for describing the meaning of functional programs. What makes this theory even more attractive is that even the programs containing “impure” features, such as jumps or assignment, can be given a purely functional interpretation. For example, in a functional programming language with assignments, programs are interpreted in state passing style, where each function is passed an extra argument representing the state of the mutable store. Likewise, each function returns a pair consisting of its result and a new state of the store. A functional program with non-local jumps, can similarly be interpreted in continuation passing style.

Monads give a framework, due to Moggi [Mog88], that unifies the ideas used in denotational semantics to handle a particular “impure” feature of functional programs. Strictly speaking, a monad (in a category) is a categorical concept, providing the structure needed to give categorical interpretation of functional programs with features like assignment, divergence, exceptions, etc.

Many concepts we use in this paper are motivated by the monadic framework, but rather than giving a detailed exposition of monads in a category, we find it more useful to present the intuitive ideas in a simplified way. For completeness, we summarize the main definitions in the Section 1.9.1. A reader is also referred to [Mog88], [Mog91], and [ML71] for more details.

For simplicity, assume we want to give a denotational interpretation of a programming language in the category of sets, so that programs are interpreted as functions, and types are interpreted as sets.^{7} A monad, T, is defined by a triple (T, η, ^{∗})^{8} where: T is a function mapping sets to sets; for each set A, η_{A} is a function from A to T (A); and for each function f: A → T (B), f^{∗} is a function from T (A) to T (B). Moreover, the components η and ^{∗} of the monad satisfy the following monad laws:

• right identity: η_{A}^{∗} = id_{T (A)},

• left identity: for every f: A → T (B), η_{A}; f^{∗} = f, and

• associativity: for every f: A → T (B), g: B → T (C) and h: C → T (D),

(f; g^{∗}); h^{∗} = f; (g; h^{∗})^{∗},

where id_{T} (A) denotes the identity function on T (A), and f; g is the composition of f followed by g.

7A fully general description could be given by describing a monad in an arbitrary Cartesian closed category, instead of in Set.

8The triple (T, η, ^{∗}) is called Kleisli triple and it uniquely defines a monad (see Section 1.9.1 for more details).

To help understanding how a monad is used in giving a denotational semantics of programs, we first present several examples.

Example 1.2.1. The nondeterministic monad (N, η, ^{∗}) is defined by:

• function N that, to each set A assigns the set P_{fin}(A), the set of all finite subsets of A,

• for each set A, the function η_{A}, assigning the set {a} to each element a of A, and

• for each function f: A → P_{fin}(B), the function f^{∗} is defined by f^{∗}(S) = ⋃_{a∈S} f(a), for each finite S ⊆ A.

This monad can be used to describes nondeterministic computations as follows. A nondeterministic program, takes a value of type A and, in general, returns a set of results of type B (one for each computation path). The interpretation of such a program using the nondeterministic monad is a function from A to P_{fin}(B). If f is a function representing a deterministic program, f; η_{A} represents a nondeterministic program that returns a single value produced by f. Let f: A → P_{fin}(B) and g: B → P_{fin}(C) be meanings of two nondeterministic programs. The meaning of a program obtained by sequencing these two programs is given by the function f; g^{∗}: A → P_{fin}(C).

Example 1.2.2. A continuation monad (K, η, ^{∗}) is defined by:

• function K that, to each set A assigns the set (A^{R})^{R}, where R is a set representing answers,

• for each set A, the function η_{A}, assigning the function λk ∈ A^{R}.k(a) to every element a of A, and

• for each function f: A →(B^{R})^{R}, the function f^{∗} is defined by

f^{∗}(c) = λk ∈ B^{R}.c(λa ∈ A.f(a)(k)),

for each c ∈ (A^{R})^{R}.

In this monad, one can give the continuation passing style interpretation of programs. In CPS semantics, a computation is a function that takes a continuation and returns a result, and a continuation is a function that takes a value and returns a result. Intuitively, a continuation describes the rest of the program. We interpret a program that takes an argument of type A and returns a value of type B as a function from the set A to the set (B^{R})^{R}. An effect-free program is a program that does not contain any “jumps”, so its interpretation is a function form A to (B^{R})^{R}, that computes a value and passes it directly to a continuation. More precisely, if f: A → B is a function describing how the program computes the return value from its argument, the function f; η_{B} = λx ∈ A.λk ∈ B^{R}.k(f(x)) gives the CPS meaning of the program. Similarly, the composition of two programs whose meaning are given by functions f: A →(B^{R})^{R} and g: B →(C^{R})^{R} is given by the function f; g^{∗} = λa ∈ A.λk ∈ C^{R}.f(a)(λb ∈ B.g(b)(k)).

Example 1.2.3. Mutable store can be described by the monad (St, η, ^{∗}) where • function St assigns, to each set A, the set (A × S)^{S}, where S is a set representing the

store (typically, elements of a S are functions from a set of locations to a set of values that can be stored in the sore),

• for each set A, the function η_{A}, assigning the function λs ∈ S.⟨a, s⟩ to every element a of A, and

• for each function f: A →(A × S)^{S}, the function f^{∗} is defined by

f^{∗}(c) = λs ∈ S.(let ⟨a, s′⟩ = c(s) in f(a)(s′)),

for each c ∈ (A × S)^{S}.

A computation is represented by a function that given a state of the store produces a pair consisting of a value, and a new state of the store. Programs, that denote functions that can manipulate the store are interpreted as functions from a set A to the set (B × S)^{S}. The meaning of a program which does not access the store is given by the function f; η_{B} = λa ∈ A.λs ∈ S.⟨f(a), s⟩, where f: A → B describes the functional behavior of the program. The composition of two programs, the meanings of which are given by functions f: A →(B ×S)^{S} and g: B →(C × S)^{S}, is interpreted by the function f; g^{∗} = λa ∈ A.λs ∈ S.(let ⟨b, s′⟩ = f(a)(s) in g(b)(s′)), which says that the first program is evaluated in the current state of the store, followed by the evaluation of the second program in the state of the store that resulted from the evaluation of the first program.

Other examples of monads corresponding to divergence, interactive I/O, exceptions, mutable store, etc. can be found in [Mog88, Mog89, Wad90, Wad95].

To summarize the above examples, we notice that in each of the examples, the components of the monad η and ^{∗} satisfy the monad laws. Secondly, computations were described by the set T (A), where T was either K, N, or St, and the programs were interpreted as functions from a set A to the set of computations T (B). The effect-free programs were interpreted as functions obtained by composing the function η_{B} with a function f: A → B, describing the functional behavior of the program. Finally, programs were composed using the composition f; g^{∗}, where f and g were the meanings of the individual programs.

In the sections that follow, we will concentrate on a general monad, and specifically on the continuation monad, and formalize the above discussed interpretation of programs. For the programming language, we use Moggi’s λ_{cp} calculus. The interpretation will be formalized by several transforms. For instance, we define the computational transform to give an interpretation of λ_{cp} using an unspecified monad, and the CPS transform to give the CPS semantics using the continuation monad. For the metalanguage in which we give interpretation we choose calculi λ_{ml}, λ_{c}, λ_{n∀} and λ_{cp∀} depending on the particular transform that specified the interpretation. Sections 1.2.3, 1.2.4, and 1.2.5 define these calculi.

1.2.3 Computational lambda calculus

Calculus λ_{cp} represents the core of a sequential call-by-value programming language with possible “impure” effects. Even though λ_{cp} does not have any such features as assignment, continuations etc., its logic is sound with respect to models where such effects can be interpreted. Our presentation of λ_{cp} differs slightly form Moggi’s and is in a style more familiar to a computer scientist.^{9} We will define the pure calculus λ_{cp} and its extension, the full computational calculus λ_{c}. Note that while we use λ_{cp} to represent a programming language, we use λ_{c} to formalize the interpretation of λ_{cp} using the modified computational transform defined in section 1.3.2.

The computational calculus, λ_{cp}, is a call-by-value calculus, and therefore we need to distinguish between values and terms. The language of λ_{cp} is defined by the grammar:

values  V ::= x | λx.M
terms  M ::= V | (M M) | (let x=M in M).

Axioms of λ_{cp} are given in Table 1.2. We consider only simply typed term over a base type

((λx.M) V) = M{V/x}  (β_{v})

λx.V x = V , x ∉ FV(V)  (η_{v})

(let x=M in x) = M  (unit)

(let x_{2}=(let x_{1}=M_{1} in M_{2}) in M) = (let x_{1}=M_{1} in (let x_{2}=M_{2} in M)) , x_{1} ∉ FV(M)  (assoc)

(M N) = (let x=M in (x N))  (let.1)

(V M) = (let y=M in (V y))  (let.2)

Table 1.2: Axioms of λ_{cp}.

ı. The λ_{cp} type system is presented in Table 1.3.

The full computational calculus λ_{c} is an extension of λ_{cp} with the term constructors:

values  V ::= ⋯ | [M]
terms  M ::= … | μ(M).

The types of λ_{c} are extended with the unary type constructor T, and rules Types:

9In contrast to [Mog88, Mog91], where λ_{cp} is presented as a calculus with two kinds of predicates, equality and existence, we only consider equality predicates. An existence predicate asserts that a term has a value, meaning that it has no computational effects. We prefer to define values as a syntactic subclass of terms.

The two approaches are equivalent, in the sense that an existence predicate is provable in Moggi’s setting for exactly the same terms that, in our setting, can be shown provably equal to a value. We should also point out, that in our presentation, we omit products, but as shown in Section 1.5.5, all of our results hold if products were included λ_{cp}.

σ ::= ı | σ→σ

Inference Rules:

\frac{Γ ▷_{cp} M: σ→τ, Γ ▷_{cp} N: σ}{Γ ▷_{cp} (M N): τ}  (app)

\frac{Γ, x: σ ▷_{cp} M: τ}{Γ ▷_{cp} λx.M: σ→τ}  (abs)

Γ, x: σ ▷_{cp} x: σ  (var)

\frac{Γ ▷_{cp} M: σ, Γ, x: σ ▷_{cp} N: τ}{Γ ▷_{cp} (let x=M in N): τ}  (let)

Table 1.3: Type inference rules of λ_{cp}.

\frac{Γ ▷_{c} M: σ}{Γ ▷_{c} [M]: T (σ)}  ([·])

and

\frac{Γ ▷_{c} M: T (σ)}{Γ ▷_{c} μ(M): σ}  (μ)

type the new term constructors. The logic of λ_{c} extends the logic of λ_{cp} with the axioms:

μ([M]) = M  (μ.β)

and

[μ(V)] = V.  (μ.η)

The language of λ_{c} is certainly more expressive that λ_{cp}. However, its logic does not prove any new equations between λ_{cp} terms, that is λ_{c} is a conservative extension of λ_{cp}.

Proposition 1.2.4. Let M and N be λ_{cp} terms. Then λ_{c} ⊢ M = N iff λ_{cp} ⊢ M = N.

Proof Sketch: We define the reduction relation in λ_{c}, and show it has the following properties. First the reduction is Church-Rosser, which implies that if λ_{c} ⊢ M = N, then there is a term P such that both M and N reduce to P, and secondly, if M is a λ_{cp} term that reduces to P, then P is also a λ_{cp} term. The reduction relation is defined by “orienting” the λ_{c} axioms from left to right. Then the second property is obvious. To show the Church-Rosser property we consider the reduction relation defined by reductions (μ.β) and (μ.η), and show that it commutes with the let, β_{v} and η_{v} reduction relations as defined in [Mog88].

In this work we do not use the full expressive power of λ_{c}. Using constructors [·] and μ(·), we can define terms

E =^{def} λx.[x] and R =^{def} λx.μ(x),

for which it is provable that

λ_{c} ⊢ R ∘ E = id.  (r-e)

In all of our proofs, we only use terms E and R, and equality (r-e), without any other reference to constructors [·] and μ(·). Thus when we consider λ_{c} we are really referring to λ_{cp} extended with terms E and R satisfying equation (r-e) and typable with appropriate types. Namely for any type σ we assume sequents Γ ▷_{c} E: σ→T (σ) and Γ ▷_{c} R: T (σ)→σ are derivable. As a consequence, our reasoning carries over if we replace E and R with any terms having the above mentioned abstract properties.

Intuitively, we think of functions E and R in a context of a particular monad. Namely, given a value denoted by V of type σ, E(V) denotes the trivial computation of the meaning of V which has the type T (σ). On the other hand, given a computation m, denoted by M, of type T (σ), R(M) denotes the result of the evaluation of m.

For example, when defining the modified CPS transform (see section 1.3.2), we define terms E^{K} and R^{K} to be

E^{K} =^{def} λxk.k x and R^{K} =^{def} λx.x id.

For a value v, denoted by V, E^{K}(V) denotes a trivial computation of v that, given a continuation, passes v to the continuation. If M denotes a computation m, R^{K}(M) denotes the result of evaluating m by passing it a “top-level” continuation id. It is easy to see that λ_{cp} ⊢ R^{K} ∘ E^{K} = id, so the reasoning in λ_{c}, using abstract properties of E and R, applies when we replace E and R with terms E^{K} and R^{K}.

Even though let-expressions are elementary constructs in λ_{c}, it is sometimes convenient to treat them as syntactic sugar. The following two lemmas justifies doing so. First we show that a let-expression is provably equivalent to its de-sugared from.

Lemma 1.2.5. (let x=M in N) = ((λx.N) M).

Proof: By (β_{v}) and (let.2) we have,

(let x=M in N) = (let x=M in ((λx.N) x)) = ((λx.N) M).

The next lemma is necessary to justify omitting the (let) case form the proofs by induction on the type derivation in λ_{c}. Let M and M′ be λ_{c} terms such that M′ is obtained from M by de-sugaring all let’s in M, that is, by replacing every subterm (let x=P in Q) in M with ((λx.Q) P). Then the lemma implies that M is typable with σ from hypothesis Γ using type inference rules of λ_{c}, if and only if M′ is typable with σ from Γ without using the (let) typing rule.

Lemma 1.2.6. Assume M and N do not contain any let-expressions. Then, sequent Γ ▷_{c} (let x=M in N): σ is derivable in λ_{c} if and only if sequent Γ ▷_{c} ((λx.N) M): σ is derivable in λ_{c}, but without using the (let) rule.

Proof Sketch: To show one direction, show that from the antecedents of the (let) rule, which must be the last rule in the derivation of Γ ▷_{c} (let x=M in N): σ, one can derive Γ ▷_{c} ((λx.N) M): σ using (abs) and (app) rules. The other direction is proved similarly.

An equivalent set of axioms for the logic of λ_{c} can be defined using the notion of an evaluation context.

Definition 1.2.7. An evaluation context is a λ_{c} context defined by the following grammar:

E⟨[·]⟩ ::= ⟨[·]⟩ | (V E⟨[·]⟩) | (E⟨[·]⟩ M) | (let x=E⟨[·]⟩ in M) | (let x=V in E⟨[·]⟩),

where V ranges over values, and M ranges over terms.

Intuitively, the evaluation context specifies the order of evaluation. Using the evaluation context, Sabry and Felleisen [SF93] have formulated a set of axioms, equivalent to axioms of λ_{c}, which are sometimes more convenient to use in proving λ_{c} identities. In their formulation, they use the following equation schema:

((λx.E⟨[x]⟩) M) = E⟨[M]⟩,  x ∉ FV(E⟨[·]⟩).  (β_{sf})

Lemma 1.2.8 (Sabry-Felleisen). Every instance of the above schema is provable in λ_{c}.

In most of our results we prove equations by convertibility and to simplify the proofs we will refer to equations in Table 1.4. Since λ_{c} is conservative over λ_{cp}, all of the equalities are provable in λ_{cp} as well. In all of the equations, we assume M, N, P, and Q are arbitrary λ_{c} terms, and V and W denote λ_{c} values. The equations in Table 1.4 all follow easily from λ_{cp} axioms, or using equation (β_{sf}). For illustration we show how (C-assoc) is proved. Note that (C-assoc) is not provable in λ_{v}.

Lemma 1.2.9. In λ_{c}, composition is associative. Namely, for any values U, V and W

((U ∘ V) ∘ W) = (U ∘ (V ∘ W)).

Proof:

((U ∘ V) ∘ W) = λx.((U ∘ V) (W x))  by defn.
= λx.((λy.(U (V y))) (W x))  by defn.
= λx.(let y=(W x) in (U (V y)))  by (let.2) and (β_{v})
= λx.(let y=(W x) in (let z=(V y) in (U z))) by (let.2)
= λx.(let z=(let y=(W x) in (V y)) in (U z)) by (assoc)
= λx.(U (let y=(W x) in (V y)))  by (let.2)
= λx.(U (V (W x)))  by (let.2)
= λx.(U ((λy.(V (W y))) x))  by (β_{v})
= λx.U ((V ∘ W) x)  by defn.
= (U ∘ (V ∘ W))  by defn.

(id M) = M  (C-id)

\frac{V ∘ W = id}{(V (W M)) = M}  (C-id.1)

((U ∘ V) ∘ W) = (U ∘ (V ∘ W))  (C-assoc)

(V ∘ id) = (id ∘ V) = V  (C-unit)

(V (let x=M in N)) = (let x=M in (V N)),  x ∉ FV(V)  (C-appl.1)

(let x=V in M) = M{V/x}  (C-let.1)

((let x=P in V) (let y=Q in W)) = (let x=P in (let y=Q in (V W))) (C-appl.2)

((λx.x M) N) = (N M),  x ∉ FV(M)  (C-appl.3)

Table 1.4: Identities provable in λ_{c}

1.2.4 Monadic metalanguage

As a formalization of a metalanguage in which a denotational semantics of λ_{cp} can be defined, we introduce λ_{ml} calculus. We remark that λ_{ml} is what Moggi [Mog91] calls a “monadic metalanguage”, but our presentation is more in tune with a functional programming point of view. We define the calculus λ_{ml} to be an extension of the simply typed βη-calculus, λ_{n}, with a set of constructs corresponding to an arbitrary monad.

The language of λ_{ml} consists of the following terms:

M ::= x | (M M) | λx.M | [M]_{T} | (let_{T} x⇐M in M).

Note that above term constructs are different from constructs [·] and let used in λ_{c}. The types of λ_{ml} are simple types over a base type ı, extended with types of the form T (σ) where T is a unary type constructor, and the type inference rules are added for typing [·]_{T} and let_{T} expressions. The type system is given in Table 1.5.

In addition to (β) and (η) axioms, the logic of λ_{ml} contains the additional axioms that correspond to monad laws. The axioms are given in Table 1.6 below.

Types:

σ ::= ı | σ→σ | T (σ)

Inference Rules:

Γ, x: σ ▷_{ml} x: σ  (var)

\frac{Γ ▷_{ml} M: σ→τ, Γ ▷_{ml} N: σ}{Γ ▷_{ml} (M N): τ} (app)

\frac{Γ, x: σ ▷_{ml} M: τ}{Γ ▷_{ml} λx.M: σ→τ}  (abs)

\frac{Γ ▷_{ml} M: T (σ), Γ, x: σ ▷_{ml} N: T (τ)}{Γ ▷_{ml} (let_{T} x⇐M in N): T (τ)} (let)

\frac{Γ ▷_{ml} M: σ}{Γ ▷_{ml} [M]_{T}: T (σ)}  (unit)

Table 1.5: Type system of λ_{ml}.

1.2.5 Calculi λ_{n}, λ_{n∀}, λ_{cp∀}, etc.

Calculus λ_{n} is intended to capture call-by-name evaluation in programming languages. The language of λ_{n} is defined by the grammar

M ::= x | λx.M | (M M),

and its axioms are

((λx.M) N) = M{N/x}  (β)

and

λx.Mx = M , x ∉ FV(M).  (η)

In λ_{n}, We consider only simply typed terms over a base type ı. The type system is described in Table 1.7.

In order to define a typed CPS transform we need to extend λ_{n} with polymorphic types. Let λ_{n∀} denote this extension. The types of λ_{n∀} are extended with type variables and universal types. Namely we have

σ ::= ı | t | σ→σ | ∀t.σ.

We will use letters s and t to range over type variables. The type inference rules, in addition to those of λ_{n}, are given in Table 1.8 below. In λ_{n∀}, it is possible to define constructors

((λx.M) N) = M{N/x}  (β)

λx.Mx = M , x ∉ FV(M)  (η)

(let_{T} x⇐M in [x]_{T}) = M  (R-unit)

(let_{T} x⇐[M]_{T} in N) = N{M/x}  (L-unit)

(let_{T} x_{2}⇐(let_{T} x_{1}⇐M_{1} in M_{2}) in M) = (let_{T} x_{1}⇐M_{1} in (let_{T} x_{2}⇐M_{2} in M)) , x_{1} ∉ FV(M)  (assoc)

Table 1.6: Axioms of λ_{ml}.

corresponding to a continuation monad. Let us define

K(σ) =^{def} ∀s.(σ→s)→s
[M]_{K} =^{def} λk.k M
(let_{K} x⇐M in N) =^{def} λk.(M (λx.(N k)))

Note that K, [·]_{K}, and let_{K} is to be understood as abbreviation for the corresponding terms on the right-hand side.

One can give an intuitive interpretation for the above constructs, similar to the intuitive explanation of the continuation monad given in section 1.2.2. A computation in a continuation monad is a function that takes a continuation and returns a result. A continuation represents the rest of the program, and can be described as a function that maps values to results. Therefore, if m is a value denoted by M, the trivial computation of m will take a continuation and pass m to it. Hence the definition of [M]_{K} = λk.k M. If N denotes a computation, and k is (bound to) a continuation, λx.(N k) denotes a new continuation that, given a value bound to x, returns a result of computing N with continuation k. Computations denoted by M and N can thus be composed by passing the continuation λx.(N k) to M as done in the definition of (let_{K} x⇐M in N).

To determine a type of a computation of values of type σ, let s denote the type of results. Then a continuation must be of type σ→s and a computation will have type (σ→s)→s. Many authors, e.g. [MW85, Wad90, Mog91, HL92, HD94], define the type of results to be a fixed (observable) type o. We believe this is not general enough for our purposes. Instead we define the type of computations to be K(σ) = ∀s.(σ→s)→s as above. The reason for defining the type of computations in this way is that we want to show that type σ is a retract of type K(σ) (see definition 1.4.1). With our definition of K(σ), the functions E^{K} and R^{K}, defined in Section 1.2.3, provide the desired retraction-embedding pair. On the other hand, Types:

σ ::= ı | σ→σ

Inference rules:

Γ, x: σ ▷_{n} x: σ  (var)

\frac{Γ ▷_{n} M: σ→τ, Γ ▷_{n} N: τ}{Γ ▷_{n} (M N): τ}  (app)

\frac{Γ, x: σ ▷_{n} M: τ}{Γ ▷_{n} λx.M: σ→τ}  (abs)

Table 1.7: Type system of simple types for λ_{n}.

Types:

σ ::= ⋯ | t | ∀t.σ

Inference rules:

\frac{Γ ▷_{∀} M: σ}{Γ ▷_{∀} M: ∀t.σ} ,  if x is not free in Γ  (gen)

\frac{Γ ▷_{∀} M: ∀t.σ}{Γ ▷_{∀} M: σ\{τ/t\}}  (inst)

Table 1.8: Polymorphic extension of a type system.

to define a retraction-embedding pair from σ to the type (σ→o)→o, one would require that each type σ is a retract of the type of answers o. It is also possible to give a proper typing for the functions E^{K} and R^{K} using recursive types, but we prefer the polymorphic solution. note that we don’t really use the full power of polymorphism, since the only polymorphic types occur in the form ∀s.(σ→s)→s, where s is not free in σ.

To restrict the codomain of the CPS transform to a call-by-value language, we also define the calculus λ_{cp∀}, to be an extension of λ_{cp} with polymorphic types.

In addition to polymorphic extension, we will also consider an extension of the type system of a calculus with products. This extension is discussed in Section 1.9.2.

1.3 Source to Source Transforms

A source-to-source transform is simply a function mapping terms of one calculus to terms of another calculus. Since we work in typed lambda calculi, instead of mapping terms to terms, we study transforms that map typing sequents of one calculus to typing sequents of another calculus. However, we will often leave the typing implicit.

Even though, the languages of some of the calculi we study coincide, we will be precise in specifying the calculus of the domain and the calculus of the codomain of each of the transforms.

We study transforms which give slightly different interpretations of λ_{cp} in λ_{ml}, λ_{c} and λ_{cp∀}. The main characteristic of these transforms is that they make the computational structure of the λ_{cp} terms explicit. For example, the CPS transform describes the computational structure of a term in terms of continuations which explicitly appear in the transformed term.

We study, the computational transform form λ_{cp} to λ_{ml} and its modification that maps λ_{cp} into λ_{c}. We also study the CPS transform and its modified counterpart as transforms form λ_{cp} into λ_{cp∀}.

1.3.1 The computational transform

The computational transform, T_{ml}, is a generalization of the CPS transform in which the notion of computations is generalized from continuation passing to an arbitrary one. Intuitively, the computational transform gives a functional interpretation of call-by-value programs with possible “impure” effects, in the calculus λ_{ml}. The computational transform was first presented in [Wad90] as an interpretation of programs by means of list comprehension. Wadler defines both, call-by-value and call-by-name variants of the transform. The same transform also appears in [Mog91] as the ^{∘} translation connecting the “computational programming language” (i.e. λ_{c}) and the “monadic metalanguage” (i.e. λ_{ml}).^{10} Furthermore, in [HD94], call-by-value and call-by-name variants of the computational transform appear as call-by-value and call-by-name encodings of programs in Moggi’s monadic metalanguage. Hatcliff and Danvy use the transform to characterize the essential part of the CPS transform, thus breaking the CPS transform into a composition of the generic encoding, given by the transform T_{ml}, and, what they call, the “continuation introduction”.

\overline{\overline{x}} =^{def} [x]_{T}
\overline{\overline{λx.M}} =^{def} [λx.\overline{\overline{M}}]_{T}
\overline{\overline{(M N)}} =^{def} (let_{T} x⇐\overline{\overline{M}} in (let_{T} y⇐\overline{\overline{N}} in (x y)))
\overline{\overline{(let x=M in N)}} =^{def} (let_{T} x⇐\overline{\overline{M}} in \overline{\overline{N}})

ı′ =^{def} ı_{(σ→τ)′ =^{def} σ′→T (τ′)} {x_{i}: σ_{i}}′ =^{def} {x_{i}: σ′_{i}}

\overline{\overline{Γ ▷_{cp} M: σ}} =^{def} Γ′ ▷_{ml} \overline{\overline{M}}: T (σ′)

Table 1.9: The computational transform T_{ml}.

10In [Mog91], the ^{∘} translation is defined only for his “simple language”, which has no lambda abstractions.

We concentrate on the call-by-value variant of the computational transform as a transform mapping typing sequents of λ_{cp} into typing sequents of λ_{ml}. The definition of the transform is given in Table 1.9. In order to show that the transform is well defined, we need to show that it maps derivable typing sequents to derivable typing sequents.

Proposition 1.3.1. If Γ ▷_{cp} M: σ then Γ′ ▷_{ml} \overline{\overline{M}}: T (σ′).

Proof: Easy by induction on the derivation of Γ ▷_{cp} M: σ.

Another aspect of the correctness of the computational transform is the equational correspondence result, which says that the transform preserves equality in λ_{cp}, and moreover, nothing, up to λ_{cp}-equivalence, is lost in the transform.

Theorem 1.3.2 (Sabry-Wadler). λ_{cp} ⊢ M = N iff λ_{ml} ⊢ \overline{\overline{M}} = \overline{\overline{N}}.

We point the reader to [HD94] and [SW96] for more detailed analysis of the transform T_{ml}.

1.3.2 The modified computational transform

In an effort to define a transform, similar to the CT, but mapping λ_{cp} into a call-by-value calculus, we define the modified computational transform, T_{ml♯}, to be a transform from λ_{cp} into λ_{c}. The transform T_{ml♯}, is defined by composing the computational transform T_{ml} with the transform T_{♯} defined in Table 1.10. It is easy to see that the transform T_{♯} is well defined. Namely,

Proposition 1.3.3. If Γ ▷_{ml} M: σ then Γ ▷_{c} M^{♯}: σ.

x^{♯} =^{def} x
(λx.M)^{♯} =^{def} λx.M^{♯}
(M N)^{♯} =^{def} (M^{♯} N^{♯})
[M]_{T}^{♯} =^{def} E(M^{♯})
(let_{T} x⇐M in N)^{♯} =^{def} (let x=R(M^{♯}) in N^{♯})

(Γ ▷_{ml} M: σ)^{♯} =^{def} Γ ▷_{c} M^{♯}: σ
Table 1.10: Transform T_{♯} from λ_{ml} to λ_{c}.

In the previous section, we have seen that the transform T_{ml} preserves λ_{cp}-equivalence. However, transform T_{♯}, does not preserve this result for all terms. We will, however, show that the equational correspondence result holds for the transform T_{ml♯}, if we restrict our attention to pure closed terms.

To compare the transforms T_{ml} and T_{ml♯}, we examine their effect on let-expressions. By definition we have:

\overline{\overline{(let x=M in N)}} = (let x⇐\overline{\overline{M}} in \overline{\overline{N}}),

and

\overline{\overline{(let x=M in N)}}^{♯} = (let x=R(\overline{\overline{M}}^{♯}) in \overline{\overline{N}}^{♯}).

To see the difference, observe that the terms (let_{T} x⇐M in N) and (let x=R(M) in N), have similar, but different meanings. The difference is that if the computation denoted by M has any computational effects, they may be discarded by the function R. For example, if M changed the store, the changes would not be seen in the evaluation of N. In the second terms, however, any possible effects in evaluation of M, will affect the evaluation of N. Therefore, if M changes the store, N will be evaluated in the changed store.

Not surprisingly, the equational correspondence result for T_{ml♯} fails for some terms. In particular we have

λ_{cp} ⊢ (let x=M in x) = M,

but

λ_{c} ⊢ \overline{\overline{(let x=M in x)}}^{♯} = E(R(\overline{\overline{M}}^{♯})),

and, in general, E(R(\overline{\overline{M}}^{♯})) ≠ \overline{\overline{M}}^{♯} unless \overline{\overline{M}}^{♯} denotes an effect-free computation. How-

ever, if M is a pure closed term one has that \overline{\overline{M}}^{♯} denotes an effect-free computation, and E(R(\overline{\overline{M}}^{♯})) = \overline{\overline{M}}^{♯}. We state this, somewhat informally, in the following lemma.

Lemma 1.3.4. Let ρ be a substitution mapping variables to “proper” terms. Then for any term M such that Γ ▷_{cp} M: σ,

λ_{c} ⊢ ρ \overline{\overline{M}}^{♯} = E(R(ρ \overline{\overline{M}}^{♯})).

Proof Sketch: While it is possible to define “proper” terms and prove the above lemma in its own right, the lemma also follows as a corollary of Lemma 1.5.10, provided the “proper” terms are defined as in the hypothesis of the same lemma.

From the above lemma, we can conclude that, for the pure closed terms, T_{ml♯} preserves λ_{cp}-equivalence, and combined with the Retraction Theorem, we obtain the following equational correspondence result.

Theorem 1.3.5. Let M and N be closed λ_{cp} terms such that ▷_{cp}M: σ and ▷_{cp}N: σ. Then,

λ_{cp} ⊢ M = N iff λ_{c} ⊢ \overline{\overline{M}}^{♯} = \overline{\overline{N}}^{♯}.

Proof Sketch: Assume λ_{cp} ⊢ M = N. We need to show that T_{ml♯} preserves all axioms of λ_{cp}. The only questionable axiom is (unit), so let us assume that M = (let x=N in x).

By the previous lemma, \overline{\overline{N}}^{♯} = E(R(\overline{\overline{N}}^{♯})) = \overline{\overline{(let x=N in x)}}^{♯} as desired.

The other implication in the theorem follows from the Retraction Theorem (Theorem 1.5.11).

1.3.3 The CPS transform

The Fischer-Reynolds [Fis72, Fis93, Rey72] continuation-passing style transform comes in several variations: call-by-name, call-by-value, left-to-right and right-to-left. We focus on a call-by-value variant based on the one defined by Plotkin [Plo75]. The definition is given in Table 1.11.

\overline{x} =^{def} λk.k x
\overline{(λx.M)} =^{def} λk.k λx.\overline{M}
\overline{(M N)} =^{def} λk.\overline{M} (λm.\overline{N} (λn.m n k))
\overline{(let x=M in N)} =^{def} λk.\overline{M} (λx.\overline{N} k)

K(σ) =^{def} (σ→σ)→σ
ı′ =^{def} ı
(σ→τ)′ =^{def} σ′→K(τ′)

{x_{i}: σ_{i}}′ =^{def} {x_{i}: σ′_{i}}
\overline{Γ ▷_{cp} M: σ} =^{def} Γ′ ▷_{n} \overline{M}: K(σ)

Table 1.11: The CPS transform.

A typed versions of the CPS transform has first been studied by Meyer and Wand [MW85] for the simple types, and later by Harper and Lillibridge [HL92] in a polymorphic setting. Our definition differs from the one in this and some other work (e.g. [Mog88, HD94]) in the definition of the type of computations. As discussed in Section 1.2.5, the type of computations, K(σ) is defined to be ∀s.(σ→s)→s instead of the more traditional (σ→o)→o, where o denotes a fixed type of answers. The following proposition asserts that the CPS transform is well defined on typing sequents.

Proposition 1.3.6. If Γ ▷_{cp} M: σ then Γ′ ▷_{cp∀} \overline{M}: K(σ′).

As for the computational transform, the equational correspondence result holds for the CPS transform as well (see Theorem 1.1.2). In fact, this result is a corollary of the equational correspondence theorem for the computational transform (Theorem 1.3.2), when the CPS transform is viewed as a special case of the transform T_{ml} as discussed below.

One can define the CPS transform as a special case of the computational transform by considering the definition of the computational transform as a template, and using the terms corresponding to continuation monad K instead of the terms corresponding to a general monad T in λ_{ml}. Recall the definition of K, [M]_{K} and (let_{K} x⇐M in N) given in section 1.2.5. Substituting K, [M]_{K} and (let_{K} x⇐M in N) for T, [M]_{T} and (let_{T} x⇐M in N) in the definition of T_{ml}, we obtain the CPS transform. For example,

\overline{(M N)} = (let_{K} m⇐\overline{M} in (let_{K} n⇐\overline{N} in (m n)))
= λk.\overline{M} (λm.((λk.\overline{N} (λn.(m n) k)) k))
= λk.\overline{M} (λm.\overline{N} (λn.m n k)).

Another interesting property of the CPS terms is that they behave the same way under the call-by-name and call-by-value evaluation strategies. This indifference result was used by Plotkin to simulate call-by-value programs with a call-by-name evaluator. Equationally, this means that the call-by-name equational logic is conservative over the call-by-value logic when restricted to the range of the CPS transform (see Theorem 1.1.5). Because of this indifference result, without loss of generality, we can restrict the logic of the codomain of the CPS transform to the logic of λ_{cp}. Because of our definition of the types of computations K(σ), the codomain of the CPS transform requires polymorphic types. Therefore we view the CPS transform as a transform from λ_{cp} to λ_{cp∀}.

1.3.4 The modified CPS transform

Analogous to the modified computational transform we can define the modified CPS transform. We do so by using the terms E^{K} and R^{K} defined in Section 1.2.3 instead of the terms E and R in the definition of the transform T_{♯}, thus obtaining the transform T_{♯}^{K} mapping λ_{n∀} to λ_{cp∀}. Composing the CPS transform with the transform T_{♯}^{K}, we get the modified CPS transform from λ_{cp} to λ_{cp∀}. The complete definition of the modified CPS transform is given in the Table 1.12 below. By the axioms of λ_{cp}, we have that R^{K} ∘ E^{K} = id, and since

\overline{x}^{♯} =^{def} (E^{K} x)
\overline{(λx.M)}^{♯} =^{def} (E^{K} λx.\overline{M}^{♯})
\overline{(M N)}^{♯} =^{def} ((R^{K} \overline{M}^{♯}) (R^{K} \overline{N}^{♯}))
\overline{(let x=M in N)}^{♯} =^{def} (let x=(R^{K} \overline{M}^{♯}) in \overline{N}^{♯})

E^{K} =^{def} λxk.k x_{R^{K} =^{def} λx.x (λz.z)}

K(σ) =^{def} ∀t.(σ→t)→t
ı′ =^{def} ı
(σ→τ)′ =^{def} σ′→K(τ′)

{x_{i}: σ_{i}}′ =^{def} {x_{i}: σ′_{i}}
\overline{Γ ▷_{cp} M: σ}^{♯} =^{def} Γ′ ▷_{cp} \overline{M}^{♯}: K(σ′)

Table 1.12: The modified CPS transform.

this is the only property of the terms E and R we used in reasoning about the modified computational transform, the results of Section 1.3.2 apply to the modified CPS transform as well.

1.4 Retractions

In this section we will show that each type σ is a retract of the type T (σ′), and also that σ is a retract of the type K(σ′). In a lambda calculus, we have the following definition of a retract:

Definition 1.4.1 ([MW85]). Let λ be a lambda calculus. A λ type σ is a retract of a λ type τ, if there are closed λ terms E_{σ,τ} (called embedding) and R_{σ,τ} (called retraction), such that ▷E_{σ,τ}: σ→τ, ▷R_{σ,τ}: τ→σ, and λ ⊢ R_{σ,τ} ∘ E_{σ,τ} = id.

In particular we want to show there is a retraction-embedding pair (R, E) such that R is a definable (in λ_{c}) inverse of the modified computational transform. Similarly, we want to find a retraction-embedding pair (R^{K}, E^{K}) such that R^{K} is a definable (in λ_{cp∀}) inverse of the CPS transform. Therefore we need to show that any λ_{cp} type σ is a retract of the type T (σ′), and also that σ is a retract of the type K(σ′).

Recall that in Section 1.2.3, we have defined the terms E: σ→T (σ) and R: T (σ)→σ and showed that λ_{c} ⊢ R ∘ E = id. Therefore, it follows immediately that any λ_{c} type σ is a retract of the type T (σ).

It remains to show that each type σ is a retract of σ′. To do so we define the functions i_{σ}: σ→σ′ and j_{σ}: σ′→σ inductively on the structure of σ:

i_{ı} =^{def} id
i_{σ→τ} =^{def} λf.E ∘ i_{τ} ∘ f ∘ j_{σ}

j_{ı} =^{def} id
j_{σ→τ} =^{def} λg.j_{τ} ∘ R ∘ g ∘ i_{σ}

It is easy to show that functions j_{σ} and i_{σ} indeed form retraction-embedding pairs.

Lemma 1.4.2. For all σ, λ_{c} ⊢ j_{σ} ∘ i_{σ} = id.

Proof: For σ = ı the lemma follows trivially. For higher order types we have

((j_{σ→τ} ∘ i_{σ→τ}) x) = (j_{σ→τ} (i_{σ→τ} x))
= ((λg.j_{τ} ∘ R ∘ g ∘ i_{σ}) ((λf.E ∘ i_{τ} ∘ f ∘ j_{σ}) x)) by definitions
= j_{τ} ∘ R ∘ (E ∘ i_{τ} ∘ x ∘ j_{σ}) ∘ i_{σ}  by (β_{v})
= x  by lemma 1.2.9, (r-e),

and induction hypothesis

Now define E_{σ,T (σ′)} = E ∘ i_{σ} and R_{σ,T (σ′)} = j_{σ} ∘ R, and from the above lemma, it follows that σ is a retract of T (σ′). Moreover, in the next section we will show that R_{σ,T (σ′)} is the inverse of the modified computational transform at type σ, that is

λ_{c} ⊢ (R_{σ,T (σ)} \overline{\overline{M}}^{♯}) = M

for closed M of type σ.

To obtain the retraction-embedding pair showing that σ is a retract of K(σ′) we simply use E^{K} = λxk.k x and R^{K} = λx.x id instead of E and R in all the definitions above. It is immediate that the resulting functions, name them R^{K} and E^{K}, are a retractionembedding pair, since in the proof of Lemma 1.4.2 we only used axioms of λ_{cp} and the equation R ∘ E = id, and we have seen that λ_{cp} ⊢ R^{K} ∘ E^{K} = id. In the next section we will also show that R^{K} is a definable inverse of the modified CPS transform, as well as an inverse of the original CPS transform.

Remark. We have defined different pairs of functions i_{σ} and j_{σ}, for each type σ. However, when clear from context, we may omit writing the subscripts, keeping in mind that i (as well as j) may denote a different function depending on the particular context in which it is used. We should also point out, that whenever we talk about the modified computational transform, we refer to definitions of i and j using functions E and R, and when we talk about the CPS transform, we will use the same notation to denote functions i and j defined using terms E^{K} and R^{K} instead.

1.5 The Retraction Theorem

The main result of this work is a stronger version of the Meyer-Wand Retraction Theorem. First we prove the Retraction Theorem for the modified computational transform (Theorem 1.5.11). We use the proof of this theorem as a template to prove the Retraction Theorem for particular transforms of interest, namely for the original CPS transform (Theorem 1.5.18), and for the state passing style transform (Theorem 1.5.19).

In our version, the conclusion of these theorems holds by convertibility in λ_{c}, λ_{cp∀}, and λ_{cp×} respectively. Therefore, throughout this section, unless specified otherwise, whenever we write M = N, when considering the modified computational transform we assume the equality is provable in λ_{c}, when discussing the results for the CPS transform, we assume the equality is provable in λ_{cp∀}, and when considering the state passing style transform we assume provability in λ_{cp×}.

1.5.1 Interpretation of terms and types

To prove the Retraction Theorem, as discussed in the introduction, we define a framework similar to Mitchell’s type inference model. We define interpretations of terms and types, as well as, a notion of validity of typing sequents with respect to these interpretations.

The key elements needed in the proof of the Retraction Theorem can be summarized as follows. For each of the transforms, T_{ml♯}, T_{cps}, etc., we define: type sets, interpretation of types as type sets, interpretation of terms using the transform, an ε-relation between meanings of terms and types, and a notion of pseudo-application for the terms in the codomain of the transform.

In this section we give the definitions suitable for the modified computational transform, but explain how to define analogous concepts for other transforms. By examining the differences in the definitions, we observe that the following conditions need to be re-proved for each of the transforms. Let App(M, N) denote the pseudo-application, and let ⟦σ⟧ be the meaning of σ. Then for all terms M and N in the codomain of the transform we require, that if M ε ⟦σ→τ⟧ and N ε ⟦σ⟧, then

App(M, N) ε ⟦τ⟧  (†)

j_{τ}(R(App(M, N))) = (j_{σ→τ}(R(M)) j_{σ}(R(N))).  (‡)

We now define these key concepts for the modified computational transform and show that above conditions are satisfied.

Definition 1.5.1. Let ρ be a substitution. For each of the transforms, T_{ml♯}, T_{cps♯} and T_{cps}, we define an interpretation of a term M, relative to a particular transform, to be:

T_{ml♯}⟦M⟧ρ =^{def} ρ \overline{\overline{M}}^{♯}
T_{cps♯}⟦M⟧ρ =^{def} ρ \overline{M}^{♯}
T_{cps}⟦M⟧ρ =^{def} ρ \overline{M}

When the transform used is clear from the context, we will simply write ⟦M⟧ρ.

Types are interpreted as certain sets of terms, the so called type sets.

Definition 1.5.2. Let D denote the set {M | M = E(V) for some value V }. A type set is any subset of D.

Remark. We understand the above definition as parameterized by the term E, so, for example, when we speak about the CPS transform, we will use term E^{K} instead.

Definition 1.5.3. Let M be a term and let S be a type set. Write M ε S iff there is a term E(V) in S such that

M = (let x_{1}=P_{1}, …, x_{k}=P_{k} in E(V)),

where x_{1}, …, x_{k} is the sequence containing of all free variables in V, and P_{i} are arbitrary terms.

Remark. For simplicity, when M ε S, we will assume that M = (let x=P in I(V)) and that x is the only free variable in V.

The intuition behind the ε-relation is to extend the membership relation. In other words, M is ε-related to a set S, if a “value” of M is a member of S (note that a “value” of M may not be unique). A “value” represents, for our purposes, important part of a term. The definition of ε-relation will be different for each transform, based on the structure of the transformed terms.

Definition 1.5.4. The interpretation of type σ is a type set defined by induction on the structure of σ as follows:

• ⟦ı⟧ is the set of all terms of the form E(V) for some value V,

• ⟦σ→τ⟧ is a set of all terms E(V) such that for all E(W) ∈ ⟦σ⟧,

(V W) ε ⟦τ⟧  (P.1)

j_{τ}(R(V W)) = (j_{σ→τ}(V) j_{σ}(W)).  (P.2)

Remark. The preceding definition of the interpretation of types uses terms E and R, as well as the ε-relation. As in the definition of type sets, we will treat terms E and R, as well as the relation ε, as parameters, and when discussing, for example, the CPS transform, we will assume terms E^{K} and J^{K}, and relation ε^{K} were used instead.

In general, the pseudo-application, App, in the codomain of a particular transform, T , will be defined so that

T (M N) = App(T (M), T (N)).

In particular, from the definition of T_{ml♯}, we know that

\overline{\overline{(M N)}}^{♯} = (R(\overline{\overline{M}}^{♯}) R(\overline{\overline{N}}^{♯})),

and for arbitrary terms in the codomain of T_{ml♯}, we have the following definition.

Definition 1.5.5. The pseudo-application in the codomain of T_{ml♯} is defined to be:

App(M, N) =^{def} (R(M) R(N)).

Definition 1.5.4 is motivated by the two conditions, (†) and (‡), which we now prove in lemmas 1.5.6 and 1.5.7 below. The property (P.1) ensures (†) holds, i.e., that type sets ⟦σ⟧ are “closed” under App. Namely we have,

Lemma 1.5.6. For any two terms M and N,

M ε ⟦σ→τ⟧ and N ε ⟦σ⟧ implies App(M, N) ε ⟦τ⟧.

Proof: Since M ε ⟦σ→τ⟧ and N ε ⟦σ⟧, for some E(V) ∈ ⟦σ→τ⟧ and E(W) ∈ ⟦σ⟧, M = (let x=P in E(V)) and N = (let y=Q in E(W)). Therefore,

App(M, N) = (R(M) R(N))  by defn.
= (R(let x=P in E(V)) R(let y=Q in E(W)))  by assumption
= ((let x=P in R(E(V))) (let y=Q in R(E(W)))) by (C-appl.1)
= ((let x=P in V) (let y=Q in W))  by (r-e)
= (let x=P in (let y=Q in (V W)))  by (C-appl.2)
= (let x=P in (let y=Q in (let z=R in E(U)))) by (P.1)

where E(U) ∈ ⟦τ⟧ as desired.

The property (P.2) ensures that (‡) holds, that is, on “proper” terms, j ∘ R is a homomorphism with respect to pseudo-application in the codomain of T_{ml♯} and the application in the domain of T_{ml♯}.

Lemma 1.5.7. Assume M ε ⟦σ→τ⟧ and N ε ⟦σ⟧. Then,

j_{τ}(R(App(M, N))) = (j_{σ→τ}(R(M)) j_{σ}(R(N))).

Proof: Since M ε ⟦σ→τ⟧ and N ε ⟦σ⟧, for some E(V) ∈ ⟦σ→τ⟧ and E(W) ∈ ⟦σ⟧, M = (let x=P in E(V)) and N = (let y=Q in E(W)). Therefore,

j(R(App(M, N))) = j(R(R(M) R(N)))  by defn.
= j(R(let x=P in (let y=Q in (V W))))  as in Lemma 1.5.6
= (let x=P in (let y=Q in j(R(V W))))  by (C-appl.1)
= (let x=P in (let y=Q in (j(V) j(W))))  by (P.2)
= ((let x=P in j(V)) (let y=Q in j(W)))  by (C-appl.2)
= ((let x=P in j(R(E(V)))) (let y=Q in j(R(E(W))))) by (r-e)
= (j(R(let x=P in E(V))) j(R(let y=Q in E(W))))  by (C-appl.1)
= (j(R(M)) j(R(N)))  by assumption.

Note that we used the fact that j(V) and j(W) are values, which follows directly from the definition of j’s.

Our goal is to prove validity of derivable typing sequents. To do so we define notions of truth and validity as follows.

Definition 1.5.8. Given a substitution ρ, a type assertion M: σ is true if ⟦M⟧ρ ε ⟦σ⟧; M: σ is valid if it is true for every substitution; and ρ is said to satisfy a typing hypothesis Γ, if every type assertion in Γ is true with respect to ρ. Finally, a typing sequent Γ ▷ M: σ is valid if M: σ is true for every substitution that satisfies Γ.

Remark. As with the other definitions of this section, we understand the definition of validity as parameterized by the ε-relation, and when speaking about other transforms, we assume the notion of validity is defined with respect to appropriate version of the ε-relation.

1.5.2 The Retraction Theorem for the modified computational transform

The main result of this paper, the Retraction Theorem, is a direct corollary of the Soundness Lemma below. The lemma says that every derivable typing sequent is valid. Moreover, the lemma includes an additional assumption, (S.2), which is the statement of the Retraction Theorem generalized to open terms. The structure of type sets interpreting types is such that it tightly couples the two conditions (S.1) and (S.2). Before we state and prove the Soundness Lemma, we prove an auxiliary result that is needed later in the proof.

Lemma 1.5.9. For each type σ, E(i_{σ}(V)) ∈ ⟦σ⟧.

Proof: By induction on the structure of σ. For base type ı, E(i_{ı}(V)) = E(V) is in ⟦ı⟧ by definition. For higher order types we need to show (P.1) and (P.2). Let E(W) ∈ ⟦σ⟧.

(i_{σ→τ}(V) W) = E(i_{τ}(V j_{σ}(W)))  by defn. of i_{σ→τ}
= E(let x=(V j_{σ}(W)) in i_{τ}(x)) by (let.2)
= (let x=(V j_{σ}(W)) in E(i_{τ}(x))) by (C-appl.1)

This shows (P.1), since E(i_{τ}(x)) is in ⟦τ⟧ by the induction hypothesis. (P.2) can be shown by computing

j_{τ}(R(i_{σ→τ}(V) W)) = j_{τ}(R(E(i_{τ}(V j_{σ}(W))))) by defn. of i_{σ→τ}
= (V j_{σ}(W))  by (r-e) and Lemma 1.4.2
= (j_{σ→τ}(i_{σ→τ}(V)) j_{σ}(W)) by Lemma 1.4.2.

Thus, E(i_{σ→τ}(V)) is in ⟦σ→τ⟧.

Lemma 1.5.10 (Soundness). Assume Γ is a typing hypothesis such that Γ ▷_{cp} M: σ. Let ρ be a substitution satisfying Γ, and let ρ′ be a substitution such that for each x_{i}: σ_{i} ∈ Γ, ρ′(x_{i}) = j_{σ_{i}}(ρ(x_{i})). Then,

T_{ml♯}⟦M⟧ρ ε ⟦σ⟧  (S.1)

j_{σ}(R(ρ\overline{\overline{M}}^{♯})) = ρ′M  (S.2)

Proof: By induction on the type derivation of Γ ▷_{cp} M: σ. Note that (S.2) implies that

j(R(ρ \overline{\overline{M}}^{♯})) = j(R(ρ\{i(j(x))/x\}\overline{\overline{M}}^{♯})).  (S.3)

Case (var): Assume Γ ▷_{cp} x: σ. This implies that x: σ ∈ Γ. To prove (S.1) we need to show that ⟦x⟧ρ ε ⟦σ⟧, which is true for any ρ that satisfies Γ. To show (S.2) we compute

j_{σ}(R(ρ(\overline{\overline{x}}^{♯}))) = j_{σ}(R(ρ(E(x)))) by defn. of \overline{\overline{x}}^{♯}
= j_{σ}(R(E(ρ(x)))) since E is closed
= j_{σ}(ρ(x))  by (r-e)
= ρ′(x)  by defn. of ρ′.

Case (app): Assume Γ ▷_{cp} M: σ→τ and Γ ▷_{cp} N: σ so that Γ ▷_{cp} (M N): τ. Let ρ be a substitution that satisfies Γ. (S.1): By induction hypothesis ⟦M⟧ρ ε ⟦σ→τ⟧ and ⟦N⟧ρ ε ⟦σ⟧. By definition,

⟦(M N)⟧ρ = (R(⟦M⟧ρ) R(⟦N⟧ρ)) = App(⟦M⟧ρ, ⟦N⟧ρ)

and, by Lemma 1.5.6, App(⟦M⟧ρ, ⟦N⟧ρ) ε ⟦τ⟧. (S.2): By induction hypothesis,

j(R(⟦M⟧ρ)) = ρ′M and j(R(⟦N⟧ρ)) = ρ′N,

and by Lemma 1.5.7,

j(R(App(⟦M⟧ρ, ⟦N⟧ρ))) = (j(R(⟦M⟧ρ)) j(R(⟦N⟧ρ))) = (ρ′M ρ′N) = ρ′(M N).

Case (abs): Assume Γ, x: σ ▷_{cp} M: τ so that Γ ▷_{cp} λx.M: σ→τ. To show (S.1), first observe that

ρ \overline{\overline{λx.M}}^{♯} = ρ(E(λx.\overline{\overline{M}}^{♯})) = E(ρ(λx.\overline{\overline{M}}^{♯})),

so that ρ \overline{\overline{λx.M}}^{♯} is of the form E(V), and thus, we need to show that ρ \overline{\overline{λx.M}}^{♯} ∈ ⟦σ→τ⟧. Let E(W) ∈ ⟦σ⟧, and show (P.1) and (P.2). We have

(ρ(λx.\overline{\overline{M}}^{♯}) W) = ((λx.ρ\{x/x\}\overline{\overline{M}}^{♯}) W) by defn. of subst.
= ρ\{W/x\}\overline{\overline{M}}^{♯}  by (β_{v}).

Since E(W) ∈ ⟦σ⟧, ρ{W/x} satisfies Γ, x: σ, so by the induction hypothesis (S.1),

ρ\{W/x\}\overline{\overline{M}}^{♯} ε ⟦τ⟧. This establishes (P.1). To show (P.2) compute

j_{τ}(R(ρ(λx.\overline{\overline{M}}^{♯}) W)) = j_{τ}(R(ρ\{W/x\}\overline{\overline{M}}^{♯}))  by (β_{v})
= j_{τ}(R(ρ\{i_{σ}(j_{σ}(W))/x\}\overline{\overline{M}}^{♯})) by ind. hyp. (S.2) and (S.3)
= j_{τ}(R(ρ(λx.\overline{\overline{M}}^{♯}) i_{σ}(j_{σ}(W)))) by (β_{v})
= (j_{σ→τ}(ρ(λx.\overline{\overline{M}}^{♯})) j_{σ}(W))  by defn. of j_{σ→τ}.

(S.2) follows by direct computation and Lemma 1.5.9.

j(R(ρ \overline{\overline{λx.M}}^{♯})) = j(λx.ρ\{x/x\}\overline{\overline{M}}^{♯})  by defn’s and (r-e)
= λx.j(R(ρ\{i(x)/x\}\overline{\overline{M}}^{♯})) by defn. of j_{σ→τ}
= λx.ρ′{j(i(x))/x}M  by Lemma 1.5.9 and ind. hyp. (S.2)
= ρ′(λx.M)  by Lemma 1.4.2 and defn. of subst.

Theorem 1.5.11 (Retraction, for T_{ml♯}). Let M be closed such that ▷_{cp}M: σ. Then,

λ_{c} ⊢ M = j_{σ}(R(\overline{\overline{M}}^{♯})).

Proof: Follows immediately from Lemma 1.5.10.

1.5.3 Back to CPS

We now focus on continuations and the modified, as well as original, CPS transform.

The modified transform

Observe that in the proof of the Soundness Lemma and the Retraction Theorem we only used abstract properties of functions E and R, namely that R ∘ E = id. Therefore, if E and R are replaced by any functions E′ and R′ (of the correct type) for which R′ ∘ E′ = id, our results will still hold. In particular, recall that, in the definition of the modified CPS transform, E^{K} and R^{K} were defined as λxk.k x and λx.x id respectively, and it follows that λ_{cp∀} ⊢ R^{K} ∘ E^{K} = id. This gives us the retraction result for the modified CPS transform as a direct corollary of Lemma 1.5.10.

Corollary 1.5.12. Let M be a λ_{cp} term, and let Γ be a typing hypothesis such that Γ▷_{cp} M: σ. Let ρ be a substitution satisfying Γ and let ρ′(x_{i}) = j_{σ_{i}}(ρ(x_{i})) for each x_{i}: σ_{i} ∈ Γ. Then,

T_{cps♯}⟦M⟧ρ ε ⟦σ⟧,  (S.1_{K})

and

λ_{cp∀} ⊢ ρ′M = j_{σ}(R^{K}(ρ \overline{M}^{♯})).  (S.2_{K})

In particular, if M is closed

λ_{cp∀} ⊢ M = j_{σ}(R^{K}(\overline{M}^{♯})).

The original transform

Unfortunately, the modified CPS transform differs slightly from the original CPS transform, and the above corollary does not apply. Nevertheless, we can salvage the retraction result by examining similarities and differences between the CPS transform and its modified counterpart, and adjusting the definitions of the ε-relation and pseudo-application appropriately. Looking at the transforms of an application one can see that if \overline{M} = E(R(\overline{M})) and \overline{N} = E(R(\overline{N}))^{11} we have

\overline{(M N)} = λk.(R(\overline{M}) R(\overline{N}) k).

It will follow that for a proper substitution ρ, ρ \overline{M} = E(R(ρ \overline{M})), and therefore that the the modified and original CPS terms only differ by (η) with respect to the continuation variable k, i.e. for a proper substitution, ρ, λk.(ρ \overline{M}^{♯} k) = ρ\overline{M}. However, since ρ \overline{M}^{♯} may not be a value, this equality may not hold in λ_{cp∀}. The role of the ε-relation is to separate essential form non-essential (for our purposes) structure of a term. Thus we can modify the ε-relation to hide the extra structure introduced by the CPS transform. The new ε-relation is defined as follows.

Definition 1.5.13. For a term M and a type set S write

M ε^{K} S iff M = λk.((let x_{1}=P_{1}, …, x_{k}=P_{k} in E(V)) k)

for some E(V) ∈ S, and where k is a fresh variable and x_{1}, …, x_{k} include all free variables in V. As before we write M = λk.((let x=P in I(V)) k) whenever M ε^{K} S. Note that M ε^{K} S iff λk.(M k) ε S, assuming k is not free in M.

Remark. Recall that in the definition of the interpretation of types (definition 1.5.4) we used the ε-relation, as well as terms E and R. In this section we assume ⟦σ⟧ to be defined using the ε^{K} relation and terms E^{K} and R^{K} instead. Similarly, we use the ε^{K}-relation in the definition of validity (definition 1.5.8).

The definition of the pseudo-application in the codomain of the CPS transform is derived from the transform of the application. Namely we have

\overline{(M N)} = λk.\overline{M} (λm.\overline{N} (λn.m n k)),

and consequently we define App^{K}, so that \overline{(M N)} = App^{K}(\overline{M}, \overline{N}).

11For the rest of this section we drop the superscripts from E^{K} and R^{K}.

Definition 1.5.14. The pseudo-application in the codomain of the CPS transform is defined to be

App^{K}(M, N) =^{def} λk.M (λm.N (λn.m n k)).

Having defined T_{cps}⟦M⟧ρ, ⟦σ⟧, App^{K} and ε^{K} we need to show that these definitions fit together as before. Namely, it remains to prove that conditions (†) and (‡) hold. We do so in the two lemmas below.

Lemma 1.5.15. Let M and N be two terms such that M ε^{K} ⟦σ→τ⟧ and N ε^{K} ⟦σ⟧. Then,

App^{K}(M, N) ε^{K} ⟦τ⟧.

Proof: By assumption,

M = λk.((let x_{1}=P_{1} in E(V_{1})) k) and N = λk.((let x_{2}=P_{2} in E(V_{2})) k)

for some E(V_{1}) ∈ ⟦σ→τ⟧ and E(V_{2}) ∈ ⟦σ⟧. Thus we have

λk.M (λm.N (λn.m n k)) =

= λk.(λk.((let x_{1}=P_{1} in E(V_{1})) k))
(λm.(λk.((let x_{2}=P_{2} in E(V_{2})) k)) (λn.m n k)))  by assumption
= λk.((let x_{1}=P_{1} in E(V_{1}))
(λm.((let x_{2}=P_{2} in E(V_{2})) (λn.m n k)))  by (β_{v})
= λk.(E(let x_{1}=P_{1} in V_{1})
(λm.(E(let x_{2}=P_{2} in V_{2}) (λn.m n k)))  by (C-appl.1)
= λk.((λxk′.k x) (let x_{1}=P_{1} in V_{1})
(λm.((λxk′.k′ x) (let x_{2}=P_{2} in V_{2}) (λn.m n k)))  by defn. of E
= λk.((let x_{1}=P_{1} in V_{1}) (let x_{2}=P_{2} in V_{2}) k)  by (C-appl.3)

and Lemma 1.2.8

= λk.((let x_{1}=P_{1} in (let x_{2}=P_{2} in (V_{1} V_{2}))) k)  by (C-appl.2)
= λk.((let x_{1}=P_{1} in (let x_{2}=P_{2} in
λk′.((let x=Q in E(W)) k′))) k)  by (P.1)
= λk.(let x_{1}=P_{1} in (let x_{2}=P_{2} in ((let x=Q in E(W)) k))) by (C-appl.2),

and (β_{v})

= λk.((let x_{1}=P_{1} in (let x_{2}=P_{2} in (let x=Q in E(W)))) k) by (C-appl.2).

Lemma 1.5.16. Assume M ε^{K} ⟦σ→τ⟧ and N ε^{K} ⟦σ⟧. Then,

j_{τ}(R(App^{K}(M, N))) = (j_{σ→τ}(R(M)) j_{σ}(R(N))).

Proof: Assume that M ε^{K} ⟦σ→τ⟧ and N ε^{K} ⟦σ⟧ so that for E(V_{1}) ∈ ⟦σ→τ⟧ and E(V_{2}) ∈ ⟦σ⟧, M = λk.((let x_{1}=P_{1} in E(V_{1})) k) and N = λk.((let x_{2}=P_{2} in E(V_{2})) k).

j(R(App^{K}(M, N))) = j(R(λk.M (λm.N (λn.m n k))))  by defn.
= j(R(λk′.(λk.(let x_{1}=P_{1} in E(V_{1})) k)
(λm.(λk.(let x_{2}=P_{2} in E(V_{2})) k) (λn.m n k′)))) by assumption
= j(R(λk.(let x_{1}=P_{1} in (let x_{2}=P_{2} in (V_{1} V_{2}))) k))  as in Lemma 1.5.15
= j(R(let x_{1}=P_{1} in (let x_{2}=P_{2} in (V_{1} V_{2}))))  by Lemma 1.2.8
= (let x_{1}=P_{1} in (let x_{2}=P_{2} in j(R(V_{1} V_{2}))))  by (C-appl.1)
= (let x_{1}=P_{1} in (let x_{2}=P_{2} in (j(V_{1}) j(V_{2}))))  by (P.2)
= (j(R(let x_{1}=P_{1} in E(V_{1}))) j(R(let x_{2}=P_{2} in E(V_{2}))))  by (r-e), and

(C-appl.1)

= (j(R(λk.(let x_{1}=P_{1} in E(V_{1})) k))
j(R(λk.(let x_{2}=P_{2} in E(V_{2})) k)))  by Lemma 1.2.8
= (j(R(M)) j(R(N)))  by assumption

Using these results, we get a version of the Soundness Lemma (Lemma 1.5.10) for the original CPS transform.

Lemma 1.5.17. Assume Γ is a typing hypothesis such that Γ ▷_{cp} M: σ. Let ρ be a substitution satisfying Γ, and let ρ′ be the substitution such that, for each x_{i}: σ_{i} ∈ Γ, ρ′(x_{i}) = j_{σ_{i}}(ρ(x_{i})). Then,

T_{cps}⟦M⟧ρ ε^{K} ⟦σ⟧  (S.1′_{K})

j_{σ}(R(ρ \overline{M})) = ρ′M  (S.2_{K})

Proof: The (var) and (abs) cases are the same as in Lemma 1.5.10. The (app) case follows from lemmas 1.5.15 and 1.5.16.

Finally, as a direct corollary, we obtain the Retraction Theorem for the original CPS transform advertised in the introduction.

Theorem 1.5.18 (Retraction, for the CPS transform). Let M be a closed term such that ▷_{cp}M: σ. Then,

λ_{cp∀} ⊢ M = j_{σ}(R^{K}(\overline{M})).

Proof: Follows immediately from Lemma 1.5.17.

1.5.4 The state passing style transform

Analogous to the CPS transform, to give a functional interpretation of a language with mutable store, we define the state passing style (SPS) transform. In this section we will sketch how the Retraction Theorem can be proved for the SPS transform. As learned in the previous section, the key in translating the ideas from the abstract version of the Retraction Theorem for the modified computational transform is the definition of the proper ε-relation, as well as the definition of the pseudo-application such that conditions (†) and (‡) are satisfied.

The SPS transform, T_{sps}, maps λ_{cp} to an extension of λ_{cp} with product types, denoted λ_{cp×}. Assume S is a special type denoting the state of the store. For instance, S can be defined to be a function space Loc→Val, where Loc denotes the type of locations and Val denotes the type of values that can be stored in the store. Note that the development we sketch below, does not depend on the actual implementation of a store, so we will think of S as representing an abstract mutable store.

The computations interpreting programs that may change the store are defined as terms of type S→(σ×S). The SPS transform maps terms to computations, as given in Table 1.13. (Note: we write (let ⟨x, y⟩=M in N) to abbreviate (let z=M, x=π_{1}(z), y=π_{2}(z) in N).) To

x^{∗} =^{def} λs.⟨x, s⟩
λx.M^{∗} =^{def} λs.⟨λx.M^{∗}, s⟩
(M N)^{∗} =^{def} λs.(let ⟨x_{1}, s_{1}⟩=(M^{∗} s), ⟨x_{2}, s_{2}⟩=(N^{∗} s_{1}) in (x_{1} x_{2} s_{2}))
(let x=M in N)^{∗} =^{def} λs.(let ⟨x, s_{1}⟩=(M^{∗} s) in (N^{∗} s_{1}))

\begin{matrix}ı′ & =^{def} & ı \\ (σ→τ)′ & =^{def} & σ′→(S→(τ′ × S)) \end{matrix} {x_{i}: σ_{i}}′ =^{def} {x:_{i}: σ′_{i}}

(Γ ▷_{cp} M: σ)^{∗} =^{def} Γ′ ▷_{cp×} \overline{M}: S→(σ′ × S)

Table 1.13: The SPS transform.

apply the proof of the Retraction Theorem for the modified computational transform to the SPS transform we define interpretations of terms and types, the pseudo-application, and the ε-relation. Before we do so, we need to define terms E^{S} and R^{S}, the intuitive meaning of which is analogous to the meaning of E^{K} and R^{K} used in the Retraction Theorem for the CPS transform. We define

E^{S} =^{def} λx.λs.⟨x, s⟩ and R^{S} =^{def} λx.(π_{1}(x initial-state),

where initial-state is a value of type S, denoting some initial state of the store. It follows easily, that R^{S} ∘ E^{S} = id is provable in λ_{cp×}.

The interpretation of terms using the SPS transform is defined to be

T_{sps}⟦M⟧ρ =^{def} ρ(M^{∗}).

The notion of type sets and interpretation of types, is the same as before, but using the definitions of E^{S}, R^{S} and ε^{S} instead of E, R and ε. Relation ε^{S} is defined as follows. If S is a type set and M is a term we write M ε^{S} S iff there is a term P and a value V, such that M = λs.(let x=P in ⟨V, s⟩). Finally, the pseudo-application App^{S} is defined to be

App^{S}(M, N) =^{def} λs.(let ⟨x_{1}, s_{1}⟩=(M s), ⟨x_{2}, s_{2}⟩=(N s_{1}) in (x_{1} x_{2} s_{2}))).

It can be shown that, using the above definitions, conditions (†) and (‡) hold, and we obtain the Retraction Theorem for the SPS transform.

Theorem 1.5.19 (Retraction, for the SPS transform). For any type σ, and every closed term M, such that ▷_{cp×}M: σ,

λ_{cp×} ⊢ M = j_{σ}(R(M^{∗})).

1.5.5 Extensions of the main results

Simply typed lambda calculus serves well as an elementary model of a functional programming language, but it is too simple to serve as a practical programming language. To make our results applicable to a real-life situation, we need to extend the Retraction Theorem to a more powerful language. There are two directions in which one can proceed. We can add additional language constructs to the language (such as numerals and primitive operations, if-then-else, recursion, etc.), or we can extend the type system of the language. We discuss some extensions using both approaches for which we have been able to prove the retraction theorem, as well as, those for which we only have partial results.

Adding new language constructs

Extending the Retraction Theorem to an extension of λ_{cp} with constants of a base type and primitive operators such as numerals is quite straightforward. However, adding arbitrary constants of higher order types may be more difficult. The difficulty lies in ensuring the closure conditions imposed on type sets by the addition of such constants are satisfied. For example if a constant c of type σ→τ is added to λ_{cp}, we need to make sure that if M ε σ then App(\overline{\overline{c}}^{♯}, M) ε τ. While such closure conditions are determined based on the type of new constants, the proof they are satisfied will, in general, depend on the functional behavior of the new constants.

Numerals and primitive operators: One of the simplest extensions of λ_{cp} is to add natural numbers together with primitive operators, such as successor and predecessor. This extension of λ_{cp} includes adding a new base type of natural numbers, as well as adding the constants to denote numerals and primitive operators. The Retraction Theorem, for any of the transforms we have discussed, can easily be extended to the extended calculus. The proof is given in Section 1.9.2.

Divergent element: The difference between call-by-name and call-by-value evaluation strategies becomes apparent only in presence of actual computational effects. So far we have only considered pure simply typed terms. In this setting every closed term is equivalent to a value in both logics of λ_{cp} and λ_{n}. Therefore, if we were to stop here, it would be unjustified to claim significant improvement over the original Meyer-Wand Retraction Theorem.

The simplest computational effect we can add to the language is divergence. In presence of divergence λ_{n} reasoning is no longer sound for call-by-value languages, so for any applications in λ_{cp} extended with divergence, we really need the stronger version of the Retraction Theorem provable in the weaker logic of λ_{cp}. While extension of the Retraction Theorem to a language with divergence, which we now present, is quite straightforward, it is important since it illustrates the practical difference between Meyer and Wand’s and our formulation of the Retraction Theorem.

Divergence is represented by the divergent element, Ω, that is added to the language of λ_{cp} as a constant, but it is not considered a value. The axioms for Ω specify that an application diverges if either the operators or the operand diverges. Moreover, these axioms identify all divergent terms. The axioms are:

(Ω M) = Ω  (Ω.1)

(M Ω) = Ω.  (Ω.2)

One can verify that the resulting equational logic is consistent and that it cannot prove Ω = V for any value V. The type system is extended with the axiom

Γ ▷_{cp} Ω: σ  (Ω)

which says that Ω has every type. The modified computational transform is defined on Ω to be

\overline{\overline{Ω}}^{♯} =^{def} Ω.

Since Ω has every type, to prove the Retraction Theorem for λ_{cp}+Ω we need to extend Lemma 1.5.10 for the case of typing axiom (Ω). In other words we need to show (S.1): that

\overline{\overline{Ω}}^{♯} ε ⟦σ⟧, and (S.2): that j_{σ}(R(\overline{\overline{Ω}}^{♯})) = Ω for every type σ. The second condition follows

trivially from the definition of \overline{\overline{Ω}}^{♯} and axiom (Ω.2). To prove the first condition observe that

Ω = (let x=Ω in E(i(x))),

and by Lemma 1.5.9, E(i_{σ}(x)) ∈ ⟦σ⟧ for every σ.

The very same reasoning can be applied to extend the Retraction Theorem for the CPS transform to λ_{cp}+Ω. The CPS transform is defined on Ω to be

\overline{Ω} =^{def} λk.Ω k.

Conditions (S.1′_{K}): that \overline{Ω} ε^{K} ⟦σ⟧ for every type σ, and (S.2_{K}): that j_{σ}(R(\overline{Ω})) = Ω, in Lemma 1.5.17 are proved as above.

Extending the type system

Many programming languages have more complex type systems than simple types, so to extend the applicability of our result we will discuss what is needed to extend the retraction result to a language with a richer type system.

A new type system will, in general, introduce new types, new typing rules, and sometimes new term constructors. First we need to extend the definitions of type sets ⟦σ⟧, as well as, functions j_{σ} and i_{σ} for each new type σ. This has to be done in such a way that

• j_{σ} ∘ i_{σ} = id,

• j_{σ}(V) and i_{σ}(V) are values, for any value V, and

• conditions (S.1) and (S.2) in Lemma 1.5.10 are preserved by the new type inference rules.

Moreover, if new term constructors are introduced, such as pairs and projections, one needs to extend the definition of the transform to include the new terms.

Products and sums: The retraction result can easily be extended to a language with products and/or sums. Let λ_{cp×} denote the extension of λ_{cp} with product types and similarly for λ_{c} and λ_{cp∀}. Then we can obtain the following results.

Theorem 1.5.20. For every λ_{cp×} type σ, there is a term R_{σ}, such that for any closed M of type σ,

λ_{c×} ⊢ M = (R_{σ} \overline{\overline{M}}^{♯}).

Theorem 1.5.21. For every λ_{cp×} type σ, there is a term R_{σ}, such that for any closed M of type σ,

λ_{cp∀×} ⊢ M = (R_{σ} \overline{M}).

The proof of the above extensions is quite straightforward, but lengthy and is given in Section 1.9.2. Analogous results can be obtained for an extension of λ_{cp} with sum types.

Recursive types: The recursive type discipline introduces types of the form μt.σ. We intend to interpret a type μt.σ as a fixed point of the function t ↦ σ. In order to extend our results to λ_{cp} extended with recursive types we need to define retraction-embedding pairs (j_{σ}, i_{σ}) at new types. In particular how does one define i_{μt.σ} and j_{μt.σ}, or even i_{t} and j_{t}?

To motivate a solution, consider the following example. Let τ = μt.t→t. Then in the recursive type discipline one can type ▷(λx.x x): τ→τ. Assume we have defined terms i_{τ} and j_{τ}, and we try to compute

j_{τ→τ}(R(\overline{\overline{λx.x x}}^{♯})) = j_{τ→τ}(R(E(λx.x x)))
= j_{τ→τ}(λx.x x)
= λx.j_{τ}(R(i_{τ}(x) i_{τ}(x)))
= ?

To complete this derivation, one would like to have i_{τ}(x) = E ∘i_{τ} ∘x∘j_{τ}, so we can continue

\begin{aligned}⋯ & = & λx.j_{τ}(E(i_{τ}(x j_{τ}(i_{τ}(x))))) \\ & = & λx.x x \end{aligned}

What we see from this example is that the two occurrences of x in λx.x x “act” as having types τ→τ and τ, respectively. Similarly, we would like the two occurrences of i_{τ} in λx.j_{τ}(R(i_{τ}(x) i_{τ}(x))) to “act” as i_{τ→τ} and i_{τ}. A solution to our problem is to find a uniform definition for i’s and j’s at all types. Namely, we want a retraction-embedding pair (j, i) that satisfies the following definition.

Definition 1.5.22. A term F is called a total function if F is a value and, for any value V, (F V) is provably equal to a value.

A pair of total functions (j, i) is a uniform retraction-embedding pair if i and j satisfy system of equations

\begin{aligned}j(f) & = & j ∘ R ∘ f ∘ i \\ i(g) & = & E ∘ i ∘ g ∘ j \\ j ∘ i & = & id. \end{aligned}  (⋆)

While it remains open whether there is a pair of terms satisfying the above conditions, we will assume we are given such a pair of functions and, under this assumption, show how the Retraction Theorem can be extended to recursive types. Moreover, since the recursive type system can type all terms, as a corollary we obtain the following theorem.

Theorem 1.5.23. Assume total functions i and j exist that satisfy equations (⋆). Then, for any closed lambda term M,

λ_{c} ⊢ M = j(R(\overline{\overline{M}}^{♯})).

Of course, the analogous theorems hold for the other transforms as well.

We now proceed with the proof of Theorem 1.5.23. First, since we need to define interpretation of all types, which includes types with free variables and, in particular, type variables alone, the interpretation will be defined relative to a type environment. A type environment is simply a function mapping type variables to type sets. Secondly, for technical reasons that will become apparent later, instead of dealing with untyped terms, we will work with derivable type sequents.^{12} Hence, our definitions of Section 1.5.1 need to be modified slightly.

Definition 1.5.24. A type set is any set of derivable typing sequents of the form Γ▷E(V): σ, for some value V, closed under all possible typings, i.e., if S is a type set and Γ ▷ E(V): σ is in S, then all derivable sequents Γ_{1} ▷ E(V): σ_{1} are in S as well. Let D denote the set of all derivable typing sequents, and let S be the set of all type sets.

12Up to now, the typing of all terms was implicit, but in this section we need to refer to types of terms explicitly.

Definition 1.5.25. The relation ε is a subset of D × S defined by Γ ▷ M: σ ε S iff there is Γ_{1} ▷E(V): σ_{1} ∈ S such that Γ▷M = (let x_{1}=P_{1}, …, x_{k}=P_{k} in E(V)) : σ, where x_{i}’s contain all free variables in V.

The recursive type system extends the simple types by adding type variables and type expressions of the form μt.σ. The new inference rules are

\frac{Γ ▷ M: σ\{μt.σ/t\}}{Γ ▷ M: μt.σ}  (μ I)

\frac{Γ ▷ M: μt.σ}{Γ ▷ M: σ\{μt.σ/t\}}  (μ E)

One can understand these rules by considering the type μt.σ as the type τ, satisfying equation τ = σ{τ/t}. Thus we need to define the interpretation, ⟦τ⟧ν, of τ such that it satisfies the equation

⟦τ⟧ν = ⟦σ{τ/t}⟧ν.

In other words ⟦τ⟧ν should be a fixed point of the function

λS.⟦σ⟧ν{S/t}.

(We assume the interpretation will satisfy ⟦σ{τ/t}⟧ν = ⟦σ⟧ν{⟦τ⟧ν/t}.) The difficulty lies in showing that for any σ and ν, the function λS.⟦σ⟧ν{S/t} always has a fixed point. To do so, we define a metric on the space of all type sets so that the resulting metric space is complete. Then we show that each function λS.⟦σ⟧ν{S/t} is a contraction, and thus, by Banach’s Fixed-point Theorem, has a unique fixed point. Mac Queen et al. [MPS86] have developed such a framework, of which our development can be viewed as a special case. Namely, our domain consists only of finite elements (typing sequents) ordered under discrete order, thus greatly simplifying general purpose structures used in [MPS86].

The metric on the space S of all type sets is defined using a rank function. In general, a rank function is any function assigning natural numbers to elements of the domain — in our case typing sequents.

Definition 1.5.26. For any two type sets S and R, the closeness of S and R is equal to

c(S, R) =^{def} min {rank(s) | s ∈ S ⊕ R},

where S ⊕ R denotes the symmetric difference between two sets. If the the sets S and R are the same, we define c(S, R) = ∞. The distance between S and R is defined

d(S, R) =^{def} 2^{−c(S,R)}.

If c(S, R) = ∞, we define d(S, R) = 0.

The proof that d is a metric on S can be found in [MPS86]. Moreover, this construction is a general one for which it can be shown that (S, d) is a complete metric space (see [MPS86]).

Recall that (S, d) is a complete metric space iff every Cauchy sequence in (S, d) has a limit in (S, d).

Lemma 1.5.27. The metric space (S, d) is complete. In particular if ⟨S_{i}⟩ is a Cauchy sequence in (S, d), the set S of all typing sequents s, that occur in all but finitely many S_{i} is the limit of ⟨S_{i}⟩.

Recall the definition of a contraction and Banach’s Fixed-point Theorem.

Definition 1.5.28. A function f: S → S is (uniformly) contractive if there is a real number 0 ≤ α < 1, such that for all S, R ∈ S,

d(f(S), f(R)) ≤ α d(S, R).

Function f is called non-expansive if the condition on α is relaxed to 0 ≤ α ≤ 1.

Theorem 1.5.29 (Banach). Let (X, d) be a complete metric space, and let f: X → X be a contraction. The, f has a unique fixed-point in X.

In particular, in metric space (S, d), the contractive (non-expansive) functions are characterized in terms of closeness.

Proposition 1.5.30 (Mac Queen et al.). A function f: S^{n} → S is non-expansive iff for all S_{1}, …, S_{n}, R_{1}, …, R_{n} ∈ S we have

c(f(S_{1}, …, S_{n}), f(R_{1}, …, R_{n})) ≥ min_{i} c(S_{i}, R_{i}),

and is contractive iff for all S_{1}, …, S_{n}, R_{1}, …, R_{n} ∈ S, with some S_{i} ≠ R_{i} we have

c(f(S_{1}, …, S_{n}), f(R_{1}, …, R_{n})) > min_{i} c(S_{i}, R_{i}).

Finally, we define a particular rank function based on the type of a sequent.

Definition 1.5.31. The rank of a type is defined as follows:

rank(ı) =^{def} 0
rank(t) =^{def} 0
rank(T (σ)) =^{def} 1 + rank(σ)
rank(σ→τ) =^{def} 1 + max {rank(σ), rank(τ)}
rank(μt.σ) =^{def} 1 + rank(σ).

The rank of a derivable typing sequent Γ ▷ M: σ is equal to rank(σ).

The important feature of the rank function is that is uniquely defined for every typing sequent, and that the rank of σ→τ is strictly larger than rank of either σ or τ, intuitively saying that a function has higher rank than its argument or result. We use this fact in the definition of type sets intended to interpret function spaces.

Definition 1.5.32. Let S be a type set and r be an integer. Define

S_{r} =^{def} {s ∈ S | rank(s) < r}.

Let S and R be type sets. Define S→_{S}R to be the set of all typing sequents Γ ▷ E(V): σ such that if r = rank(Γ ▷ E(V): σ), for all Γ_{1} ▷ E(W): σ_{1} ∈ S_{r}

• for all Γ_{2} and σ_{2} of rank less than r, Γ_{2} ▷ (V W): σ_{2} ε R_{r}, and

• Γ_{3} ▷ j(R(V W))=(j(V) j(W)) : σ_{3}, for some Γ_{3} and σ_{3}.

Lemma 1.5.33. f: S, R ↦ (S→_{S}R) is a contraction.

Proof: Fix type sets S_{1}, S_{2}, R_{1} and R_{2}. Using Proposition 1.5.30, it suffices to show that if s is a witness that S_{1}→_{S}R_{1} is different from S_{2}→_{S}R_{2}, then there is, either a witness that S_{1} is different from S_{2} or that R_{1} is different form R_{2}, of rank lesser than rank(s). Assume S_{1}→_{S}R_{1} ≠ S_{2}→_{S}R_{1}. Then there is Γ▷E(V): σ that is in one set but not the other. Without loss of generality we can assume Γ ▷ E(V): σ ∈ S_{1}→_{S}R_{1}. Let r = rank(Γ ▷ E(V): σ). Since Γ ▷ E(V): σ ∉ S_{2}→_{S}R_{2}, by the definition of →_{S}, there is Γ_{1} ▷ E(W): σ_{1} ∈ (S_{2})_{r}, such that either

• Γ_{2} ▷ (V W): σ_{2} ε̸ (R_{2})_{r}, for some Γ_{2} and σ_{2} of rank less than r, or

• Γ_{3} ▷ j(R(V W)) ≠ (j(V) j(W)) : σ_{3}, for all Γ_{3} and σ_{3}.

We have two cases: either Γ_{1} ▷ E(W): σ_{1} is in (S_{1})_{r}, or not.

Case Γ_{1} ▷E(W): σ_{1} ∈ (S_{1})_{r}: Then, by definition of →_{S}, and since Γ▷E(V): σ is in S_{1}→_{S}R_{1}, we must have Γ_{3} ▷ j(R(V W)) = (j(V) j(W)) : σ_{3}, and therefore it must be the case that Γ_{2} ▷ (V W): σ_{2} ε̸ (R_{2})_{r}, but, by definition of →_{S}, Γ_{2} ▷ (V W): σ_{2} ε (R_{1})_{r}. This, by definition of ε, implies there is Γ_{4} ▷ E(U): σ_{4}, of rank less than r, in R_{1}, but not in R_{2}. Therefore, c(R_{1}, R_{2}) < r.

Case Γ_{1} ▷ E(W): σ_{1} ∉ (S_{1})_{r}: Since Γ_{1} ▷ E(W): σ_{1} is in (S_{2})_{r}, it has rank less than r and is in S_{2}, but not in S_{1} and hence, c(S_{1}, S_{2}) < r.

In either case, c(S_{1}→_{S}R_{1}, S_{2}→_{S}R_{2}) > min(c(S_{1}, S_{2}), c(R_{1}, R_{2})).

We can now define interpretation of types.

Definition 1.5.34. Let ν be a type environment mapping type variables to type sets. The interpretation of types ⟦·⟧ is defined as follows:

⟦ı⟧ν =^{def} ⋃ S
⟦t⟧ν =^{def} ν(t)
⟦σ→τ⟧ν =^{def} ⟦σ⟧ν→_{S}⟦τ⟧ν
⟦μt.σ⟧ν =^{def} fixed point of λS.⟦σ⟧ν{S/t}

To show that this definition is a valid one we need to show that every function λS.⟦σ⟧ν{S/t} is a contraction, and therefore, by Banach’s theorem has a unique fixed point. Obviously, the function λS.⟦t⟧ν{S/t} = λS.S is not contractive. As discussed in [MPS86] (section 5), this is the only problematic case, and for all types σ that do not contain μt.t as a subexpression, ⟦σ⟧ν is well defined. To remedy this situation, we can either syntactically restrict the set of types, as done in [MPS86], to exclude the ones containing μt.t as a subexpression, or we can define the meaning of μt.t to be, say, the type set ⋃ S. Since every type set S is a fixed point of the identity function, this definition is consistent with our specification that ⟦μt.t⟧ν is a fixed point of λS.⟦t⟧ν{S/t}.

It remains to show how to modify Lemma 1.5.10 to extend the Retraction Theorem to recursive types. We only sketch the proof.

Lemma 1.5.35. Assume Γ ▷ M: σ is derivable, and let ρ be a substitution, and ν be a type environment such that for each x_{i}: σ_{i} ∈ Γ, Γ′ ▷ ρ(E(x)): T (σ′_{i}) ∈ ⟦σ_{i}⟧ν. Let ρ′ be substitution such that Γ ▷ ρ′(x_{i}) = j(ρ(x_{i})) : σ_{i} for each x_{i}: σ_{i} ∈ Γ. Then

• Γ′ ▷ ρ \overline{\overline{M}}^{♯}: T (σ′) ε ⟦σ⟧ν, and

• Γ ▷ M = j(R(ρ\overline{\overline{M}}^{♯})) : σ.

Proof Sketch: All cases, (var), (app), (abs) and (let) follow by almost the same argument. The only difference in (app) and (abs) cases comes form the modified definition of ⟦σ→τ⟧ν, where one need to pay attention to ranks of typing sequents. The recursive types introduction and elimination rules, (μ I) and (μ E), preserve validity, since by definition, ⟦μt.σ⟧ν is a fixed point of λS.⟦σ⟧ν{S/t}, and therefore we have

⟦μt.σ⟧ν = ⟦σ⟧ν{⟦μt.σ⟧ν/t} = ⟦σ{μt.σ/t}⟧ν.

The second condition of the lemma for these rules follows trivially.

We conclude with the proof of Retraction Theorem.

Proof: [of Theorem 1.5.23] If M is closed then the typing sequent ∅▷M: μt.t→t is derivable. By the previous lemma we have

∅ ▷ M = j(R(\overline{\overline{M}}^{♯})) : μt.t→t.

Erasing the type information from the proof of the above equation in context, we obtain the proof of the untyped equation M = j(R(\overline{\overline{M}}^{♯})).

By same arguments as presented in Section 1.5.3, the above proof can be modified for the CPS transform.

1.6 Applications

The CPS transform has found applications in studying semantics of programs, as well as, in devising better compilation techniques. We point out that the retraction approach only attempts to explain the relation between equivalence classes of direct style and CPS terms. In CPS based compilers, one is also interested in other features of CPS terms, such as their structure and suitability for various optimizations (see [App92]). In comparison with the results in [FSDF93, SF92, SW96], which provide more precise relation between terms and their images under the CPS transform in terms of reduction relation, we feel that our result will be of greater importance in studying the semantics of programs. We elaborate on an interesting application of the Retraction Theorem.

Riecke and Viswanathan [RV95] have found a particular use for the retraction-embedding pairs (j_{σ}∘R, E∘i_{σ}) defined in Section 1.4. Their main result shows how to define an operator, called encap, that enables a safe use of functional code in an extension of a programming language with imperative features such as assignments or jumps. Informally, their results can be summarized by saying that a term (encap M) behaves the same in the extended language as the term M does in the pure language.

The development in [RV95] depends on fully-abstract least fixed-point models of callby-value PCF (VPCF). We believe that their results can be shown to hold in a larger class of models by using the stronger equational version of the Retraction Theorem.

However, we must point out, that we have not been able to extend our version of the Retraction Theorem, to a programming language like the VPCF. Namely, our results do not cover a language with recursion.

To summarize Riecke-Viswanathan’s results in equational framework, let us focus on the CPS transform and an extension of the basic programming language with control.

Let E_{σ}^{K} =^{def} E^{K} ∘ i_{σ} and R_{σ}^{K} =^{def} j_{σ} ∘ R^{K}. For each type σ define the operator encap_{σ} so that the transform of (encap M) is

\overline{(encap_{σ} M)} = E_{σ}^{K}(R_{σ}^{K}(\overline{M})).

Let λ_{cp} (assume λ_{cp} includes numerals) be the calculus representing the pure programming language, and let λ_{cp+K} denote the extended calculus. In particular, λ_{cp+K} is extended with the control operators callcc and abort, and encap. Let C⟨[·]⟩ be a context in λ_{cp}, and let C_{+}⟨[·]⟩ be a context in λ_{cp+K}. Then the results analogous to those in [RV95] can be stated as follows.

Theorem 1.6.1. For any (typable) closed terms M and N in λ_{cp} we have,

• adequacy: λ_{cp} ⊢ M = n iff λ_{cp+K} ⊢ (encap_{nat} M) = n,

• preservation: ∀C⟨[·]⟩ . λ_{cp+K} ⊢ C⟨[M]⟩ = n iff λ_{cp+K} ⊢ C⟨[(encap M)]⟩ = n, and

• full abstraction:

∀C⟨[·]⟩ . λ_{cp} ⊢ C⟨[M]⟩ = C⟨[N]⟩

iff ∀C_{+}⟨[·]⟩ . λ_{cp+K} ⊢ C_{+}⟨[(encap M)]⟩ = C_{+}⟨[(encap N)]⟩.

The proof relies on the fact that the CPS transform is a transform from λ_{cp+K} to λ_{cp}, equational correspondence result, and the Retraction Theorem (see [RV95] for details).

Analogous result holds for the SPS transform and an extension of the basic programming language with assignment.

Remark. Since the equational correspondence result holds for all (untyped) terms, and by Theorem 1.5.23, the retraction result holds in all models of untyped λ_{cp} that contain total functions i and j satisfying equations (⋆), the above theorem holds in all such models as well. Is remains to be investigated how these models relate to those used in [RV95].

1.7 Related Work

In this work, we have established a relation between direct style and CPS terms using definable retraction functions. The Retraction Theorem shows that a term can be recovered, up to λ_{cp}-equivalence, from its image under the CPS transform. Therefore, the retraction approach, in fact, only provides a relation between equivalence classes of terms. On the other hand, in contrast to other results, the relation is established via retraction functions that are definable in the target language of the transform, and therefore can be used in applications like the one described in Section 1.6.

The retraction approach was first introduced by Meyer and Wand [MW85], and was further explored by Meyer and Riecke in [MR], where the authors point out some of the limitations of the original Meyer-Wand Retraction Theorem. Most notably, the original Retraction Theorem was proved in βη-equational logic which is not sound for call-by-value languages. In [MR], the provable equality is replaced by call-by-value observational congruence. However, authors fail to prove the Retraction Theorem in this setting and, in fact, show that the original retraction pairs defined in [MW85] no longer serve when βηequational reasoning is replaced with call-by-value observational congruence.

A semantic variation of the retraction approach has been studied by Riecke [Rie93], and later refined by Riecke and Viswanathan [RV95]. The motivation for their work was to isolate side-effects in sequential programs. To apply the reasoning to a call-by-value language, the authors focus on call-by-value PCF. Rather than working with provable equality, Riecke and Viswanathan construct a relation between two semantics of VPCF in least fixed-point models: the direct semantics, and monadic semantics (generalizing the CPS semantics) utilizing the additional structure of a strict monad. While their version of the Retraction Theorem holds only at base type, this suffices for deriving results by observational congruence as those discussed in Section 1.6.

One generalization of the Meyer-Wand Retraction Theorem is given by Filinski [Fil94]. He extends the CPS transform to the monadic metalanguage, λ_{ml}, and shows that for closed simply typed λ_{ml} term M,

λ_{ml} ⊢ M = β_{σ}(\overline{M}).

While this result enables embedding a purely functional language with a monadic feature in a call-by-value language with continuations (provided certain conditions are met), it still prohibits generalizations to a language with divergence as does the original Meyer-Wand theorem.

In applications of the CPS transform to compiler technology, definability of the retraction functions may not be relevant, but a more detailed relation between a term and its CPS form, as well as the knowledge about the structure of CPS terms is desirable.

The proof of Sabry Felleisen’s [SF92] equational correspondence result (Theorem 1.1.2) yields an inverse to CPS transform, but again, only up to λ_{c}-equivalence. Similar, but more extensive study of the several variants of the CPS transform has been done by Hatcliff and Danvy [HD94]. Besides the equational correspondence, they also study the structure of the transform in greater detail (e.g. separating the CPS transform into its generic part and “continuation introduction”, overhead of administrative reductions, etc.).

A different view of the CPS transform was presented by Flanagan et al. [FSDF93]. By observing implementations of typical CPS based compilers they suggest an alternative transformation that combines several phases done by the compiler.

Sabry and Wadler [SW96] exhibit an even stronger relation between direct style terms and their CPS forms. In particular, they construct an inverse of the CPS transform, as well as the computational transform, so that the transform and its inverse form a reflection. A transform T and its inverse T^{−1} are said to form a reflection if T (M) ↠^{∗} N iff M ↠^{∗} T^{−1}(N), and M is identical to T^{−1}(T (M)).

Above mentioned results provide more information on the structure of CPS terms which can be exploited in the design of CPS based compilers, but seem to have fewer implications for studying semantics of programs in presence of different computational effects.

1.8 Some Open Questions

In all practical applications, functional programming languages are equipped with some form of recursion. Therefore, to make the retraction approach applicable in practice, we need to extend our results to a language with recursion. This can be done in two ways: By extending the type system so that the fixed-point operator is definable in the pure language, or by adding a language construct such as constant Y, letrec, etc. The first approach has been discussed in Section 1.5.5.

One difficulty in adding fixed-point operator Y, or a similar language construct, is that additional closure conditions are needed in the definition of type sets, and we haven’t been able to construct type sets satisfying these conditions. The other difficulty is determining the correct axiomatization of a fixed-point operator. It appears that the axiom

(Y V) = (V (Y V))  (fix)

does not suffice. In models of λ_{c}, fixed-point operator can be defined using the so called fixpoint object. Crole and Pitts [CP92] define such an object in models of λ_{c}, and discuss a logical system for reasoning about fixpoint computations, which may hold the answer to above questions.

Another class of extensions is motivated by the application of the Retraction Theorem described in Section 1.6, where we have seen how one can isolate effects of an extension of a language with assignment or control from interfering with pure functional code. A natural question arises, whether it is possible to extend this approach to isolate one computational effect from interfering with code possibly containing a different computational effect. For instance, if M is a program in, say VPCF with assignment, can we define an operator similar to encap, so that, in an extension of VPCF with both assignment and control, (encap M) will behave the same as M behaves in the extension of VPCF with assignment. We believe that an appropriate extension of the Retraction Theorem to a programming language with imperative features will give us such results.

1.9 Appendix

1.9.1 Monads

In section 1.2.2 we gave an intuitive explanation of monads in the category of sets. We now summarize the definitions in a more general setting. The interested reader is also referred to [Mog88, Mog91, LS86, Cro93, ML71] for a more detailed discussion.

Standard categorical interpretation of functional programs assigns objects to types and morphism to terms. The Cartesian closed structure of a category ensures that (β) and (η) axioms are sound. However, in a call-by-value language, these axioms take restricted forms and the Cartesian close structure is no longer appropriate.

To capture computational aspects of programs, such as call-by-name and call-by-value evaluation strategies, Moggi [Mog88] introduced a framework based on monads. The basic idea behind using monads in a category to interpret programs, is that values are separated from computations. If an object A, in a category C, represents values (of type A) then the object T (A), where T is the functor of the monad, represents computations of type A. The reason for this distinction is that computations can have possible computational effects. For example, a computation can diverge, alter the store, or branch nondeterministically. The separation between values and computations allows an interpretation to differentiate between call-by-value and call-by-name languages. For instance, in a call-by-value language, a function form A to B would be interpreted as a morphism from A to T (B), modeling the fact that arguments are evaluated before they are passed to a function. On the other hand the same function in a call-by-name interpretation would be interpreted as a morphism from T (A) to T (B), since arguments are not evaluated before they are passed to a function. The functor T represents a particular notion of computation, e.g. continuation passing, partiality, nondeterminism, etc.

The formal definition of a monad in a category C is equivalent to one of a Kleisli triple in a sense that each Kleisli triple over C uniquely determines a monad in C and vice versa (see [Mog91]). We find the Kleisli triples more convenient to use.

Definition 1.9.1 ([Man76]). A Kleisli triple over a category C is a triple (T, η, ^{∗}), where T is a function mapping objects of C to objects of C, η is a family of morphisms indexed by objects of C, such that for each object A, η_{A}: A → T (A), and for each morphism f: A → T (B), f^{∗} is a morphism f^{∗}: T (A) → T (B) such that

• η_{A}^{∗} = id_{A},

• η_{A}; f^{∗} = f, for all f: A → T (B), and

• f^{∗}; g^{∗} = (f; g^{∗})^{∗}, for all f: A → T (B) and g: B → T (C).

Given a Kleisli triple (T, η, ^{∗}), the corresponding monad is defined by the triple (T, η, μ), where T is an extension of the function T to an endofunctor on C, by defining T (f) = (f; η_{B})^{∗} for f: A → B; η: Id →^{.} T is a natural transformation defined by η of the Kleisli triple, and μ: T^{2} →^{.} T is a natural transformation defined by μ_{A} = id_{T (A)}^{∗}.

Note that our discussion of a monad in Set is a special case of this definition. Given a Kleisli triple over C one can construct the Kleisli category, C_{T}, which is a syntax-free representation of the computational lambda calculus.

Definition 1.9.2 ([ML71, Mog91]). Let (T, η, ^{∗}) be a Kleisli triple. The Kleisli category, C_{T}, is defined as follows:

• the objects of C_{T} are objects of C,

• a morphisms f: A → B in C_{T} is a morphism f: A → T (B) in C,

• the identity on A in C_{T} is the morphism η_{A}: A → T (A) in C, and

• the composition of f: A → B followed by g: B → C in C_{T} is defined by the morphism f; g^{∗}: A → T (C) in C.

It is easy to verify that C_{T} is a category. C_{T} provides a model for the core of the computational lambda calculus, but to express products and functions additional structure is needed. Namely,

Definition 1.9.3. A strong monad in C is a monad (T, η, μ) together with a natural transformation t_{A,B}: A × T (B) → T (A × B), satisfying certain identities (see [Mog91]). Natural transformation t is also called tensorial strength.

Definition 1.9.4 ([Mog91]). A λ_{c}-model is a category C with finite products, a strong monad (T, η, μ, t) satisfying the mono requirement (i.e. η_{A} is mono for all A ∈ C) and T -exponential T (B)^{A} for every A, B ∈ C.

A Kleisli category (with tensorial strength and T -exponentials), is a syntax free representation of the computational lambda calculus, λ_{c}. There are notable differences between a CCC and a Kleisli category. For example, the composition in the Kleisli category does not represent substitution, as it does in a CCC, but rather it represents the let-constructor. Substitution in the computational lambda calculus corresponds to composition in the underlying category of the Kleisli category. Another difference is the interpretation of function spaces, which are interpreted as T -exponentials in the Kleisli category as opposed to ordinary exponentials in a CCC.

Example 1.9.5. Let C be a CCC, and let R be an object in C. The continuation monad, K, in C is given by the Kleisli triple (K, η, ^{∗}) with tensorial strength t defined as follows (using lambda notation):

K(A) =^{def} (A→R)→R
η_{A}: A→K(A) =^{def} λa: A.λk: (A→R).k a
f^{∗}: K(A)→K(B) =^{def} λc: K(A).λk: (B→R).c (λa: A.(f a) k)
t_{A,B}: (A×K(B))→K(A×B) =^{def} λ⟨a, c⟩: A×K(B).λk: ((A×B)→R).c (λb: B.k ⟨a, b⟩)

Other notions of computation, such as partiality, side-effects, exceptions and interactive I/O can also be expressed in terms of monads (see [Mog91]).

Every category C (with enough structure) can be viewed as a lambda theory, Th(C), called the internal language of the category, and conversely, for every lambda theory, Th, there is a category, Cl(Th), the classifying category of Th, such that the categories Cl(Th(C)) and C are equivalent (see [Cro93] and [LS86] for more details).

In this sense, the computational lambda calculus, λ_{c} is the internal language of the initial Kleisli category. Similarly, λ_{ml} is the internal language of the initial category in the category of CCC’s equipped with strong monads.

1.9.2 Extensions

Adding Numerals

The calculus λ_{cp}+numerals represents the following extension of λ_{cp}.

• The language of λ_{cp}+numerals is extended with constructs:

values  V ::= ⋯ | n | succ | pred

where n stands for numerals 0, 1, 2, etc. We write n+1 to denote the successor numeral of n.

• The logic of λ_{cp}+numerals is extended with axioms:

(succ n) = n+1  (succ)

(pred 0) = 0  (pred.0)

(pred n+1) = n  (pred.n)

• The type system of λ_{cp}+numerals is extended with the base type nat and the following typing axioms:

Γ ▷_{cp} n: nat  (num)

Γ ▷_{cp} succ: nat→nat  (succ)

Γ ▷_{cp} pred: nat→nat  (pred)

The modified computational transform must be extended appropriately. In particular we have

\overline{\overline{n}}^{♯} =^{def} E(n)

\overline{\overline{succ}}^{♯} =^{def} E(λx.E(succ x))
\overline{\overline{pred}}^{♯} =^{def} E(λx.E(pred x))

To prove the Retraction Theorem for the extended calculus we need to extend the proof of Lemma 1.5.10 with the three cases for the new type inference axioms. Before we do so, since nat is treated as a base type, we define

i_{nat} =^{def} id and j_{nat} =^{def} id,

and

⟦nat⟧ =^{def} {M | M = E(V) for some value V }.

We are now ready to extend the proof of Lemma 1.5.10.

Proof: (Extending the proof of Lemma 1.5.10.) Let Γ be a typing hypothesis and assume that ρ satisfies Γ.

Case (num): (S.1) follows immediately from definitions. For (S.2) compute

j_{nat}(R(ρ \overline{\overline{n}}^{♯})) = id(R(E(n))) = n.

Case (succ): To show (S.1) first observe that ρ′ \overline{\overline{succ}}^{♯} is of the form E(V), so we need to show that ρ \overline{\overline{succ}}^{♯} ∈ ⟦nat→nat⟧. Let E(W) ∈ ⟦nat⟧.

ρ \overline{\overline{succ}}^{♯} = E(λx.E(succ x)),

so

((λx.E(succ x)) W) = E(succ W)
= (let x=(succ W) in E(x)),

and, by definition of ⟦nat⟧, E(x) ∈ ⟦nat⟧. Therefore,

((λx.E(succ x)) W) ε ⟦nat⟧

as desired. To show (P.2) we compute

j_{nat}(R((λx.E(succ x)) W)) = j_{nat}(R((λx.E(succ x)) i_{nat}(j_{nat}(W))))
= (j_{nat→nat}(λx.E(succ x)) j_{nat}(W)),

using the fact that i_{nat} = j_{nat} = id. Finally, to show (S.2) compute

       j_{nat→nat}(R(ρ′ \overline{\overline{succ}}^{♯}))

= j_{nat→nat}(R(E(λx.E(succ x)))) by defn.
= j_{nat→nat}(λx.E(succ x))  by (r-e)
= λx.j_{nat}(R(E(succ i_{nat}(x)))) by defn. of j_{nat→nat}
= λx.succ x  by (r-e) and defn. of i_{nat} and j_{nat}
= succ  by (η_{v}).

Case (pred): This case is identical to the (succ) case.

The Retraction Theorem for the CPS transform can be extended in a similar manner by defining

\overline{n}  =^{def} λk.k n
\overline{succ}  =^{def} λk.k λx.(λk′.k′ (succ x))
\overline{pred}  =^{def} λk.k λx.(λk′.k′ (pred x)),

and extending the proof of Lemma 1.5.17 the same way we have done above.

Adding Products

The calculus λ_{cp×} is an extension of λ_{cp} with products. The language of λ_{cp×} is extended with the following term constructs:

values  V ::= ⋯ | π_{1}(V) | π_{2}(V) | ⟨V, V ⟩
terms  M ::= ⋯ | π_{1}(M) | π_{2}(M) | ⟨M, M⟩.

The types are enriched with the binary type constructor × and the type inference rules given in Table 1.14. The logic of λ_{cp×} contains the following axioms (taken from [Mog89])

Types:

σ ::= ⋯ | σ × σ

Inference Rules:

\frac{Γ ▷_{×} M: σ, Γ ▷_{×} N: τ}{Γ ▷_{×} ⟨M, N⟩: σ × τ}  (×I)

\frac{Γ ▷_{×} M: σ_{1} × σ_{2}}{Γ ▷_{×} π_{i}(M): σ_{i}} ,  i=1,2  (×E)

Table 1.14: Extension of a type system with products.

⟨M_{1}, M_{2}⟩ = (let x_{1}=M_{1} in (let x_{2}=M_{2} in ⟨x_{1}, x_{2}⟩))  (let.×)

π_{i}⟨V_{1}, V_{2}⟩ = V_{i}  (×.β)

⟨π_{1}(V), π_{2}(V)⟩ = V  (×.η)

These axioms specify that the pairs are strict and that the first component is always evaluated before the second. Consequently, the modified computational transform is extended to the new language constructs as follows:

\overline{\overline{π_{i}(M)}}^{♯} =^{def} E(π_{i}(R(\overline{\overline{M}}^{♯})))

\overline{\overline{⟨M_{1}, M_{2}⟩}}^{♯} =^{def} (let x_{1}=R(\overline{\overline{M}}^{♯}) in (let x_{2}=R(\overline{\overline{M_{2}}}^{♯}) in E⟨x_{1}, x_{2}⟩))

A product type, σ × τ is interpreted as the following type set

⟦σ × τ⟧ =^{def} {E⟨V, W ⟩ | E(V) ∈ ⟦σ⟧ and E(W) ∈ ⟦τ⟧}.

The definition of the retraction functions i and j is extended to product types to be

j_{σ×τ} =^{def} λx.⟨j_{σ}(π_{1}(x)), j_{τ}(π_{2}(x))⟩,

and

i_{σ×τ} =^{def} λx.⟨i_{σ}(π_{1}(x)), i_{τ}(π_{2}(x))⟩.

It is easy to see that i_{σ×τ}(V) and j_{σ×τ}(V) are values for any value V. Moreover, we can compute

j_{σ×τ} ∘ i_{σ×τ} =

= λx.⟨j_{σ}(π_{1}(x)), j_{τ}(π_{2}(x))⟩ ∘ λx.⟨i_{σ}(π_{1}(x)), i_{τ}(π_{2}(x))⟩  by defn.
= λx.⟨j_{σ}(π_{1}⟨i_{σ}(π_{1}(x)), i_{τ}(π_{2}(x))⟩), j_{τ}(π_{2}⟨i_{σ}(π_{1}(x)), i_{τ}(π_{2}(x))⟩)⟩ by (β_{v})
= λx.⟨j_{σ}(i_{σ}(π_{1}(x))), j_{τ}(i_{τ}(π_{2}(x)))⟩  by (×.β)
= λx.⟨π_{1}(x), π_{2}(x)⟩  by Lemma 1.4.2
= λx.x  by (×.η)

It remains to show that the rules (× E) and (× I) preserve properties (S.1) and (S.2) of Lemma 1.5.10. To do so we first prove the following results.

Lemma 1.9.6. Let M and N be terms such that M ε ⟦σ⟧ and N ε ⟦τ⟧. Then,

(let x=R(M) in (let y=R(N) in E⟨x, y⟩)) ε ⟦σ × τ⟧.

Proof: By assumption M = (let x_{1}=P_{1} in E(V_{1})) and N = (let x_{2}=P_{2} in E(V_{2})) for some E(V_{1}) ∈ ⟦σ⟧ and E(V_{2}) ∈ ⟦τ⟧. Therefore,

(let x=R(M) in (let y=R(N) in E⟨x, y⟩)) =
= (let x=R(let x_{1}=P_{1} in E(V_{1})) in
(let y=R(let x_{2}=P_{2} in E(V_{2})) in E⟨x, y⟩)) by assumption

       = (let x=(let x_{1}=P_{1} in V_{1}) in

(let y=(let x_{2}=P_{2} in V_{2}) in E⟨x, y⟩))  by (C-appl.1) and (r-e)

       = (let x_{1}=P_{1} in (let x=V_{1} in

(let x_{2}=P_{2} in (let y=V_{2} in E⟨x, y⟩))))  by (assoc)
= (let x_{1}=P_{1} in (let x_{2}=P_{2} in E⟨V_{1}, V_{2}⟩))  by (C-let.1),

and by the definition of ⟦σ × τ⟧, E⟨V_{1}, V_{2}⟩ ∈ ⟦σ × τ⟧.

Lemma 1.9.7. If M is such that M ε ⟦σ_{1} × σ_{2}⟧ then E(π_{i}(R(M))) ε ⟦σ_{i}⟧.

Proof: By assumption M ε ⟦σ_{1} × σ_{2}⟧, so for some E(V_{1}) ∈ ⟦σ_{1}⟧ and E(V_{2}) ∈ ⟦σ_{2}⟧, M = (let x=P in E⟨V_{1}, V_{2}⟩). Therefore,

E(π_{i}(R(M))) = E(π_{i}(R(let x=P in E⟨V_{1}, V_{2}⟩))) by assumption
= (let x=P in E(π_{i}(R(E⟨V_{1}, V_{2}⟩)))) by (C-appl.1)
= (let x=P in E(π_{i}⟨V_{1}, V_{2}⟩))  by (r-e)
= (let x=P in E(V_{i}))  by (×.β),

and E(V_{i}) is in ⟦σ_{i}⟧ by assumption. Now we are ready to extend the proof of Lemma 1.5.10 to product types. Proof: (Extending the proof of Lemma 1.5.10.) Case (× E): Assume ρ satisfies Γ and Γ ▷_{cp×} M: σ_{1} × σ_{2}, so that Γ ▷_{cp×} π_{i}(M): σ_{i}. Then by induction hypothesis, ρ\overline{\overline{M}}^{♯} ε ⟦σ_{1} × σ_{2}⟧. By definition ρ \overline{\overline{π_{i}(M)}}^{♯} = ρ(E(π_{i}(R(\overline{\overline{M}}^{♯})))), so by Lemma 1.9.7, ρ \overline{\overline{π_{i}(M)}}^{♯} ε ⟦σ_{i}⟧. This proves (S.1). To show (S.2) compute

j_{σ_{i}}(R(ρ \overline{\overline{π_{i}(M)}}^{♯})) = j_{σ_{i}}(R(ρ(E(π_{i}(R(\overline{\overline{M}}^{♯}))))))  by defn.
= j_{σ_{i}}(R(E(π_{i}(R(ρ\overline{\overline{M}}^{♯})))))  by defn. of subst.
= j_{σ_{i}}(R(E(π_{i}(R(let x=P in E⟨V_{1}, V_{2}⟩))))) by assumption
= (let x=P in j_{σ_{i}}(R(E(π_{i}(R(E⟨V_{1}, V_{2}⟩)))))) by (C-appl.1)
= (let x=P in j_{σ_{i}}(V_{i}))  by (r-e) and (×.β)
= (let x=P in π_{i}⟨j_{σ_{1}}(V_{1}), j_{σ_{2}}(V_{2})⟩)  by (×.β)
= π_{i}(let x=P in ⟨j_{σ_{1}}(V_{1}), j_{σ_{2}}(V_{2})⟩)  by (C-appl.1)
= π_{i}(let x=P in j_{σ_{1}×σ_{2}}⟨V_{1}, V_{2}⟩)  by defn. of j_{σ_{1}×σ_{2}}
= π_{i}(j_{σ_{1}×σ_{2}}(R(let x=P in E(⟨V_{1}, V_{2}⟩))))  by (C-appl.1) and (r-e)
= π_{i}(j_{σ_{1}×σ_{2}}(R(ρ\overline{\overline{M}}^{♯})))  by assumption
= π_{i}(ρ′M)  by ind. hyp.
= ρ′ π_{i}(M)  by defn. of subst.,

where ρ′(x) = j_{σ}(ρ(x)) for each x: σ ∈ Γ. Case (× I): Assume Γ ▷_{cp×} M: σ and Γ ▷_{cp×} N: τ so that Γ ▷_{cp×} ⟨M, N⟩: σ × τ. By definition ρ \overline{\overline{⟨M, N⟩}}^{♯} = (let x=R(ρ\overline{\overline{M}}^{♯}) in (let y=R(ρ\overline{\overline{N}}^{♯}) in E⟨x, y⟩)), and by induction hypothesis, for ρ that satisfies Γ, ρ\overline{\overline{M}}^{♯} ε ⟦σ⟧ and ρ\overline{\overline{N}}^{♯} ε ⟦τ⟧, so by Lemma 1.9.6, ρ \overline{\overline{⟨M, N⟩}}^{♯} ε ⟦σ × τ⟧.

64 CHAPTER 1. RETRACTION APPROACH TO CPS TRANSFORM

This establishes (S.1). Again, (S.2) follows by computation.

j_{σ×τ} (R(ρ \overline{\overline{⟨M, N⟩}}^{♯})) =

= j_{σ×τ} (R(let x=R(ρ\overline{\overline{M}}^{♯}) in (let y=R(ρ\overline{\overline{N}}^{♯}) in E⟨x, y⟩))) by defn.
= j_{σ×τ} (R(let x=R(let x_{1}=P_{1} in E(V_{1})) in
(let y=R(let x_{2}=P_{2} in E(V_{2})) in E⟨x, y⟩)))  by ind. hyp. (S.1)
= j_{σ×τ} (R(let x=(let x_{1}=P_{1} in V_{1}) in
(let y=(let x_{2}=P_{2} in V_{2}) in E⟨x, y⟩)))  by (C-appl.1) & (r-e)
= j_{σ×τ} (R(let x_{1}=P_{1} in (let x_{2}=P_{2} in E⟨V_{1}, V_{2}⟩)))  by (assoc)

and (C-let.1)

= (let x_{1}=P_{1} in (let x_{2}=P_{2} in j_{σ×τ} ⟨V_{1}, V_{2}⟩))  by (C-appl.1) & (r-e)
= (let x_{1}=P_{1} in (let x_{2}=P_{2} in ⟨j_{σ}(V_{1}), j_{τ} (V_{2})⟩))  by defn of j_{σ×τ}, (β_{v})

& (×.β)

= ⟨(let x_{1}=P_{1} in j_{σ}(V_{1})), (let x_{2}=P_{2} in j_{τ} (V_{2}))⟩  by (C-let.1)

& (let.×)

= ⟨j_{σ}(R(let x_{1}=P_{1} in E(V_{1}))), j_{τ} (R(let x_{2}=P_{2} in E(V_{2})))⟩ by (r-e) & (C-appl.1)
= ⟨j_{σ}(R(ρ\overline{\overline{M}}^{♯})), j_{τ} (R(ρ\overline{\overline{N}}^{♯}))⟩  by ind. hyp. (S.1)
= ⟨ρ′M, ρ′N⟩  by ind. hyp. (S.2)
= ρ′⟨M, N⟩  by defn. of subst.

The extension of the Retraction Theorem for the CPS transform can be done in a similar way. The CPS transform of pairs and projections is defined to be

\overline{π_{i}(M)} =^{def} λk.\overline{M} (λm.k π_{i}(m))
\overline{⟨M, N⟩} =^{def} λk.\overline{M} (λm.\overline{N} (λn.k ⟨m, n⟩)).

Using relation ε^{K} instead of ε and terms E^{K} and R^{K} instead of E and R, one can extend Lemma 1.5.17 and the Retraction Theorem for the CPS transform to λ_{cp×}.

1.10 Acknowledgments

I’d like to thank to my advisor Albert Meyer for lengthy discussions about this work, and to Prof. Mitch Wand for helpful comments. I’d also like to thank Jens Palsberg and Jon Riecke for the discussions and comments on some issues in the early stages of this work.

Chapter 2

Another Look at “Theorems for Free!”

Abstract: We reexamine Wadler’s “free theorems” — theorems about polymorphic functions derivable from the type of the function — in an extension of Mairson’s syntactic treatment of logical relations. Logical relations are defined as formulas in second (and higher) order logic over untyped lambda terms, from which we can instantiate equations involving a given term. As a consequence we can formulate a free theorem as an equation schema, each instance of which is provable by convertibility, given typing conditions on the terms involved are met. In our framework datatypes are represented as free algebras generated by constants, and we define sufficient conditions which a representation of a datatype must satisfy to preserve free theorems. As a special case we prove examples of free theorems, as equations by convertibility, using Böhm-Berarducci representation of datatypes.

2.1 Introduction

What are “free theorems”? The purpose of using types in programming languages is to avoid certain kinds of errors. For example, in a well typed program a function cannot be applied to an argument of a wrong type. Thus, types give us certain guarantees about the behavior of well typed programs. What Wadler, in his “Theorems for Free!” paper [Wad89], points out is that not only we know that well type programs will not have any run-time type errors, but we can also infer, from the type of a program, certain identities that the program must satisfy. To quote Wadler:

Write down a definition of a polymorphic function on a piece of paper. Tell me its type, but be careful not to let me see the function’s definition. I will tell you a theorem that the function satisfies.

Such “free theorems” are all instances of parametric behavior of polymorphic functions in a model of polymorphic lambda calculus. In this paper, we propose a syntactic treatment of free theorems inspired by the types-as-propositions paradigm, extending the one developed by Mairson [Mai91]. We develop a framework, in which parametric behavior of polymorphic lambda terms is captured by formulae of type theory. This setting allows us to present the free theorems as metatheorems about convertibility. In other words, a free theorem is an equation schema that is provable by convertibility whenever certain typing assumptions about the terms involved hold. For example, the famous “map theorem” can be restated as follows. Let \underline{List(t)} abbreviate the type of lists ∀s.(t→s→s)→s→s, and write \underline{map} be the map function on lists: λflcn.(l (λxycn.(c (f x) (y c n))) n).^{1}

Proposition 2.1.1. Assume M is a closed pure λ-term of type

∀st.(s→t)→(\underline{List(s)})→(\underline{List(t)}),

and let L be a pure λ-term such that

\{x_{1}: r, … x_{k}: r\} ▷ L: (\underline{List(r)}).

Then equation,

(\underline{map} f (M (λx.x) L)) = (M f L).

is provable by convertibility in βη-theory.

This theorem, as well as other examples in [Wad89], are all considered manifestations of parametric polymorphism. Intuitively, a polymorphic function is called parametric if it can be described as having a uniform algorithm that works for all types [Str67]. There have been numerous attempts to formulate this notion, for example [Rey83, BFSS90, MR91, Mai91], and in each of these formulations, the parametric functions have the expected properties. Even though there doesn’t seem to be a general agreement on the “right” definition of parametricity, it is agreed that the polymorphic λ-terms denote parametric functions.

To capture the parametric behavior of lambda terms, we use a form of logical relations defined as formulae of type theory. In a way, our formulation of logical relation is an extension of types-as-propositions paradigm. For instance, the proposition (in the type theory) ∀ST.S ⊃ T, corresponding to type σ ≡ ∀st.s→t, can be considered a null-ary logical relation. Unary logical relation, R^{σ}(x), is defined to be the proposition ∀ST.∀y.T (y) ⊃ S(x y) of the type theory over lambda terms. Similarly, one can define logical relations of any arity. For this definition of logical relations we prove the The Fundamental Theorem of Logical Relations which, informally, states that if a term M has type σ, then the proposition R^{σ}(M) is provable in type theory. Moreover, by proper instantiations of the universally quantified variables in the logical relation, R^{σ}(M), we derive, in type theory, an equation involving the term M. By soundness of type theory and completeness of a lambda theory we conclude that the type theory is conservative over equational logic of the lambda theory, so the derived equation about M, in fact, holds by convertibility.

An interesting point in the syntactic version of free theorems is that we obtain an equation, about a term M, that holds by convertibility without actually knowing what M is. Of course, any derivation (by convertibility) of the resulting equality would depend on the structure of the term involved. However, in the types-as-propositions paradigm a term corresponds to a proof of the proposition corresponding to its type, and the derivation by convertibility corresponds to the normalization of the proof. Thus, it is not surprising, that from the proposition corresponding to the type of a term, one can extract the computational content corresponding to the derivation of an equation by convertibility.

1The type of lists and the map function are derived from the Böhm-Berarducci representation of lists discussed in more detail in Section 2.5.

In proving free theorems where elements of an inductive data type, such as lists, are used, as Mairson points out, the apparent absence of induction looks suspicious. Wadler defines the logical relation corresponding to lists to say that two lists are related if they are of the same length and the corresponding elements of the lists are related. This definition relies on our intuitive understanding what lists are, and assumes that, in the model in which he studies the free theorems, lists behave according to our intuition. On the other hand, in the syntactic formulation of free theorems, we need to be precise how we represent datatypes such as lists. For instance, we can use the Böhm-Berarducci [BB85] encoding of lists in polymorphic lambda calculus similar to the encoding of natural numbers as Church numerals. Then, the type of lists yields a logical relation quite different from the induction axiom corresponding to Wadler’s semantic interpretation of the logical relation on lists. It seems that the free theorems require the induction axiom, and the question is whether the free theorems hold for Böhm-Berarducci lists, without using induction. To answer this question, rather than asking if Böhm-Berarducci lists are “inductive”, we reformulate the question and ask what is a correct way to represent inductive datatypes such as lists.

To answer the question we develop a framework where datatypes are represented as free algebras generated by a set of constants. For example, lists are generated by constants nil: List(t) and cons: t→List(t)→List(t). In this framework logical relations corresponding to inductive datatypes are the induction axioms, from which free theorems follow easily. Then we define a general notion of a representation (of generators of a datatype), and define sufficient conditions that allows us to translate the free theorems. In particular, we show that the Böhm-Berarducci representation satisfies the conditions and the free theorems hold when Böhm-Berarducci encodings of lists are used. This also answers Mairson’s question whether induction is necessary in proving the free theorem when Böhm-Berarducci lists are used. To be precise we should say that the explicit use of induction in not necessary. Implicitly, induction is “contained” in the type of Böhm-Berarducci lists.

2.2 Definitions

In this section we define the main notions used in the paper. We assume the reader is familiar with untyped λ-calculus and elementary concepts such as free and bound variables, substitution, parallel substitution, as well as, (α), (β) and (η) axiom schemes. For precise treatment of these notions one is referred to [Bar84].

2.2.1 Untyped λ-calculus and λ-theories

We work with standard definition of the untyped λ-calculus with constants. Let C_{Λ} be a set of constants and write Λ(C_{Λ}) to denote the set of λ-terms over constants in C_{Λ} and an infinite set of λ-variables. We do not distinguish between α-equivalent λ-terms. We use lower-case letters towards the end of the alphabet to denote λ-variables, and upper-case letters, M, N, etc. to denote arbitrary λ-terms. Following [Bar84] we write Λ^{0}(C_{Λ}) for the set of all closed λ-terms over constants in C_{Λ}. We will use parentheses freely to make expressions more readable, and in doing so we assume application of terms associates to the left.

A set, 𝔗𝔥, of equations between λ-terms is called λ-congruence if it contains all instances of axiom (ref) and is closed under the rules given in Table 2.1. If a λ-congruence also contains

M = M  (ref)

\frac{M = N}{N = M}  (sym)

\frac{M = P, P = N}{M = N}  (trans)

\frac{M = P, N = Q}{(M N) = (P Q)}  (cong)_{\frac{M = N}{λx.M = λx.N}  (ξ)}

Table 2.1: Inference rules of a λ-congruence.

all instances of (β), it is a λ-theory. If a theory, 𝔗𝔥, contains an equation M = N, we say M = N is provable by convertibility and write 𝔗𝔥 ⊢_{λ} M = N. In particular if 𝔗𝔥 is the minimal λ-theory containing (η), and 𝔗𝔥 ⊢_{λ} M = N, we write M =_{βη} N.

2.2.2 Type Inference System F_{ω}+𝔗𝔥

Let 𝔗𝔥 be a λ-congruence. The type inference system F_{ω}+𝔗𝔥 is a version of Girard’s system F_{ω} [Gir72]. In F_{ω}+𝔗𝔥 we use implicit typing in the style of Curry, and add an extra typing rule (term-cong) [Mit88]. Moreover, we enrich the set of type constructors with a set of type constructor constants.

The set of type constructors is defined as simply kinded λ-calculus, over a set of constant type constructors, with base kind ⋆. More precisely, we have that ⋆ is a kind, and if κ′ and κ are kinds, then so is κ′⇒κ. For each kind κ there are infinitely many variables t^{κ} of that kind. Let C_{T} be a set of constant type constructors, each assigned a kind. We write c^{κ} to denote a constant type constructor of kind κ. The set T (C_{T}), of type constructors over constants in C_{T} is defined inductively.

• A constant c^{κ} in C_{T} is a type constructor of kind κ.

• A type constructor variable t^{κ} is a type constructor of kind κ.

• If σ and τ are type constructors of kind ⋆, then σ→τ is a type constructor of kind ⋆.

• If σ is a type constructor of kind ⋆, then ∀t^{κ}.σ is a type constructor of kind ⋆.

• If σ is a type constructor of kind κ′⇒κ and τ is a type constructor of kind κ′, then (σ τ) is a type constructor of kind κ.

• If σ is a type constructor of kind κ, then λt^{κ′}.σ is a type constructor of kind κ′⇒κ.

We define equality between type constructors of the same kind by the usual βη-equational rules for simply typed lambda calculus. We write σ =_{λ} σ′ if σ and σ′ can be proven equal using these equational rules. Type constructors of kind ⋆ are called λ-types, or simply types.

As with the λ-terms, we will use parentheses freely to make type constructors more readable. In doing so, we assume the application associates to the left and the exponentiation operator → associates to the right, so that σ→(τ→υ) can be written as σ→τ→υ. We will also omit the kind information form type constructors, when it is clear from the context or irrelevant.

An expression of the form M: σ, where M is a λ-term and σ is a type is called a type assertion. A set of type assertions, Γ = {x_{1}: σ_{1}, …, x_{k}: σ_{k}} where no variable occurs twice in Γ is called a typing hypothesis. We write Γ, x: σ for the set Γ ∪ {x: σ}, assuming x does not occur in Γ. A typing sequent is a formula of the form Γ ▷ M: σ, where Γ is a typing hypothesis, M is a λ-term and σ is a type.

Let Type be a partial function, assigning types to constants in C_{Λ}. Write Type(g) = σ_{g} to say that Type(g) is defined and equal to σ_{g}. Then, the inference rules for proving typing sequents in F_{ω}+𝔗𝔥 are given in Table 2.2 below. If a sequent Γ ▷ M: σ is derivable using

Γ, x: σ ▷ x: σ  (var)

\frac{Γ ▷ M: σ→τ, Γ ▷ N: σ}{Γ ▷ (M N): τ}  (app)

\frac{Γ, x: σ ▷ M: τ}{Γ ▷ (λx.M): σ→τ}  (abs)

\frac{Γ ▷ M: ∀t.τ}{Γ ▷ M: ((λt.τ) σ)}  (inst)

\frac{Γ ▷ M: σ}{Γ ▷ M: ∀t.σ} ,  if t ∉ FV(Γ)  (gen)

\frac{Γ ▷ M: σ}{Γ ▷ M: τ} ,  if σ =_{λ} τ  (type-cong)

Γ ▷ g: σ_{g},  if g ∈ C_{Λ} and Type(g) = σ_{g}  (const)

\frac{Γ ▷ N: σ}{Γ ▷ M: σ} ,  if N = M ∈ 𝔗𝔥  (term-cong)

Table 2.2: Type inference system F_{ω}+𝔗𝔥.

these rules, we write 𝔗𝔥 ⊢ Γ ▷ M: σ. If the rule (term-cong) was not used in the derivation, we write ⊢ Γ ▷ M: σ, or simply Γ ▷ M: σ. We will also abbreviate 𝔗𝔥 ⊢ ∅ ▷ g: σ_{g} by g: σ_{g} when g is in C_{Λ} and Type(g) = σ_{g}.

Note that if σ_{g} is not closed, since ⊢ ∅▷g: σ_{g}, then also ⊢ ∅▷g: ∀t⃗.σ_{g}, where t⃗ is a sequence of all free type constructor variables in σ_{g}. Thus, without loss of generality, we may assume that each σ_{g} is closed. If c is a constant type constructor and t_{1}, … t_{k} are type constructor variables of appropriate kinds so that (c t_{1} ⋯ t_{k}) is of kind ⋆, type (c t_{1} ⋯ t_{k}) is called a base type.

Given a set C_{Λ} of constant λ-terms, a set C_{T} of constant type constructors, a partial function Type typing constant λ-terms and a λ-congruence 𝔗𝔥, the tuple ℭ = (C_{Λ}, C_{T} , Type, 𝔗𝔥) will simply be called a calculus.

2.2.3 Data Structures

In this paper a data structure is a free algebra over lambda terms defined by a signature ({c_{1}, …, c_{k}}, {g_{1}: ϕ_{1}, …, g_{l}: ϕ_{l}}) where c_{1}, …, c_{k} are type constructor constants in C_{T}, and g_{1}, …, g_{l} are constants in C_{Λ}, called the generators of the data structure. We assume the function Type is defined on all g_{i}’s and Type(g_{i}) = ϕ_{i} for all i. We also assume that c_{1}, …, c_{k} are the only constant type constructors occurring in ϕ_{i}’s.

Example 2.2.1. The data structure representing lists is given by the signature

L =^{def} ({List^{⋆⇒⋆}}, {cons: ∀t.t→(List t)→(List t), nil: ∀t.(List t)}).

The lists of type (List σ) are terms of the form (cons N_{1} (⋯ (cons N_{k} nil) ⋯)), where N_{i}’s are lambda terms of type σ.

Example 2.2.2. Natural numbers can be defined with the signature

                   N =^{def} ({Nat^{⋆}}, {succ: Nat→Nat, zero: Nat}).

Natural number k corresponds to the k-fold application of succ to zero.

Let ({c_{1}, … c_{m}}, {g_{1}: ϕ_{1}, … g_{n}: ϕ_{n}}) be a signature of a data structure such that each c_{i} is of kind ⋆⇒ ⋯ ⇒⋆ and each ϕ_{i} is of the form ∀t⃗.σ_{1}→ ⋯ →σ_{r}→(c t_{1} ⋯ t_{k}) with σ_{i}’s either type variables or base types. Call such a data structure simple. This class of data structures is sufficient to express a large set of commonly used datatypes, such as list, trees, natural numbers, etc.

If ({c_{1}, …, c_{k}}, {g_{1}, …, g_{l}}) and ({c′_{1}, …, c′_{m}}, {g′_{1}, …, g′_{n}}) are two signatures of different data structures, we always assume that {c_{1}, …, c_{k}} ∩ {c′_{1}, …, c′_{m}} = ∅ = {g_{1}, …, g_{l}} ∩ {g′_{1}, …, g′_{n}}.

2.2.4 Programs over λ-terms

Let f be a constant in C_{Λ}, that is not a generator of any data structure. A program for f is a set, 𝔓_{f}, of equations between λ-terms. Intuitively, equations in 𝔓_{f} define a function denoted by f. For example, if f denotes a function f, from natural numbers to natural numbers, the equations in 𝔓_{f} will correspond to the inductive definition of f.

We say that the calculus contains a program 𝔓_{f} for f, if 𝔓_{f} ⊆ 𝔗𝔥 and f ∈ C_{Λ}. Such a constant f is called a function symbol. In general we will assume that constants in C_{Λ} are either generators of a data structure or function symbols.

Example 2.2.3. Given the constructors cons and nil, as in the above example, the program 𝔓_{map} for map is given by the following set of equations:

𝔓_{map} =^{def} {(map f nil) = nil, (map f (cons x t)) = (cons (f x) (map f t))}.

Example 2.2.4. Given the data structure N of natural numbers, one can define addition by the following program:

𝔓_{add} =^{def} {(add zero x) = x, (add (succ x) y) = (succ (add x y))}

2.2.5 Type Theory over λ-terms

Type theory is a generalization of the minimal second order logic over lambda terms^{2} to include higher-order predicates. We define the language of type theory with base logical types ı and o. Therefore, a logical type is either ı, o, or κ_{1}⇒κ_{2}, whenever κ_{1} and κ_{2} are logical types. The terms of logical type ı will be λ-terms and the logical type o will represent truth values. We have an infinite supply of variables of each logical type. Variables of type κ are denoted X^{κ}. We do not distinguish λ-variables from variables of type ı, and use lowercase letters to range over either. The terms of type theory are defined inductively.

• Every variable X^{κ} is a term of type κ.

• If M is a λ-term then M is a term of type ı.

• If M and N are terms of type ı then M = N is a term of type o.

• If P is a term of type κ′⇒κ and Q is a term of type κ′ then (P Q) is a term of type κ.

• If P is a term of type κ then ΛX^{κ′}.P is a term of type κ′⇒κ.

• If P and Q are terms of type o then P ⊃ Q is a term of type o.

• If P is a term of type o then ∀X^{κ}.P is a term of type o.

We assume the usual βη-equality between terms of type theory and write P =_{Λ} Q if terms P and Q of the same type can be proven equal with respect to “=_{Λ}”. This equality should not be confused with equality “=” between λ-terms. The equality “=_{Λ}” is defined in terms of (β), (η), (ξ), etc. defined w.r.t. Λ and not λ. Moreover, the equality “=_{Λ}” is used to denote equality of terms of type theory, and is not a part of the language of the type theory, while the equality “=” is used to form the terms of the type theory of the form M = N.

Notation. We reserve the letters M, N, L and K to range over lambda terms, and letters P and Q to range over terms of type theory. Letters X, Y and Z, as well as S and T, will range over variables of type theory of any logical type, and specifically for the variables of logical type ı, we will use lower case x, y, z, etc. When writing formulas of type theory, we use parentheses freely, and assume application associates to the left and implication associates to the right. If P is a term of type theory of logical type ı⇒o, and M is a lambda term, we will write P (M) for the application (P M). Similarly, if P is of logical type ı⇒ı⇒ ⋯ ⇒ı⇒o, and M_{i} are lambda terms, we write P (M_{1}, M_{2}, …, M_{k}) for the application (P M_{1} M_{2} ⋯ M_{k}).

2By the minimal logic, we mean the fragment of the logic that contains only implication and universal quantification.

Let Γ be a set of terms of type o. For a term P of type o we write Γ ⊢_{T T} P, to say that P is provable in type theory from assumptions in Γ, if the sequent Γ ⊢ P can be derived using the rules of inference given in Table 2.3. Note that P and Q range over terms of type theory of type o, M, N, L and K range over lambda terms, and X ranges over variables of any logical type, while x ranges over λ-variables (i.e. variables of logical type ı). The

Γ, P ⊢ P  (Id)

\frac{Γ, P ⊢ Q}{Γ ⊢ P ⊃ Q}  (⊃ I)

\frac{Γ ⊢ P ⊃ Q, Γ ⊢ P}{Γ ⊢ Q}  (⊃ E)

\frac{Γ ⊢ P}{Γ ⊢ ∀X.P} ,  if X ∉ FV(Γ)  (∀ I)

\frac{Γ ⊢ ∀X.P}{Γ ⊢ P [Q/X]}  (∀ E)

\frac{Γ ⊢ P}{Γ ⊢ Q} ,  if P =_{Λ} Q  (=_{Λ})

\frac{Γ ⊢ P [M/x], Γ ⊢ M = N}{Γ ⊢ P [N/x]}  (Cong)
Γ ⊢ M = M  (ref)

\frac{Γ ⊢ M = N}{Γ ⊢ N = M}  (sym)

\frac{Γ ⊢ M = N, Γ ⊢ N = L}{Γ ⊢ M = L}  (trans)

\frac{Γ ⊢ M = N, Γ ⊢ K = L}{Γ ⊢ (M K) = (N L)}  (cong)

\frac{Γ ⊢ M = N}{Γ ⊢ λx.M = λx.N} ,  if x ∉ FV(Γ) (ξ)

Table 2.3: Inference rules of type theory.

set of equations provable from assumptions in Γ using the above rules is a λ-congruence. Moreover, the rules of type theory only prove equations between lambda terms, that are derivable by convertibility form the equations in Γ. We prove this conservativity result in the next section.

Remark. We have identified variables of type theory of logical type ı and lambda variables. While, from the perspective of the interpretation described in the next section, it is correct to treat the two kinds of variables the same way, we need to clarify a few points to avoid possible confusion. Lambda variables are treated differently in the context of type theory than in the context of equational logic. It helps one’s intuition to think of lambda variables in the context of type theory as metavariables. For example, consider the sequent x = λy.y ⊢ (x z) = z. In the context of a lambda theory, this sequent conveys little information, since it says that in a theory in which x = λy.y, which is necessarily inconsistent, equation (x z) = z is provable. On the other hand the same sequent, in the context of type theory makes perfect sense, and it says that x = λy.y implies (x z) = z. This apparent paradox comes from the fact that in equational theory, there is no way to express implication.

2.2.6 Semantics of Type Theory

In this paper, we only consider a special class of models of the type theory. Observe that the type theory is essentially a simply typed lambda calculus. Thus, we can use the same construction as in a set-theoretic model of simply typed lambda calculus to construct a model of type theory. More precisely, let the set I be an environment model of untyped λ-calculus (as defined in [Mey82]) and let O be the two element set {True, False}. Logical types are given the following interpretation:

⟦o⟧ =^{def} O
⟦ı⟧ =^{def} I
⟦κ_{1}⇒κ_{2}⟧ =^{def} ⟦κ_{2}⟧^{⟦κ_{1}⟧}

To give an interpretation of terms we define an environment to be a function mapping variables of type κ to ⟦κ⟧. Given an environment, ρ, the interpretation function ⟦·⟧ assigning meaning to the terms of type theory is defined inductively:

⟦X^{κ}⟧ρ =^{def} ρ(X^{κ})
⟦M⟧ρ =^{def} ⟦M⟧_{I}ρ, if M is a λ-term and ⟦M⟧_{I}ρ is

the interpretation of M in I

⟦M = N⟧ρ =^{def} True if ⟦M⟧_{I}ρ = ⟦N⟧_{I}ρ and False otherwise
⟦(P Q)⟧ρ =^{def} ⟦P ⟧ρ(⟦Q⟧ρ)
⟦ΛX^{κ}.P ⟧ρ =^{def} function f such that for all e ∈ ⟦κ⟧, f(e) = ⟦P ⟧ρ[e/X^{κ}]
⟦P ⊃ Q⟧ρ =^{def} True iff ⟦P ⟧ρ = False or ⟦Q⟧ρ = True
⟦∀X^{κ}.P ⟧ρ =^{def} True iff for all e ∈ ⟦κ⟧, ⟦P ⟧ρ[e/X^{κ}] = True

In order for this interpretation to be well defined, one must have the meaning of all λ-terms in Λ(C_{Λ}) defined in I. We will always assume this is so.

Any model of type theory is completely determined by the underlining model of the untyped lambda calculus I. Therefore we will speak of the meaning of a term P in I, but with the understanding that P is interpreted in the model of type theory defined by the model I.

Let I be model of the untyped lambda calculus, and let ρ be an environment. If P is a term of type o, ρ is said to satisfy P, if ⟦P ⟧ρ = True. A sequent Γ ⊢ P is said to be valid in I, written Γ ⊧_{I} P, if for every ρ that satisfies all terms in Γ, ρ satisfies P.

The inference rules of type theory are sound for the class of models we are considering. This result follows easily by showing that each inference rule in Table 2.3 preserves validity.

Lemma 2.2.5 (Soundness). Let I be a model of the untyped lambda calculus. Then,

if Γ ⊢_{T T} P then Γ ⊧_{I} P.

Even though we lack the completeness result for the type theory, one can use semantic reasoning in type theory to prove that an equation between lambda terms holds by convertibility.

Lemma 2.2.6. Let 𝔗𝔥 be a λ-theory. If, for every model I, 𝔗𝔥 ⊧_{I} M = N then 𝔗𝔥 ⊢_{λ} M = N. In particular, if I is the term model, consisting of 𝔗𝔥-equivalence classes of lambda terms, and 𝔗𝔥 ⊧_{I} M = N, then M = N is provable by convertibility from equations in 𝔗𝔥.

Proof: To say that 𝔗𝔥 ⊧_{I} M = N in every model I, is to say that M = N is true in every interpretation satisfying equations in 𝔗𝔥. Therefore, by the completeness of λconvertibility [Mey82], M = N is provable by convertibility, i.e. 𝔗𝔥 ⊢_{λ} M = N.

Theorem 2.2.7. Type theory is conservative over λ-convertibility, that is

𝔗𝔥 ⊢_{T T} M = N iff 𝔗𝔥 ⊢_{λ} M = N.

Proof: Since 𝔗𝔥 ⊢_{T T} M = N, by soundness of the inference rules of type theory, for any model I, 𝔗𝔥 ⊧_{I} M = N, and by the above lemma, 𝔗𝔥 ⊢_{λ} M = N.

2.2.7 Models of Type Inference

To define a model of type inference, one needs to define how to interpret terms and types, as well as define a notion of type sets, relating the two interpretations, so that if M is a term of type σ, the meaning of M is an element of the type set corresponding to σ. The type inference models of the second order polymorphic lambda calculus have been studied in detail by Mitchell [Mit88], and his definitions easily generalize to system F_{ω}+𝔗𝔥. We summarize the main definitions.

A type structure, 𝔗, is a set theoretic model of simply typed lambda calculus, containing special elements →^{𝔗} and ∀^{𝔗}. More precisely, 𝔗 consists of a family of sets, {U_{κ}}, indexed by kinds. We interpret type constructors of kind κ as elements of set U_{κ}. We have →^{𝔗} ∈ U_{⋆⇒⋆⇒⋆} and ∀^{𝔗} ∈ U_{(⋆⇒⋆)⇒⋆}. Given a mapping, η, from type constructor variables of kind κ to U_{κ}, define the interpretation of functional and universal types to be

⟦σ→τ⟧η = →^{𝔗}(⟦σ⟧η)(⟦τ⟧η) and ⟦∀t.σ⟧η = ∀^{𝔗}(⟦λt.σ⟧η).

Let D be a model of the untyped lambda calculus. Then, we define type sets using the subset function that, to each element, a, in U_{⋆} assigns a subset, D_{a}, of D. In addition, we require that the type sets satisfy the following conditions:^{3}

D_{a→b} = {d | d · D_{a} ⊆ D_{b}}  (Arrow)

D_{∀f} = ⋂_{a∈U_{⋆}} D_{f(a)}.  (ForAll)

We say that a type structure 𝔗, a model of untyped lambda calculus D, and a subset function define a model of type inference.

3We assume D is a model of βη calculus, and thus (Arrow) simplifies conditions (Arrow.1) and (Arrow.2)

in [Mit88]

2.2.8 Logical Relations

Curry-Howard isomorphism gives a bijective correspondence between typed lambda calculus and propositional logic. In this isomorphism, polymorphic types correspond to propositions of higher order logic, and terms correspond to proofs. For example, the type ∀t.t→t correspond to proposition ∀T.T ⊃ T, and the identity function λx.x corresponds to a proof of that proposition. The syntactic version of logical relation represents, in a way, a generalization of this correspondence. In our example, the proposition ∀T.T ⊃ T is a null-ary logical relation corresponding to type ∀t.t→t. We define unary logical relation, R^{∀t.t→t}(f), to be ∀T.∀x.T (x) ⊃ T (f(x)), and a binary version R^{∀t.t→t}(f_{1}, f_{2}), to be ∀T.∀x_{1}x_{2}.T (x_{1}, x_{2}) ⊃ T (f_{1}(x_{1}), f_{2}(x_{2})), etc.

Our definition of logical relations extends the one used by Mairson [Mai91] to type theory in order to accommodate higher order, as well as constant, type constructors of the type inference system F_{ω}+𝔗𝔥. For each type constructor σ, of kind κ, we define a term R^{σ} of type theory of logical type κ(κ), where κ is an injection from kinds to logical types defined inductively so that: κ(⋆) =^{def} ı⇒o and κ(κ′⇒κ) =^{def} κ(κ′)⇒κ(κ).

We also assume there is a bijection between type constructor variables and of kind κ and propositional variables of logical type κ(κ) that maps a variable t^{κ} to a propositional variable T^{κ(κ)}. We will write type constructors variables in lowercase, and use the same letters in uppercase to denote variables of type theory, that are uniquely determined by the above mentioned bijection. Given a sequence of type constructor variables t_{1}, …, t_{k}, we say the variables T_{1}, …, T_{k} correspond to variables t_{1}, …, t_{k}, and vice versa.

Using these conventions, for each type σ, we define the unary logical relation, R^{σ}, inductively as follows:

R^{t^{κ}}  =^{def} T^{κ(κ)}
R^{c}   =^{def} D_{c}, if c is in C_{T}
R^{(σ τ)} =^{def} (R^{σ} R^{τ})
R^{(λt.τ)} =^{def} ΛT.R^{τ}
R^{σ→τ} =^{def} Λf.∀x.R^{σ}(x) ⊃ R^{τ}(f x)
R^{∀t.σ} =^{def} Λx.∀T.R^{σ}(x)

In the above definition, for each c ∈ C_{T}, the term D_{c} is defined as in [Lei90]. Namely, let ({c_{1}, …, c_{m}}, {g_{1}: ϕ_{i}, …, g_{n}: ϕ_{n}}) be a signature of a data structure. Assume for j = 1, …, m, c_{j} is of kind κ_{j1}⇒ ⋯ κ_{jl_{j}}⇒⋆. Let c_{j} be a type variable of the same kind as c_{j}, and let ϕ̂ denote a type constructor obtained from ϕ by replacing all c_{j}’s by c_{j}’s. Let C⃗ be the sequence of variables of type theory corresponding to c_{1}, …, c_{m}. Let t_{j1}, …, t_{jl_{j}} be a sequence of fresh type constructor variables of kinds κ_{j1}, …, κ_{jl_{j}} and let T⃗_{j} be the corresponding sequence of variables of type theory. Then define

D_{c_{j}} =^{def} ΛT⃗_{j}.Λx.∀C⃗.Rϕ̂_{1}(g_{1}) ⊃ ⋯ ⊃ Rϕ̂_{n}(g_{n}) ⊃ (C_{j} T_{j1} ⋯ T_{jl_{j}})(x).

The definition of logical relations, in particular of D_{c_{j}}, is well defined, since all types ϕ̂_{i}, in the definition of D_{c_{j}} above, are pure.

Example 2.2.8. Let data structure B = ({Bool^{⋆}}, {true: Bool, false: Bool}). The logical relation corresponding to Bool is

R^{Bool} =^{def} Λx.∀P^{ı⇒o}.P (true) ⊃ P (false) ⊃ P (x).

Example 2.2.9. Recall the data structure N defining the natural numbers. The logical relation R^{Nat} is nothing but the Peano’s induction axiom:

Λx.∀P^{ı⇒o}.(∀y.P (y) ⊃ P (succ y)) ⊃ P (zero) ⊃ P (x).

Example 2.2.10. Consider the data structure L of lists defined in example 2.2.1. The logical relation R^{List} corresponding to the type constructor List is defined to be

ΛT^{ı⇒o}.Λz.∀P^{(ı⇒o)⇒ı⇒o} .∀S^{ı⇒o}(∀x.S(x) ⊃ ∀y.(P S)(y) ⊃ (P S)(cons x y)))
⊃ ∀S^{ı⇒o}.(P S)(nil)
⊃ (P T)(z).

The relation R^{(List t)}(z) is provably equivalent to a more familiar induction axiom

∀P.(∀xy.T (x) ⊃ P (y) ⊃ P (cons x y)) ⊃ P (nil) ⊃ P (z)

used in [Mai91].

The definition of unary logical relations, can be easily modified to obtain a definition of logical relations of any arity. Fix arity k ≥ 0, and let κ(⋆) =^{def} ı⇒ ⋯ ⇒ı⇒o (k ı’s). For higher kinds κ, let κ(κ) be defined as before. Then the k-ary logical relations are defined as follows:

R^{t^{κ}}  =^{def} T^{κ(κ)}
R^{c}   =^{def} D_{c}, for c ∈ C_{T}
R^{(σ τ)} =^{def} (R^{σ} R^{τ})
R^{(λt.τ)} =^{def} ΛT.R^{τ}
R^{σ→τ} =^{def} Λf^{(1)} ⋯ f^{(k)}.∀x^{(1)} ⋯ x^{(k)}.
R^{σ}(x^{(1)}, ⋯, x^{(k)}) ⊃ R^{τ}(f^{(1)}(x^{(1)}), ⋯, f^{(k)}(x^{(k)}))
R^{∀t.σ} =^{def} Λx^{(1)} ⋯ x^{(k)}.∀T.R^{σ}(x^{(1)}, ⋯, x^{(k)})

In the above definition D_{c} is defined using k-ary versions of R^{(·)}, and x^{(i)} and f^{(i)} denote distinct variables of type ı.

2.3 The Fundamental Theorem of Logical Relations

The Fundamental Theorem we prove in this section is a key tool in proving free theorems. As we explain in Section 2.4, free theorems about a term M, are instances of the logical relation corresponding to the type of M, and the Fundamental Theorem states that, whenever M is typable, the logical relation corresponding to the type M is provable.

We prove two versions of the Fundamental Theorem. The first theorem applies to all F_{ω} types, and states that if a term is typable, then the corresponding logical relation is provable. However, we need to place certain restrictions on the types of constants. For example, it would be wrong to assign type ∀t.t to a constant g, since the corresponding logical relation, ∀T.T (g), is not provable. The constraints we place on types of constants, help us avoid such problems.

The second version of the Fundamental Theorem applies only to a subset of types similar to ML types, and says that a term is typable if and only if the corresponding logical relation is provable.

We first state a lemma which is essentially the Fundamental Theorem for the pure calculus, that is we will assume the types of constants are such that the corresponding logical relations are provable.

Lemma 2.3.1. Let 𝔗𝔥 be a λ-theory, and suppose for all constants g in C_{Λ}, if Type(g) = ϕ then 𝔗𝔥 ⊢_{T T} R^{ϕ}(g). Then, for any λ-term M

if 𝔗𝔥 ⊢ {x_{i}: σ_{i}} ▷ M: σ then 𝔗𝔥, {R^{σ_{i}}(x_{i})} ⊢_{T T} R^{σ}(M).

Proof: The proof of this lemma is a straight-forward generalization of the proof of Lemma 2.5 in [Mai91] to type theory.

We would like to reformulate the assumptions of the above lemma in terms of typing constraints. In other words, how can one characterize a type ϕ, such that if g: ϕ, R^{ϕ}(g) is provable in type theory?

For example, the generators for the natural numbers, zero and succ have types Nat and Nat→Nat respectively, so we need to show that ⊢_{T T} R^{Nat}(zero) and ⊢_{T T} R^{Nat→Nat}(succ). These relations are, indeed, provable and the Church numeral λsz.z and Church successor function λnsz.(s (n s z)) represent exactly the proofs of these statements (see [Lei90])! Similarly, if the function symbol add is assigned type Nat→Nat, we need to show that 𝔓_{add} ⊢_{T T} R^{Nat→Nat}(add). Again, the lambda representation of the addition represents the proof of this relation.

We define a class of sound types, which can safely be assigned to generators of a data structure, so that the corresponding logical relations are provable.

Definition 2.3.2. We say a type ϕ is sound if

ϕ = ∀t⃗.σ_{1}→ ⋯ →σ_{k}→(c ρ_{1} ⋯ ρ_{l}),

where each ρ_{i} is pure and each σ_{i} ∈ T^{+}. The the set of types T^{+} is defined by the following grammar:

\begin{aligned}T^{+} & ::= & (c T ⋯ T ) | (t T ⋯ T ) | ∀t.T^{+} | T^{−}→T^{+} \\ T^{−} & ::= & (t T ⋯ T ) | ∀t.T^{−} | T^{+}→T^{−}, \end{aligned}

where c ranges over a set of type constructor constants, and T is the set of pure type constructors. We may write T^{+}(C) to emphasize that constant type constructors in T^{+} are taken from a set C.

Lemma 2.3.3. Let g ∈ C_{Λ} be a generator of a data structure such that Type(g) is sound. Then,

⊢_{T T} R^{ϕ}(g).

Proof: Let ({c_{1}, …, c_{m}}, {g_{1}: ϕ_{1}, …, g_{n}: ϕ_{n}}) be the signature of a data structure such that g = g_{i} for some i. Recall that we write ϕ̂ to for the type obtained from a type ϕ, be substituting a fresh variable c_{i} for each constant c_{i} in ϕ. To prove the lemma, we first show the following. Let Γ = {R^{ϕ_{1}}(g_{1}), …, R^{ϕ_{n}}(g_{n})} and let Γ̂ = {Rϕ̂_{1}(g_{1}), …, Rϕ̂_{n}(g_{n})}. Then for every σ,

(1) if σ ∈ T^{+}({c_{1}, …, c_{m}}), then Γ̂, R^{σ}(x) ⊢ Rσ̂(x), and

(2) if σ ∈ T^{−}({c_{1}, …, c_{m}}), then Γ̂, Rσ̂(x) ⊢ R^{σ}(x).

We have four cases:

Case σ ≡ (t ρ_{1} ⋯ ρ_{k}): Trivial, since σ ≡ σ̂.

Case σ ≡ (c_{j} ρ_{1} ⋯ ρ_{k}): (1) follows from the definition of R^{(c_{j} ρ_{1}···ρ_{k})}(x), and (2) is vacuously true.

Case σ ≡ τ_{1}→τ_{2}: Recall that R^{τ_{1}→τ_{2}}(x) ≡ ∀y.R^{τ_{1}}(x) ⊃ R^{τ_{2}}(xy). Therefore, Γ̂, R^{τ_{1}→τ_{2}}(x) ⊢ R^{τ_{1}}(y) ⊃ R^{τ_{2}}(xy) and Γ̂, R^{τ_{1}→τ_{2}}(x), R^{τ_{1}}(y) ⊢ R^{τ_{2}}(xy). If τ_{1}→τ_{2} is in T^{+}, we must have that τ_{1} is in T^{−} and τ_{2} is in T^{+}. Then, by the induction hypothesis Γ̂, Rτ̂_{1}(y) ⊢ R^{τ_{1}}(y) and Γ̂, R^{τ_{2}}(x y) ⊢ Rτ̂_{2}(x y). Therefore, Γ̂, R^{τ_{1}→τ_{2}}(x) ⊢ R^{τ̂_{1}→τ̂_{2}}(x). This establishes (1), and (2) follows by a similar argument.

Case σ ≡ ∀t.τ: We have R^{∀t.τ}(x) ≡ ∀T.R^{τ}(x), and (1) and (2) follow easily by the induction hypothesis.

To complete the proof, assume ϕ ≡ ∀t⃗.σ_{1}→ ⋯ σ_{k}→(c ρ_{1} ⋯ ρ_{l}), and let

Δ = {R^{σ_{1}}(x_{1}), …, R^{σ_{k}}(x_{k})} and Δ̂ = {Rσ̂_{1}(x_{1}), …, Rσ̂_{k}(x_{k})}.

By assumption we have that each σ_{j} is in T^{+} and therefore, by (1) above, Γ̂, Δ ⊢ Rσ̂_{j}(x_{j}) for all j. Moreover, since Γ̂, Δ̂ ⊢ (C R^{ρ_{1}} ⋯ R^{ρ_{l}})(g x⃗)), we also have Γ̂, Δ ⊢ (C R^{ρ_{1}} ⋯ R^{ρ_{l}})(g x⃗)) from which we conclude ⊢ R^{ϕ}(g) by (⊃ I) and (∀ I).

Remark. Lemma 2.3.3 is an extension of Theorem 3.2 in [Lei90] to a more general class of types.

Lemma 2.3.3 covers the generators of a data structure. To say that, for a function symbol f, of type σ→τ, logical relation R^{σ→τ}(f) is provable, assuming equations 𝔓_{f}, is to say that f denotes a provably total function from σ to τ [Lei90]. We will satisfy ourselves with this criterion for the function symbols included in the calculus, and note that this covers quite a large set of functions used in practice. For example, every iterative function on simple data structure is provably total, and in fact, its Böhm-Berarducci representation, which must exist [BB85], represents the proof of its totality [Lei90].

Theorem 2.3.4 (Fundamental Theorem of Logical Relations). Let 𝔗𝔥 be a λtheory, and assume that for every generator of a data structure, g, Type(g) is sound, and all function symbols denote provably total functions. Then, for any λ-term M,

if 𝔗𝔥 ⊢ {x_{i}: σ_{i}} ▷ M: σ then 𝔗𝔥, {R^{σ_{i}}(x_{i})} ⊢_{T T} R^{σ}(M).

Proof: Immediate form lemmas 2.3.1 and 2.3.3.

To prove the converse of the Fundamental Theorem for ML types, we compare a complete type inference model with a model of type theory. Recall that a type inference model is a triple (𝔗, D, subset), where 𝔗 is a type structure, D is a model of untyped lambda calculus, and subset is a function mapping interpretations of types into subsets of D. In what follows we will define a complete model of type inference based on the term model of untyped lambda calculus, and compare it with the model of type type theory defined by the same term model of the untyped lambda calculus.

The types we consider are essentially ML types. Namely, we restrict our attention to the simple types over type variables and base types. In addition assume that no type constructor constant has a kind of order more than one.

Definition 2.3.5. A type constructor σ is said to be ML type constructor if it is of kind ⋆⇒ ⋯ ⇒⋆ (or kind ⋆ as a special case), it is ∀-free, and contains no subexpression of kind greater than one (i.e. all subexpressions are of kind ⋆ or ⋆⇒ ⋯ ⇒⋆). A type of the form ∀t⃗.σ is called quantified ML type, if σ is ML type.

Fix a λ-theory, 𝔗𝔥, and let D be a term model consisting of 𝔗𝔥-equivalence classes of λ-terms. If M is a λ-term, let [M]_{𝔗𝔥} be its equivalence class.

We construct the type structure 𝔗 = ({U_{κ}}, →, ∀) to be the term model of type constructors. By abuse of notation, we write σ to denote the equivalence class of a type constructor σ.

The subset function assigns to each type σ a set D_{σ} defined as follows. Let Σ to be an infinite set of type assignments to λ-variables such that: Σ only assigns pure ML types, each variable is assigned a type exactly once by Σ, and each pure ML type is assigned to infinitely many variables by Σ. Then D_{σ} is defined to be the set

D_{σ} =^{def} {[M]_{𝔗𝔥} | for some finite Γ ⊆ Σ, 𝔗𝔥 ⊢ Γ ▷ M: σ},

It is easy to see that the subset function can be extended to type constructors of higher kind. Let σ ∈ U_{⋆⇒···⇒⋆} and define D_{σ} to be the function such that for all τ_{1}, …, τ_{k}, (D_{σ} D_{τ_{1}} ⋯ D_{τ_{k}}) = D_{(σ τ_{1}···τ_{k})}.

Assuming that no D_{(c t_{1}···t_{k})} is empty, it is easy to see that this gives us a type inference model. Therefore, assuming 𝔗𝔥 contains (η), we can characterize the sets D_{σ} as follows (see [Mit88]):

\begin{aligned}D_{σ→τ} & = & \{d ∈ D | d · D_{σ} ⊆ D_{τ}\}, and \\ D_{∀t.σ} & = & ⋂_{τ} D_{σ[τ/t]}. \end{aligned}

Now consider sets D_{(c t_{1}···t_{k})}, where (c t_{1} ⋯ t_{k}) is a base type. For simple data structures, we get a clean characterization of the sets D_{(c t_{1}···t_{k})}. Namely we have, Lemma 2.3.6. Let ({c_{1}, … c_{m}}, {g_{1}: ϕ_{1}, … g_{n}: ϕ_{n}}) be a signature of a simple data structure. For each c_{i}, the set D_{(c_{i} t_{1}···t_{k})} consists exactly of equivalence classes [M]_{𝔗𝔥}, where M is an applicative term over g_{i}’s and terms N ∈ ⋃_{t} D_{t}.

Proof: Observe that M cannot be a variable, since Σ only assigns pure types to variables. M cannot be an abstraction, for it would have a functional type. Therefore, M is an application (N_{1} N_{2} ⋯ N_{n}). Now, by the Normalization Theorem, assume M is in normal form, and therefore N_{1} cannot be an abstraction. Similarly, for the same reason M cannot be a variable, N_{1} cannot be a variable either, so it must be one of the g_{i}’s. From the restriction on the type of g_{i} we conclude that each N_{j} (for j = 2, …, n) must either be in D_{t} for some t, or by induction, is an applicative term over g_{i}’s and terms in ⋃_{t} D_{t}.

On the other hand the meaning, ⟦R^{(c t_{1}···t_{k})}⟧ρ, of the unary logical relation R^{(c t_{1}···t_{k})} in D is exactly the set of equivalence classes of terms which are applicative terms over generators g_{i} and terms in ρ(T_{i}). Thus, if ν is a type substitution, and ν̃ is an environment mapping such that ν̃(T) = D_{ν(t)}, we have that ⟦R^{(c t_{1}···t_{k})}⟧ν̃ = D_{ν(c t_{1}···t_{k})}. In fact we can generalize this correspondence beyond base types.

Lemma 2.3.7. Assume 𝔗𝔥 is a λ-theory containing (η), and that all data structures are simple. Let ν be a type substitution. Write ν̃ for an environment mapping, induced by ν, mapping variables of type theory to the model of type theory defined by D. Assume moreover that ν̃(T^{κ(⋆)}) = D_{ν(t^{⋆})} and for all τ_{i}, (ν̃(T^{κ(⋆⇒···⇒⋆)}) D_{τ_{1}} ⋯ D_{τ_{k}}) = (D_{ν(t^{⋆⇒···⇒⋆})} D_{τ_{1}} ⋯ D_{τ_{k}}). Let σ be a ML type constructor. Then,

• if σ is of kind ⋆ then ⟦R^{σ}⟧ν̃ = D_{ν(σ)}, and

• if σ is of kind ⋆⇒ ⋯ ⇒⋆ then for all τ_{i}, (⟦R^{σ}⟧ν̃ D_{τ_{1}} ⋯ D_{τ_{k}}) = (D_{ν(σ)} D_{τ_{1}} ⋯ D_{τ_{k}}).

In particular for any closed quantified ML type τ, ⟦R^{τ}⟧ν̃ ⊆ D_{ν(τ)}.

Proof: By induction of structure of σ.

Case σ = t: This case follows from assumption.

Case σ = c: Given τ_{1}, …, τ_{k} for k ≥ 0, (⟦R^{c}⟧ν̃ D_{τ_{1}} ⋯ D_{τ_{k}}) = ⟦R^{(c t_{1}···t_{k})}⟧ν̃[D_{τ_{i}}/T_{i}] which, by Lemma 2.3.6 and the discussion following the lemma, is the same as D_{(c τ_{1}···τ_{k})} = (D_{c} D_{τ_{1}} ⋯ D_{τ_{n}}).

Case σ = (τ τ_{1} ⋯ τ_{k}): It suffices to consider the case where τ is of kind ⋆⇒ ⋯ ⇒⋆ and τ_{i}’s are of kind ⋆. By definition R^{(τ τ_{1}···τ_{k})} = (R^{τ} R^{τ_{1}} ⋯ R^{τ_{k}}), so ⟦R^{(τ τ_{1}···τ_{k})}⟧ν̃ = (⟦R^{τ}⟧ν̃ ⟦R^{τ_{1}}⟧ν̃ ⋯ ⟦R^{τ_{k}}⟧ν̃). Moreover, by induction hypotheses ⟦R^{τ_{i}}⟧ν̃ = D_{ν(τ_{i})}, so

(⟦R^{τ}⟧ν̃ ⟦R^{τ_{1}}⟧ν̃ ⋯ ⟦R^{τ_{k}}⟧ν̃) = (D_{ν(τ)} D_{ν(τ_{1})} ⋯ D_{ν(τ_{k})}) = D_{ν(τ τ_{1}···τ_{k})}.

Case σ = (λt⃗.τ): Again, we only need to consider the case where t’s and τ are of kind ⋆ so that σ is of kind ⋆⇒ ⋯ ⇒⋆. By definition ⟦R^{(λt⃗.τ)}⟧ν̃ is a function f such that

for all d_{i} ⊆ D, (f d_{1} ⋯ d_{k}) = ⟦R^{τ}⟧ν̃[d⃗/T⃗]. Since for d = D_{τ′}, ν̃[d/T] still satisfies the assumption of the lemma, by induction hypothesis, for D_{τ′_{i}}, ⟦R^{τ}⟧ν̃[D_{τ′_{i}}/T_{i}] = D_{ν[τ′_{i}/t_{i}](τ)}. Therefore, f coincides with D_{ν(λt⃗.τ)} on elements of the form D_{τ} as required.

Case σ = τ_{1}→τ_{2}: By definition, ⟦R^{τ_{1}→τ_{2}}⟧ν̃ = {d ∈ D | ∀e ∈ ⟦R^{τ_{1}}⟧ν̃ . d · e ∈ ⟦R^{τ_{2}}⟧ν̃}. By induction hypothesis, ⟦R^{τ_{i}}⟧ν̃ = D_{ν(τ_{i})}, i = 1, 2, so ⟦R^{τ_{1}→τ_{2}}⟧ν̃ = D_{ν(τ_{1}→τ_{2})}.

Finally, for a type ∀t.σ we have that D_{∀t.σ} = ⋂_{τ} D_{σ[τ/t]}, so that

⟦R^{∀t.σ}⟧ν̃ = ⋂_{d} ⟦R^{σ}⟧ν̃[d/t] ⊆ D_{ν(∀t.σ)}.

We are now ready to state and prove the Fundamental Theorem for the ML types. However, in Section 2.5 we need a special case of the Fundamental Theorem, which we state in the following lemma.

Lemma 2.3.8. Let 𝔗𝔥 be a theory containing (η), and assume all data structures are simple, types of generators are sound, and function symbols denote total functions. Then if σ is a quantified ML type, and σ_{i} are pure ML types we have,

𝔗𝔥, {R^{σ_{i}}(x_{i})} ⊧_{D} R^{σ}(M) implies 𝔗𝔥 ⊢ {x_{i}: σ_{i}} ▷ M: σ.

Proof: Let Σ be an assignment of types to variables as defined earlier in this section on page 79. Assume 𝔗𝔥, {R^{σ_{i}}(x_{i})} ⊧_{D} R^{σ}(M)). For each σ_{i} let x′_{i} be such that x′_{i}: σ_{i} ∈ Σ and let ν(x_{i}) = x′_{i} and identity on other variables as well as on type variables. Let ν̃ be the environment map induced by ν (as in Lemma 2.3.7). Then [x′_{i}]_{𝔗𝔥} ∈ D_{σ_{i}} = ⟦R^{σ_{i}}⟧ν̃ and by assumption [ν(M)]_{𝔗𝔥} ∈ ⟦R^{σ}⟧ν̃. By Lemma 2.3.7, [ν(M)]_{𝔗𝔥} ∈ D_{σ}. Therefore 𝔗𝔥 ⊢ Γ ▷ M[x′_{i}/x_{i}]: σ, for some finite Γ ⊆ Σ. Moreover, Γ must contain all free variables in M[x′_{i}/x_{i}], i.e. all the x′_{i}’s, and we can conclude that 𝔗𝔥 ⊢ {x_{i}: σ_{i}} ▷ M: σ.

Theorem 2.3.9 (Fundamental Theorem of Logical Relations for ML types). Under assumptions of Lemma 2.3.8, we have,

𝔗𝔥 ⊢ {x_{i}: σ_{i}} ▷ M: σ iff 𝔗𝔥, {R^{σ_{i}}(x_{i})} ⊢_{T T} R^{σ}(M).

Proof: Immediate from Theorem 2.3.4, soundness of type theory and Lemma 2.3.8.

Remark. The Fundamental Theorem can be easily modified to logical relation of any arity. Let R^{(k)σ} denote the k-ary version of R^{σ}, and let M^{(j)} = M[x_{1}^{(j)}/x_{1}, …, x_{n}^{(j)}/x_{n}], where x^{(j)} denote distinct variables. Then the conclusion of the Fundamental Theorem reads

if 𝔗𝔥 ⊢ {x_{i}: σ_{i}} ▷ M: σ then 𝔗𝔥, {R^{(k)σ_{i}}(x_{i}^{(1)}, …, x_{i}^{(k)})} ⊢_{T T} R^{(k)σ}(M^{(1)}, ⋯, M^{(k)}).

The proof of the k-ary version of the theorem can be obtained form the proof of the unary version by replacing each unary version of a logical relation by the corresponding k-ary version.

2.4 Deriving the Free Theorems

Having proven the Fundamental Theorem we are ready to show the proofs of the free theorems. In general, our free theorems are equations by convertibility that follow from typing assumptions. We now try to describe the general heuristics involved in the deduction of free theorems from the instances of the Fundamental Theorem. Let A[M, N_{1}, …, N_{r}] and B[M, N_{1}, …, N_{r}] denote lambda terms (in Λ(C_{Λ})) with possible occurrences of M and N_{i} as subterms. We can state a generic free theorem as follows:

“Let M and N_{1}, …, N_{r} be terms such that ∅ ▷ M: σ and Γ_{i} ▷ N_{i}: τ_{i}. Then
𝔗𝔥 ⊢_{λ} A[M, N_{1}, …, N_{r}] = B[M, N_{1}, …, N_{r}].”

The term M represents the polymorphic function that the theorem describes, and N_{i} are other terms for which the typing hypotheses are necessary. All the examples from [Wad89] can be expressed in this form. The result of a free theorem is an equation that holds by convertibility form equations in 𝔗𝔥. In most of the examples, 𝔗𝔥 contains only (β), (η), as well as δ-axioms defining certain functions (e.g. program for map). However, it may contain additional assumptions as in the example about sort-like functions (see [Wad89] and Proposition 2.4.3).

All the examples of free theorems are deduced from the Fundamental Theorem using only rules (∀ E), (⊃ E) and (Cong). This suggests the following heuristics for deducing the target equation A[M, N_{1}, …, N_{r}] = B[M, N_{1}, …, N_{r}]. Without loss of generality, we may assume that R^{σ}(M) is of the form ∀T⃗.∀x⃗.Φ_{1} ⊃ ⋯ ⊃ Φ_{n} ⊃ (T_{i}(M x_{1} ⋯ x_{n})).

• Start with k-ary version of R^{σ}(M) where k is the number of occurrences of M in the target equation.

• Instantiate T_{i} to Ψ_{i}, and x_{j}^{(1)}, …, x_{j}^{(k)}, for j = 1, …, n, to appropriate lambda terms L_{j}^{(i)} so that Ψ_{i}((M L_{1}^{(1)} ⋯ L_{n}^{(1)}), …, (M L_{1}^{(k)} ⋯ L_{n}^{(k)})) equals, or is equivalent, to the target equation.

• Find instantiations Ψ⃗ and L⃗ for universally quantified variables T⃗ and x⃗ (other than those instantiated in the previous step) such that 𝔗𝔥 ⊢_{T T} Φ_{i}[Ψ⃗/T⃗, L⃗/x⃗], i = 1, …, n. In proving this, one will, in general, use the typing assumptions about N_{i}’s and the Fundamental Theorem, as well as equations in 𝔗𝔥.

• Using (⊃ E) conclude the target equation is provable, i.e. 𝔗𝔥 ⊢_{T T} A[M, N_{1}, …, N_{r}] = B[M, N_{1}, …, N_{r}].

• Finally, by Theorem 2.2.7 we conclude 𝔗𝔥 ⊢_{λ} A[M, N_{1}, …, N_{r}] = B[M, N_{1}, …, N_{r}].

This is an entirely mechanical procedure, where only nontrivial step is finding formulae Ψ⃗ and terms L⃗, so we can prove all clauses Φ_{i}[Ψ⃗/T⃗, L⃗/x⃗]. The following examples illustrate how the above heuristics is used to prove several free theorems.

Proposition 2.4.1. Assume the calculus contains data structures defining lists and natural numbers as defined in Section 2.2.3. Let M ∈ Λ(C_{Λ}) be such that ∅ ▷ M: ∀t.(List t)→Nat, and let L ∈ Λ(C_{Λ}) be such that {x_{1}: r, … x_{k}: r} ▷ L: (List r). Then,

(M L) =_{βη} (M ((λx_{1} ⋯ x_{k}.L) y_{1} ⋯ y_{k})).

More informally, this proposition says, that a polymorphic function from lists to natural numbers can only depend on the number of elements in the list.

Proof: We start with the binary version (since M occurs twice in the target equation) of the logical relation corresponding to the type of M. This relation is provable by the Fundamental Theorem, so we have 𝔗𝔥 ⊢_{T T} R^{∀t.(List t)→Nat}(M, M). We expand this relation into

∀T.∀z′z′′ . R^{(List t)}(z′, z′′) ⊃ R^{Nat}((M z′), (M z′′)),

which is provably equivalent to

∀T P.∀z′z′′ .R^{(List t)}(z′, z′′)
⊃ (∀x′x′′.P (x′, x′′) ⊃ P ((succ x′), (succ x′′)))
⊃ P (zero, zero) ⊃ P ((M z′), (M z′′)).

We first instantiate P to Λuv.u = v, and z′ and z′′ to L and ((λx_{1} ⋯ x_{k}.L)y_{1} ⋯ y_{k}), so that P ((M z′), (M z′′)) converts to the target equation ((M L) = (M ((λx_{1} ⋯ x_{k}.L) y_{1} ⋯ y_{k}))). Instantiating T to an always true relation, say Λxy.Q ⊃ Q, and using the Fundamental Theorem we can prove

R^{(List t)}(z′ z′′)[L/z′, ((λx_{1} ⋯ x_{k}.L) y_{1} ⋯ y_{k})/z′′, Λxy.Q ⊃ Q/T].

The remaining two clauses are obviously provable with the above instantiation of P, so by (⊃ E) we derive

𝔗𝔥 ⊢_{T T} (M L) = (M ((λx_{1} ⋯ x_{k}.L) y_{1} ⋯ y_{k})).

Finally by Theorem 2.2.7, we conclude

(M L) =_{βη} (M ((λx_{1} ⋯ x_{k}.L) y_{1} ⋯ y_{k})).

Remark. In the theorem above, one can include 𝔓_{map} so that the function M is allowed to use function symbol map. Then, of course, the conclusion of the theorem would read:

𝔗𝔥, 𝔓_{map} ⊢_{λ}(M L) = (M ((λx_{1} ⋯ x_{k}.L) y_{1} ⋯ y_{k})).

The following proposition is proved similarly.

Proposition 2.4.2. Let S be a pure λ-term, such that ∅▷S: ∀stu.(s→t→u)→(s→t)→s→u. Then,

S =_{βη} (λxyz.(x z) (y z)).

Proof: (Proposition 2.4.2) The target equation is S = λxyz.(x y) (x z), so we start with the unary version of the logical relation R^{∀ptu.(p→t→u)→(p→t)→p→u}(S) which is provable by the Fundamental Theorem. This relation is provably equivalent to

∀P T U.∀xyz .(∀vw.P (V) ⊃ T (w) ⊃ U(x v w)))
⊃ (∀v.P (v) ⊃ T (y v))) ⊃ P (z) ⊃ U(S x y z)).

We first instantiate U to Λv.v = (x z) (y z), so that U(S x y z)) converts to ((S x y z) = ((x z) (y z))). We then instantiate P to Λv.v = z, and T to Λv.v = (y z). Then the first three clauses are easily provable and we derive β, η ⊢_{T T} (S x y z) = ((x z) (y z)). Using (η) and Theorem 2.2.7, we get S =_{βη} λxyz.(x z) (y z).

For illustration we show how the result about sort-like functions is proved.

Proposition 2.4.3. Assume the calculus contains data structures for booleans and lists, and 𝔗𝔥 contains the program for map. Let σ be arbitrary but fixed type. Let M, C and L be terms such that ∅ ▷ M: ∀t.(t→t→Bool)→(List t)→(List t), ∅ ▷ C: (σ→σ→Bool) and {x_{i}: r} ▷ L: (List r). Let F and C′ be arbitrary lambda terms. Then,

𝔗𝔥, (C x y) = (C′ (F x) (F y)) ⊢_{λ}(map F (M C L)) = (M C′ (map F L)).

Proof: As before, we start with the binary version of the Fundamental Theorem which gives us

𝔗𝔥 ⊢_{T T} R^{∀t.(t→t→Bool)→(List t)→(List t)}(M, M),

which can be expanded into

𝔗𝔥 ⊢_{T T} ∀T.∀zz′uu′ .(∀xyx′y′.T (x, x′) ⊃ T (y, y′) ⊃ R^{Bool}((z z z), (z′ x′ y′)))
⊃ R^{(List t)}(u, u′)
⊃ ∀P.P (nil, nil)
⊃ (∀xyx′y′.T (x, x′) ⊃ P (y, y′)
⊃ P ((cons x y), (cons x′ y′)))
⊃ P (M z u), (M z′ u′)).

We instantiate P to Λxy.((map F x) = y), z to C, z′ to C′, u to L, u′ to (map F L) and T to Λxy.(Y = (F x)) ∧ (R^{σ} x y). Then, the last clause implies our target equation (map F (M C L)) = (M C′ (map F L)), and it remains to show the first two clauses are derivable with given instantiations. Using the Fundamental Theorem, we can prove

(∀xyx′y′.R^{σ}(x, x′) ⊃ R^{σ}(y, y′) ⊃ R^{Bool}((C x y), (C x′ y′))),

which implies

(∀xyx′y′.T (x, x′) ⊃ T (y, y′) ⊃ R^{Bool}((C x y), (C x′ y′))),

where T stands for above instantiation. With the additional assumption that (C x y) = (C′ (F x) (F y)) we derive

(∀xyx′y′.T (x, x′) ⊃ T (y, y′) ⊃ R^{Bool}((C x y), (C′ x′ y′))).

R^{(List t)}(L, (mapF L)) can also be derived using the Fundamental Theorem and equations for map. Finally, we use Theorem 2.2.7 to conclude the target equation holds by convertibility.

In our formulation, the conclusions of the free theorems are equations between untyped lambda terms provable by convertibility. In contrast to this, Wadler’s free theorems are semantic equations between polymorphic lambda terms. We claim that our formulation is more general. First observe that, by Church-Rosser and subject reduction properties, typed lambda theory and untyped lambda theory prove exactly the same equations between terms typable with the same type.

Secondly, by soundness, every provable equation is valid in all models of polymorphic lambda calculus, so a conclusion of a free theorem in our formulation implies the one in Wadler’s formulation.

However, a little care is needed to give a proper interpretation of a “conditional” theorem such as Wadler’s result for the sort-like functions. In Wadler’s formulation the theorem reads as follows: If M is a closed term of type ∀t.(t→t→Bool)→List(t)→List(t), then if the equation

(C x y) = (C′ (F x) (F y))

is valid then the equation

(map F (M C l)) = (M C′ (map F l))

is valid as well. Note that x, y and l are variables, and C, C′, and F are arbitrary terms. We also assume that all terms (and variables) are appropriately typed. Since validity in particular model may not imply provable equality, the conclusion of Proposition 2.4.3 does not (directly) imply the above statement. To remedy the situation, we extend the calculus with constants c, c′, and f, and assume theory 𝔗𝔥 contains equations equations c = C, c′ = C′, and f = F. Then we conclude (as in Proposition 2.4.3) that

𝔗𝔥, (c x y) = (c′ (f x) (f y) ⊢_{λ}(map f (M c L)) = (M c′ (map f L)),

where L is a term is in the assumption of Proposition 2.4.3. Now, any model of 𝔗𝔥 in which (C x y) = (C′ (F x) (F y)) is valid is a model of 𝔗𝔥, (c x y) = (c′ (f x) (f y)), so (mapf (M c L)) = (M c′ (mapf L)) is true in the model. Moreover, the meanings of C and c coincide in the model (and similarly for C′ and F), and any interpretation of l (because of the type of l) must be a list and thus a meaning of some term L satisfying the typing hypothesis. Thus, we conclude that (map F (M C l)) = (M C′ (map F l)) is valid in the model.

2.5 Representation of Constants

The examples of free theorems given in the previous section were derived from logical relations defined using a particular way of describing data structures. Naturally, one could ask whether the free theorems hold independently of the way we defined data structures. For example, datatypes such as lists, natural numbers, trees, etc., can be represented in the pure polymorphic lambda calculus using a generalization of Church numerals [BB85]. Do the free theorems hold if we choose to work with these representations? The answer is “yes”, but it requires some explaining. Let us illustrate the problem with the example of natural numbers. If we choose to represent natural numbers using the data structure ({Nat: ⋆}, {succ: Nat→Nat, zero: Nat}), as we did in our development so far, the logical relation corresponding to type Nat is the Peano’s induction axiom

Ind(n) =^{def} ∀P.(∀x.P (x) ⊃ P (succ x)) ⊃ P (zero) ⊃ P (n).

On the other hand, if we choose to represent the natural numbers as Church numerals, the type of natural numbers is defined to be

\underline{Nat} =^{def} ∀t.(t→t)→t→t,

and the corresponding logical relation is

Nat(n) =^{def} ∀P.∀sz.(∀x.P (x) ⊃ P (s z)) ⊃ P (z) ⊃ P (n s z).

Since the free theorems are, in fact, instances of logical relations, it is not obvious that one can derive the same theorems, regardless whether Ind or Nat was used in the definition of a logical relation. It is not hard to see, and we show this in general in Lemma 2.5.2, that if one substitutes Church representations of the successor and zero, λxsz.(s (x s z)) and λsz.z, for constants succ and zero, that

∀n.Ind(n) ⊃ Nat(n)

is provable in type theory. The other implication seems difficult to prove, but we can show it is valid when interpreted in a term model (of appropriate theory) of lambda calculus. Thus, the formulae Ind(n) and Nat(n) are semantically equivalent in the term model of lambda calculus, and if an equation is derivable from Ind(n), it holds by convertibility whenever Nat(n) is valid, and vice versa.

Rather than restricting ourselves to Böhm-Berarducci representation, we discuss a general notion of a representation of data structures. A representation translates terms and types, so it preserves typings and equations, thus allowing us to translate assumptions as well as conclusions of free theorems. We also discuss sufficient conditions that a representation needs to satisfy, so we can translate the proofs of the free theorems as well.

Definition 2.5.1. Let ℭ = (C_{Λ}, C_{T} , Type, 𝔗𝔥) and ℭ′ = (C_{Λ}′, C_{T} ′, Type′, 𝔗𝔥′) be two calculi. Suppose we want to translate data structures and programs from ℭ into ℭ′. Consider a function Rep_{Λ} mapping constants in C_{Λ} to Λ^{0}(C_{Λ}′), and a function Rep_{T} mapping constants in C_{T} into T^{0}(C_{T} ′). Extend functions Rep_{Λ} and Rep_{T} to be identity on variables and constants in C_{Λ}′ and C_{T} ′ respectively, and finally consider the unique homomorphic extensions of Rep_{Λ} and Rep_{T} to all of Λ(C_{Λ} + C_{Λ}′) and T (C_{T} + C_{T} ′) respectively. By abuse of notation, we write Rep_{Λ} and Rep_{T} to denote these extensions. The pair (Rep_{Λ}, Rep_{T}) is called a representation of ℭ in ℭ′ if it satisfies the following:

• for all g ∈ C_{Λ}, if σ_{g} = Type(g) then ∅ ▷ Rep_{Λ}(g): Rep_{T} (σ_{g}), and

• if M = N ∈ 𝔗𝔥 then Rep_{Λ}(M) = Rep_{Λ}(N) ∈ 𝔗𝔥′.

In other words, a representation preserves typings and equations. For simplicity we may write Rep to denote either Rep_{Λ} or Rep_{T}, or both.

Now let σ be type in T (C_{T}). In general, if σ and Rep(σ) are different types, the corresponding logical relations, R^{σ} and R^{Rep(σ)} will be different formulae. Nevertheless if for all types σ, the sequent

𝔗𝔥′ ∪ {g = Rep(g) | g ∈ C_{Λ}} ⊢ ∀x.R^{Rep(σ)}(x) ⊃ R^{σ}(x)  (†)

is valid in the model of type theory defined by the the term model of 𝔗𝔥 ∪ {g = Rep(g) | g ∈ C_{Λ}}, we will be able able to translate any free theorem using this representation, and the proof will still hold! This is formalized in Theorem 2.5.4 below.

However, checking sequent (†) at every type may be quite difficult, making it unjustified to call the translated theorems “free”. Because of Lemma 2.5.2, it is not necessary to do so, and it suffices to prove sequent (†) only when σ is a base type. (Lemma 2.5.2 is a generalization of Theorem 3.3 in [Mai91].)

Lemma 2.5.2. 𝔗𝔥′, {g = Rep(g) | g ∈ C_{Λ}} ⊢_{T T} ∀x.R^{(c_{j} t_{1}···t_{k})}(x) ⊃ R^{Rep((c_{j} t_{1}···t_{k}))}(x)

Proof Sketch: Let c_{j}’s be type constants and g_{i}’s be generators in the signature of the data structure where g = g_{i} for some i. Instantiate each C_{j} in R^{c_{j}} with R^{Rep(c_{j})}. Then using g_{i} = Rep(g_{i}) and the Fundamental Theorem we can deduce R^{Rep(ϕ_{i})}(Rep(g_{i})) for each i.

Lemma 2.5.3. If sequent (†) is valid (derivable) at all base types, then it is valid (derivable) at all types.

Proof Sketch: The proof is by induction on the structure of type σ using the assumption and Lemma 2.5.2 for the base case.

Theorem 2.5.4 (Translation). Let ℭ and ℭ′ be two calculi. Let Rep be a representation of ℭ in ℭ′ such that for each base type sequent (†) is valid in the model of type theory defined by the term model of 𝔗𝔥∪{g = Rep(g) | g ∈ C_{Λ}}. Suppose also that a free theorem

“Let M and N_{1}, …, N_{r} be terms in Λ(C_{Λ}) such that ∅ ▷ M: σ and Γ_{i} ▷ N_{i}: τ_{i}.

Then

𝔗𝔥 ⊢_{λ} A[M, N_{1}, …, N_{r}] = B[M, N_{1}, …, N_{r}].”

is provable as described in Section 2.4. Then, its translation,

“Let M′ and N′_{1}, …, N′_{r} be terms in Λ(C_{Λ}′) such that ∅ ▷ M′: Rep(σ) and
Rep(Γ_{i}) ▷ N′_{i}: Rep(τ_{i}). Furthermore, let A′[·, …, ·] = Rep(A[·, …, ·]) and
B′[·, …, ·] = Rep(B[·, …, ·]). Then
𝔗𝔥′ ⊢_{λ} A′[M′, N′_{1}, …, N′_{r}] = B′[M′, N′_{1}, …, N′_{r}].”

is provable as well.

Proof: Let D be the term model of 𝔗𝔥 ∪ {g = Rep(g) | g ∈ C_{Λ}}. By the Fundamental Theorem we have 𝔗𝔥′ ⊢_{T T} R^{Rep(σ)}(M′), and by the assumption and Lemma 2.5.3, it follows that

𝔗𝔥′, {g = Rep(g) | g ∈ C_{Λ}} ⊧_{D} R^{σ}(M′).

Using the same derivation as in the original theorem, we derive

𝔗𝔥, 𝔗𝔥′, {g = Rep(g) | g ∈ C_{Λ}} ⊧_{D} A[M′, N′_{1}, …, N′_{r}] = B[M′, N′_{1}, …, N′_{r}].

Moreover, since representation preserves equations, we conclude that

𝔗𝔥, 𝔗𝔥′, {g = Rep(g) | g ∈ C_{Λ}} ⊧_{D} A′[Rep(M′), Rep(N′_{1}), …, Rep(N′_{r})] =

B′[Rep(M′), Rep(N′_{1}), …, Rep(N′_{r})].

Notice that, since M′ and N′_{j} are in Λ(C_{Λ}′), Rep(M′) = M′ and Rep(N′_{j}) = N′_{j}, so we have

𝔗𝔥, 𝔗𝔥′, {g = Rep(g) | g ∈ C_{Λ}} ⊧_{D} A′[M′, N′_{1}, …, N′_{r}] = B′[M′, N′_{1}, …, N′_{r}].

Now observe that, since representation preserves equations, every equation provable from 𝔗𝔥 ∪ {g = Rep(g) | g ∈ C_{Λ}} is also provable from 𝔗𝔥′ ∪ {g = Rep(g) | g ∈ C_{Λ}}, and that 𝔗𝔥′ ∪ {g = Rep(g) | g ∈ C_{Λ}} is conservative over 𝔗𝔥′. Since D is the term model of 𝔗𝔥 ∪ {g = Rep(g) | g ∈ C_{Λ}}, any equation between terms in Λ(C_{Λ}′) that is valid in D is provable by convertibility from equations in 𝔗𝔥′. Hence, we conclude

𝔗𝔥′ ⊢_{λ} A′[M′, N′_{1}, …, N′_{r}] = B′[M′, N′_{1}, …, N′_{r}].

Going back to Böhm-Berarducci representation of datatypes in the pure lambda calculus, we now show that sequent (†) is valid at all base types in a term model of lambda calculus that identifies constants with their Böhm-Berarducci representations. Following [BB85] we write \underline{σ} for the representation of type σ, and likewise, \underline{M} for the representation of term M.

For example, consider the Church numerals. The type of church numerals is

\underline{Nat} =^{def} ∀t.(t→t)→t→t.

The corresponding logical relation is

R\underline{Nat}(x) =^{def} ∀P.∀sz.(∀y.P (y) ⊃ P (s y)) ⊃ P (z) ⊃ P (x s z).

Let D be a term model of a βη-theory which also identifies zero = λsz.z and succ = λxsz.(s (x s z)), and let us examine the interpretation of the above formula in this model. Fix variables s and z, and define N to be the set of elements in the model of the form s(s(⋯ (s(z)) ⋯)). (Note: when speaking of terms as elements of D, we identify terms with their equivalence classes.) Then if n ∈ ⟦R\underline{Nat}⟧ρ it follows, by interpreting P, in R\underline{Nat}, as the set N, that (n z s) = s(s(⋯ (s(z)) ⋯)), and therefore n is the meaning, in D, of a Church numeral. It is easy to see that meanings of Church numerals satisfy the induction axiom

∀P.P (zero) ⊃ (∀y.P (y) ⊃ P (succ y)) ⊃ P (x),

under the assumption that zero = λsz.z and succ = λnzs.(s (n s z)). Combining this observation with Lemma 2.5.2, it follows that, in D, the induction axiom is semantically equivalent to the logical relation corresponding to the type of Church numerals. This, as we now show, can be generalized to any data structure and its Böhm-Berarducci representation.

Let us first recall the definition of the Böhm-Berarducci representation.

Definition 2.5.5. Let ({c_{1}, …, c_{n}}, {g_{1}: ϕ_{1}, …, g_{m}: ϕ_{m}}) be a signature of a data structure. The Böhm-Berarducci representation of a base type (c_{j} t_{1} ⋯ t_{k}) is defined to be

\underline{(c_{j} t_{1} ⋯ t_{k})} =^{def} ∀c_{1} ⋯ c_{n}.ϕ̂_{1}→ ⋯ ϕ̂_{m}→(c_{j} t_{1} ⋯ t_{k}),

where we write ϕ̂ for the type ϕ with constants c_{j} replaced by the fresh variables c_{j}. The representation of a generator g_{i} is defined as follows. Assume

ϕ_{i} = ∀t⃗.α_{1}→ ⋯ →α_{k}→β_{1}→ ⋯ →β_{l},

where α’s are type variables, and β’s are base types. Then define

\underline{g_{i}} =^{def} λx_{1} ⋯ x_{k}.λy_{1} ⋯ y_{l}.λg_{1} ⋯ g_{m}.(g_{i} x_{1} ⋯ x_{k} (y_{1} g_{1} ⋯ g_{m}) ⋯ (y_{l} g_{1} ⋯ g_{m})).

Assume data structures in the calculus correspond to the class of free algebras for which the Completeness Theorem in [BB85] holds.

Theorem 2.5.6. Let ({c_{1}, …, c_{n}}, {g_{1}: ϕ_{1}, …, g_{m}: ϕ_{m}}) be a signature of a data structure satisfying the above criterion. Let D be the term model of the βη-theory that also identifies g_{i}’s with their representation. Then,

(β), (η), \{g_{i} = \underline{g_{i}} | 1 ≤ i ≤ m\} ⊧_{D} ∀x.R\underline{(c_{j} t_{1}···t_{k})}(x) ⊃ R^{(c_{j} t_{1}···t_{k})}(x).

Proof Sketch: Rather than giving a proof of the completely general case, we make up a representative example and prove the theorem for this example. Let our data structure be defined by the signature

{OList: ⋆⇒⋆, EList: ⋆⇒⋆},

        {enil: ∀s.EList(s), onil: ∀s.OList(s),
         econs: ∀s.s→OList(s)→EList(s), ocons: ∀s.s→EList(s)→OList(s)}

We call terms generated by above signature “even lists” if they are of type EList(s), and “odd lists” if they are of type OList(s). The Böhm-Berarducci representation of the above constants is defined as follows:

\underline{EList(t)} =^{def} ∀oe.o→e→(t→e→o)→(t→o→e)→e
\underline{OList(t)} =^{def} ∀oe.o→e→(t→e→o)→(t→o→e)→o
\underline{enil}  =^{def} λn_{e}n_{o}c_{e}c_{o}.n_{e}
\underline{onil}  =^{def} λn_{e}n_{o}c_{e}c_{o}.n_{o}
\underline{econs}  =^{def} λxyn_{e}n_{o}c_{e}c_{o}.(c_{e} x (y n_{e} n_{o} c_{e} c_{o}))
\underline{ocons}  =^{def} λxyn_{e}n_{o}c_{e}c_{o}.(c_{o} x (y n_{e} n_{o} c_{e} c_{o}))

Using the definition of logical relations we obtain logical relations, R^{EList(s)}(x) and R\underline{EList(s)}(x), corresponding to the constants type constructor, and its representation.

R^{EList(s)}(x) =^{def} ∀EO.E(enil) ⊃ O(onil) ⊃
(∀yz.S(y) ⊃ O(z) ⊃ E(econs y z)) ⊃
(∀yz.S(z) ⊃ E(z) ⊃ O(ocons y z)) ⊃
E(x)
R\underline{EList(s)} =^{def} ∀EO.∀n_{e}n_{o}c_{e}c_{o}.E(n_{e}) ⊃ O(n_{o})
(∀yz.S(z) ⊃ O(z) ⊃ E(c_{e} y z)) ⊃
(∀yz.S(z) ⊃ E(z) ⊃ E(c_{o} y z)) ⊃
E(x n_{e} n_{o} c_{e} c_{o})

Let D be the term model of the βη-theory including axioms that identify constants of our data structure with their representations. (Note: when we speak of a λ-term M as an element of D we are referring to the equivalence class of M.) Fix λ-variables n_{e}, n_{o}, c_{e} and c_{o}. Let the set S to be the set of all lambda terms M with variables n_{e}, n_{o}, c_{e} and c_{o} not free in M. Define sets E and O of elements in D by the following grammar:

\begin{aligned}E & ::= & n_{e} | (c_{e} S O) \\ O & ::= & n_{o} | (c_{o} S E), \end{aligned}

Interpret variable S in R\underline{EList(s)} as the set S, and assume R\underline{EList(s)}(x) is true. Interpret universally quantified variables E and O as the sets E and O defined above. Interpret universally quantified variables n_{e}, n_{o}, c_{e} and c_{o} as (equivalence classes of) variables with the same names. By definition of the sets E and O, we know that n_{e} ∈ E, and n_{o} ∈ O. Moreover, if N is a term in O, and M is a term in S, then (c_{e} M N) is in E, and likewise, if N is a term in E, the term (c_{o} M N) is in O. Therefore we can conclude that (the interpretation of) (x n_{e} n_{o} c_{e} c_{o}) is in E. Since the choice of variables n_{e}, n_{o}, c_{e} and c_{o} was arbitrary and these variables do not appear anywhere in the assumptions, we can lambda abstract to conclude that (the interpretation of) x must be a representation of an “evenlist”, and therefore R^{EList(s)}(x) must be true under the assumptions that the constants enil, onil, econs and ocons are identified with their representations.

Combining this theorem with the Translation Theorem, we conclude that the above representation preserves free theorems. Therefore, for example, Proposition 2.5.7 directly follows from Proposition 2.4.1.

Proposition 2.5.7. Let M be a closed pure λ-term, such that ∅▷M: ∀t.(\underline{List}t)→\underline{Nat}, and let L be a pure λ-term such that \{x_{1}: r, … x_{k}: r\} ▷ L: (\underline{List} r). Then,

(M L) =_{βη} (M ((λx_{1} ⋯ x_{k}.L) y_{1} ⋯ y_{k})).

Similarly, Proposition 2.1.1 follows from derivation of the corresponding result in [Mai91].

Validity of sequent (†) at base types is a sufficient condition for a representation to preserve the free theorems. As wee have seen in the preceding theorem, the proof of the validity of this sequent requires detailed understanding of the particular representation. We would like to give a more practical and, perhaps more intuitive, condition that will imply the validity of sequent (†), and thus, guarantee the free theorems are preserved.

Consider the set, D_{σ}^{0} = {M | ▷ M: σ}, of all closed terms of type σ and the restriction Rep|_{D_{σ}^{0}} as a function from D_{σ}^{0} to D_{Rep(σ)}^{0}. Then showing that this function is surjective suffices to preserve the free theorems. More formally, we have,

Theorem 2.5.8. For any quantified ML type σ, if function Rep|_{D_{σ}^{0}} is surjective then, at σ, sequent (†) is valid in the term model of 𝔗𝔥′ ∪ {g = Rep(g)}.

Proof: Let D be the term model of 𝔗𝔥′ ∪ {g = Rep(g)}, and assume that R^{Rep(σ)}(M) is true, so that

𝔗𝔥′, {g = Rep(g)} ⊧_{D} R^{Rep(σ)}(M).

Then by Lemma 2.3.8, we conclude that

𝔗𝔥′, {g = Rep(g)} ⊢ ∅ ▷ M: Rep(σ),

so that M is in D_{Repσ}^{0}. By assumption, Rep|_{D_{σ}^{0}} is surjective so there is a lambda term N such that M = Rep(N), and 𝔗𝔥 ⊢ ∅ ▷ N: σ. By the Fundamental Theorem, 𝔗𝔥 ⊢_{T T} R^{σ}(N) and therefore 𝔗𝔥′, {g = Rep(g)} ⊢_{T T} R^{σ}(M), since {g = Rep(g)} ⊢_{T T} M = N and representation preserves equations in 𝔗𝔥. Hence, by soundness, R^{σ}(M) is true in D.

By the above theorem, it suffices to check that, for each base type σ, the set D_{Rep(σ)}^{0} contains only terms representing elements in D_{σ}^{0}. For example the Completeness Theorem [BB85] for the Böhm-Berarducci representation would suffice to conclude that this representation preserves the free theorems.

While the surjectivness condition in Theorem 2.5.8 is (arguably) more intuitive, we must say it is somewhat stronger than the validity of sequent (†). For instance, the surjectivness condition may be true at base types, but fail at higher types, while, as seen in Lemma 2.5.3, if sequent (†) is valid at base types, it is also valid at higher types.

2.6 Conclusions

We have developed a syntactic framework in which parametric behavior of lambda terms is captured by logical relations as formulae of type theory. In this framework we have been able to formulate free theorems — identities about polymorphic programs that follow from the types of the programs — as equations schemas that are derivable by convertibility whenever typing assumptions about the terms involved are met.

Furthermore, we have defined a general notion of a representation of data structures. For a representation of a data structure we have defined, in two ways, a sufficient condition that guarantees that the representation preserves free theorems. In particular, we have shown that the Böhm-Berarducci representation of inductive data structures in pure lambda calculus does preserve the free theorems. This also answers the question raised by Mairson [Mai91] asking whether induction is necessary to derive free theorems.

2.7 Acknowledgments

The credit for the right formulation of the main problem addressed in this chapter should go Albert Meyer. Thanks, also to Harry Mairson for explaining the issues dealt with in this work. Thanks to both for the help in solving the problems.

Bibliography

[App92] Anrew W. Appel. Compiling with Continuations. Cambridge Universisty Press, 1992.

[Bar84] Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic. North-Holland Publishing Co., Amsterdam, second edition, 1984.

[BB85] Corrado Böhm and Alessandro Berarducci. Automatic synthesis of typed Λprograms on term algebras. Theoretical Computer Science, 39(2,3):135–154, August 1985.

[BFSS90] E. S. Bainbridge, P. J. Freyd, A. Scedrov, and P. J. Scott. Functorial polymorphism. Theoretical Computer Science, 70(1):35–64, January 1990.

[CP92] Roy L. Crole and Andrew M. Pitts. New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic. Information and Computation, 98(2):171– 210, jun 1992.

[Cro93] Roy L. Crole. Categories for Types. Cambridge Mathematical Textbooks. Cambridge University Press, Cambridge, UK, 1993.

[Fil94] Andrzej Filinski. Representing monads. In Symposium on Principles of Programming Languages, pages 446–457, Portland, Oregon, January 1994.

[Fis72] Michael J. Fischer. Lambda calculus schemata. In Proceedings of An ACM Conference on Proving Assertions About Programs, pages 104–109, Las Cruces, NM, 1972. ACM.

[Fis93] Michael Fischer. Lambda-calculus schemata. Lisp and Symbolic Computation, 6(3/4):259–288, November 1993.

[FSDF93] Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. SIGPLAN Notices, 28(6):237–247, June 1993. Proceedings of the ACM SIGPLAN ’93 Conference on Programming Language Design and Implementation.

[Gir71] Jean-Yves Girard. Une extension de l’interpretation de Gödel à l’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types. In J. E. Fenstad, editor, 2^{nd} Scandinavian Logic Symp., pages 63–92. North-Holland Publishing Co., 1971.

[Gir72] Jean-Yves Girard. Interprétation fonctionelle et élimination des coupures dans l’arithmétique d’ordre supérieure. PhD thesis, Université Paris VII, 1972.

[HD94] John Hatcliff and Olivier Danvy. A generic account of continuation-passing styles. In Proceedings of the 21st Symposium on Principles of Programming Languages, pages 458–471, Portland, Oregon, January 1994. ACM.

[HL92] Robert Harper and Mark Lillibridge. Explicit polymorphism and CPS conversion. Technical Report CMU-CS-92-210, Carnegie Mellon University, October 1992. This is an expanded version of a paper presented at the ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, Charleston, SC, January, 1993.

[Lei90] Daniel Leivant. Contracting proof to programs. In P. Odifreddi, editor, Logic and Computer Science, volume 31 of APIC Studies in Data Processing, pages 279–327. Academic Press, 1990.

[LS86] L. Lambek and P. J. Scott. Introduction to Higher Order Categorical Logic. Cambridge University Press, 1986.

[Mai91] Harry G. Mairson. Outline of a proof theory of parametricity. In J. Hughes, editor, Functional Programming Languages and Computer Architecture, volume 523 of LNCS, pages 313–327. Springer-Verlag, 1991.

[Man76] Ernest G. Manes. Algebraic Theories, volume 26 of Graduate Texts in Mathematics. Springer-Verlag, 1976.

[Mey82] Albert R. Meyer. What is a model of the lambda calculus? Information and Control, 52(1):87–122, January 1982.

[Mit88] John C. Mitchell. Polymorphic type inference and containment. Information and Computation, 76:211–249, 1988.

[MKO95] D. McAllester, J. Kučan, and D. F. Otth. A proof of strong normalization of F_{2}, F_{ω} and beyond. Information and Computation, 121(2):193–200, September 1995.

[ML71] Saunders Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, 1971.

[Mog88] Eugenio Moggi. Computational lambda-caluclus and monads. Technical Report ECS-LFCS-88-86, University of Edinburgh, October 1988.

[Mog89] Eugenio Moggi. Computational lambda-caluclus and monads. In LICS, 1989.

[Mog91] Eugenio Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92, July 1991.

[MPS86] David MacQueen, Gordon Plotkin, and Ravi Sethi. An ideal model for recursive polymorphic types. Information and Control, 71(1/2):95–130, October/November 1986.

[MR] Albert R. Meyer and Jon G. Riecke. Continuations may be unreasonable. In Proceedings of the 1988 ACM Conference on Lisp and Functional Programming, pages 63–71.

[MR91] QingMing Ma and John C. Reynolds. Types, abstraction, and parametric polymorphism, part 2. In Mathematical Foundations of Programming Semantics, 1991.

[MW85] Albert R. Meyer and Mitchell Wand. Continuation semantics in typed lambdacalculi (summary). In Rohit Parikh, editor, Logics of Programs: Proceedings, volume 193 of Lecture Notes in Computer Science, pages 219–224. Springer-Verlag, 1985.

[Plo75] G. D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1(2):125–159, December 1975.

[Rey72] John C. Reynolds. Definitional interpreters for higher-order programming languages. In Proceedings of the ACM National Meeting (Boston, 1972), pages 717–740, 1972.

[Rey83] John C. Reynolds. Types, abstraction, and parametric polymorphism. In R. E. A. Mason, editor, Information Processing 83, pages 513–523. IFIP, North-Holland Publishing Co., 1983.

[Rey93] John C. Reynolds. The discoveries of continutions. Lisp and Symbolic Computation, 6(3/4), November 1993.

[Rie93] Jon G. Riecke. Delimiting scope of side effects. In Proceedings of the 1993 Conference on Functional Programming and Computer Architecture, pages 146– 158. ACM, 1993.

[RV95] Jon G. Riecke and Ramesh Viswanathan. Isolating side effects in sequential languages. In In Proceedings of Symposium on Principles of Programming Languages, 1995.

[SF92] Amr Sabry and Mathias Felleisen. Reasoning about programs in continuationpassing style. Technical Report COMP TR 92-180, Rice University, 1992.

[SF93] Amr Sabry and Matthias Felleisen. Reasoning with continuations III: A complete calculus of control. Unpublished manuscript, 1993.

[Ste78] Guy L. Steele. Rabbit: A compiler for Scheme. Technical Report AI-TR-474, MIT Artificial Intelligence Laboratory, 1978.

[Sto77] Joseph E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge, MA, 1977.

[Str67] C. Strachey. Fundamental concepts in programming languages. Lecture Notes, Int’l. Summer School in Computer Programming, Copenhagen, 1967., 1967.

[SW74] C. Strachey and C. P. Wadsworth. Continuations: A mathematical semantics for handling full jumps. Technical Report PRG–11, Oxford University Computing Laboratory, 1974.

[SW96] Amr Sabry and Philip Wadler. A reflection on call-by-value. In International Conference on Functional Programing, Philadelphia, May 1996. ACM Press.

[Wad89] Philip Wadler. Theorems for free! In 4th International Symposium on Functional Programming Languages and Computer Architecture, London, September 1989.

[Wad90] Philip Wadler. Comprehending monads. Mathematical Structures in Computer Science, 2(4):461–493, December 1990.

[Wad95] Philip Wadler. Monads for functional programming. In J. Jeuring and E Meijer, editors, Advanced Functional Programming. Proceedings of the Båstard Spring School, May 1995. Springer Verlag Lecture Notes in Computer Science 925.