Advertisement

Extended Call-by-Push-Value: Reasoning About Effectful Programs and Evaluation Order

  • Dylan McDermottEmail author
  • Alan Mycroft
Open Access
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11423)

Abstract

Traditionally, reasoning about programs under varying evaluation regimes (call-by-value, call-by-name etc.) was done at the meta-level, treating them as term rewriting systems. Levy’s call-by-push-value (CBPV) calculus provides a more powerful approach for reasoning, by treating CBPV terms as a common intermediate language which captures both call-by-value and call-by-name, and by allowing equational reasoning about changes to evaluation order between or within programs.

We extend CBPV to additionally deal with call-by-need, which is non-trivial because of shared reductions. This allows the equational reasoning to also support call-by-need. As an example, we then prove that call-by-need and call-by-name are equivalent if nontermination is the only side-effect in the source language.

We then show how to incorporate an effect system. This enables us to exploit static knowledge of the potential effects of a given expression to augment equational reasoning; thus a program fragment might be invariant under change of evaluation regime only because of knowledge of its effects.

Keywords

Evaluation order Call-by-need Call-by-push-value Logical relations Effect systems 

1 Introduction

Programming languages based on the Open image in new window -calculus have different semantics depending on the reduction strategy employed. Three common variants are call-by-value, call-by-name and call-by-need (with the third sometimes also referred to as “lazy evaluation” when data constructors defer evaluation of arguments until the data structure is traversed). Reasoning about such programs and their equivalence under varying reduction strategies can be difficult as we have to reason about meta-level reduction strategies and not merely at the object level.

Levy [17] introduced call-by-push-value (CBPV) to improve the situation. CBPV is a calculus with separated notions of value and computation. A characteristic feature is that each CBPV program encodes its own evaluation order. It is best seen as an intermediate language into which lambda-calculus-based source-language programs can be translated. Moreover, CBPV is powerful enough that programs employing call-by-value or call-by-name (or even a mixture) can be simply translated into it, giving an object-calculus way to reason about the meta-level concept of reduction order.

However, CBPV does not enable us to reason about call-by-need evaluation. An intuitive reason is that call-by-need has “action at a distance” in that reduction of one subterm causes reduction of all other subterms that originated as copies during variable substitution. Indeed call-by-need is often framed using mutable stores (graph reduction [32], or reducing a thunk which is accessed by multiple pointers [16]). CBPV does not allow these to be encoded.

This work presents extended call-by-push-value (ECBPV), a calculus similar to CBPV, but which can capture call-by-need reduction in addition to call-by-value and call-by-name. Specifically, ECBPV adds an extra primitive Open image in new window which runs Open image in new window , with Open image in new window being evaluated the first time Open image in new window is used. On subsequent uses of Open image in new window , the result of the first run is returned immediately. The term Open image in new window is evaluated at most once. We give the syntax and type system of ECBPV, together with an equational theory that expresses when terms are considered equal.

A key justification for an intermediate language that can express several evaluation orders is that it enables equivalences between the evaluation orders to be proved. If there are no (side-)effects at all in the source language, then call-by-need, call-by-value and call-by-name should be semantically equivalent. If the only effect is nondeterminism, then need and value (but not name) are equivalent. If the only effect is nontermination then need and name (but not value) are equivalent. We show that ECBPV can be used to prove such equivalences by proving the latter using an argument based on Kripke logical relations of varying arity [12].

These equivalences rely on the language being restricted to particular effects. However, one may wish to switch evaluation order for subprograms restricted to particular effects, even if the language itself does not have such a restriction. To allow reasoning to be applied to these cases, we add an effect system [20] to ECBPV, which allows the side-effects of subprograms to be statically estimated. This allows us to determine which parts of a program are invariant under changes in evaluation order. As we will see, support for call-by-need (and action at a distance more generally) makes describing an effect system significantly more difficult than for call-by-value.

Contributions. We make the following contributions:
  • We describe extended call-by-push-value, a version of CBPV containing an extra construct that adds support for call-by-need. We give its syntax, type system, and equational theory (Sect. 2).

  • We describe two translations from a lambda-calculus source language into ECBPV: one for call-by-name and one for call-by-need (the first such translation) (Sect. 3). We then show that, if the source language has nontermination as the only effect, call-by-name and call-by-need are equivalent.

  • We refine the type system of ECBPV so that its types also carry effect information (Sect. 4). This allows equivalences between evaluation orders to be exploited, both at ECBPV and source level, when subprograms are statically limited to particular effects.

2 Extended Call-by-Push-Value

We describe an extension to call-by-push-value with support for call-by-need. The primary difference between ordinary CBPV and ECBPV is the addition of a primitive that allows computations to be added to the environment, so that they are evaluated only the first time they are used. Before describing this change, we take a closer look at CBPV and how it supports call-by-value and call-by-name.

CBPV stratifies terms into values, which do not have side-effects, and computations, which might. Evaluation order is irrelevant for values, so we are only concerned with how computations are sequenced. There is exactly one primitive that causes the evaluation of more than one computation, which is the computation Open image in new window . This means run the computation M, bind the result to x, and then run the computation N. (It is similar to Open image in new window in Haskell.) The evaluation order is fixed: M is always eagerly evaluated. This construct can be used to implement call-by-value: to apply a function, eagerly evaluate the argument and then evaluate the body of the function. No other constructs cause the evaluation of more than one computation.

To allow more control over evaluation order, CBPV allows computations to be thunked. The term Open image in new window is a value that contains the thunk of the computation Open image in new window . Thunks can be duplicated (to allow a single computation to be evaluated more than once), and can be converted back into computations with Open image in new window . This allows call-by-name to be implemented: arguments to functions are thunked computations. Arguments are used by forcing them, so that the computation is evaluated every time the argument is used. Effectively, there is a construct Open image in new window , which evaluates Open image in new window each time the variable Open image in new window is used by Open image in new window , rather than eagerly evaluating. (The variable Open image in new window is underlined here to indicate that it refers to a computation rather than a value: uses of it may have side-effects.)

To support call-by-need, extended call-by-push-value adds another construct Open image in new window . This term runs the computation Open image in new window , with the computation Open image in new window is used. On subsequent uses of Open image in new window , the result of the first run is returned immediately. The computation Open image in new window is evaluated at most once. This new construct adds the “action at a distance” missing from ordinary CBPV.

We briefly mention that adding general mutable references to call-by-push-value would allow call-by-need to be encoded. However, reasoning about evaluation order would be difficult, and so we do not take this option.

2.1 Syntax

The syntax of extended call-by-push-value is given in Fig. 1. The Open image in new window parts are new here. The rest of the syntax is similar to CBPV.1
Fig. 1.

Syntax of ECBPV

We assume two sets of variables: value variables Open image in new window and computation variables Open image in new window . While ordinary CBPV does not include computation variables, they do not of themselves add any expressive power to the calculus. The ability to use call-by-need in ECBPV comes from the Open image in new window construct used to bind the variable.2

There are two kinds of terms, value terms VW which do not have side-effects (in particular, are strongly normalizing), and computation terms MN which might have side-effects. Value terms include constants Open image in new window , and specifically the constant Open image in new window . There are no constant computation terms; value constants suffice (see Sect. 3 for an example). The value term Open image in new window suspends the computation Open image in new window ; the computation term Open image in new window runs the suspended computation Open image in new window . Computation terms also include Open image in new window -ary tuples Open image in new window (where Open image in new window ranges over finite sets); the Open image in new window th projection of a tuple Open image in new window is Open image in new window . Functions send values to computations, and are computations themselves. Application is written Open image in new window , where Open image in new window is the argument and Open image in new window is the function to apply. The term Open image in new window is a computation that just returns the value Open image in new window , without causing any side-effects. Eager sequencing of computations is given by  Open image in new window , which evaluates Open image in new window until it returns a value, then places the result in Open image in new window and evaluates Open image in new window . For example, in Open image in new window , the term Open image in new window is evaluated once, and the result is duplicated. In Open image in new window , the term Open image in new window is still evaluated once, but its result is never used. Syntactically, both Open image in new window and Open image in new window (explained below) are right-associative (so Open image in new window means Open image in new window ).

The primary new construct is Open image in new window . This term evaluates Open image in new window . The first time Open image in new window is evaluated (due to a use of Open image in new window inside Open image in new window ) it behaves the same as the computation Open image in new window . If Open image in new window returns a value Open image in new window , then subsequent uses of Open image in new window behave the same as Open image in new window . Hence only the first use of Open image in new window will evaluate Open image in new window . If Open image in new window is not used then Open image in new window is not evaluated at all. The computation variable Open image in new window bound inside the term is primarily used by eagerly sequencing it with other computations. For example,uses Open image in new window twice: once where the result is bound to Open image in new window , and once where the result is bound to Open image in new window . Only the first of these uses will evaluate Open image in new window , so this term has the same semantics as Open image in new window . The term Open image in new window does not evaluate Open image in new window at all, and has the same semantics as Open image in new window .

With the addition of Open image in new window it is not in general possible to determine the order in which computations are executed statically. Uses of computation variables are given statically, but not all of these actually evaluate the corresponding computation dynamically. In general, the set of uses of computation variables that actually cause effects depends on run-time behaviour. This will be important when describing the effect system in Sect. 4.

The standard capture-avoiding substitution of value variables in value terms is denoted \({V}[{x} \mapsto {W}]\). We similarly have substitutions of value variables in computation terms, computation variables in value terms, and computation variables in computation terms. Finally, we define the call-by-name construct mentioned above as syntactic sugar for other CBPV primitives:where Open image in new window is not free in Open image in new window .

Types are stratified into value types Open image in new window and computation types Open image in new window . Value types include the unit type, products and sum types. (It is easy to add further base types; we omit Levy’s empty types for simplicity.) Value types also include thunk types Open image in new window , which are introduced by Open image in new window and eliminated by Open image in new window . Computation types include Open image in new window -ary product types Open image in new window for finite I, function types Open image in new window , and returner types Open image in new window . The latter are introduced by Open image in new window , and are the only types of computation that can appear on the left of either Open image in new window or Open image in new window (which are the eliminators of returner types). The type constructors Open image in new window and Open image in new window form an adjunction in categorical models. Finally, contexts Open image in new window map value variables to value types, and computation variables to computation types of the form Open image in new window . This restriction is due to the fact that the only construct that binds computation variables is Open image in new window , which only sequences computations of returner type. Allowing computation variables to be associated with other forms of computation type in typing contexts is therefore unnecessary. Typing contexts are ordered lists.

The syntax is parameterized by a signature, containing the constants c.

Definition 1

(Signature). A signature Open image in new window consists of a set Open image in new window of constants of type A for each value type A. All signatures contain Open image in new window .

2.2 Type System

The type system of extended call-by-push-value is a minor extension of the type system of ordinary call-by-push-value. Assume a fixed signature Open image in new window . There are two typing judgements, one for value types and one for computation types. The rules for the value typing judgement Open image in new window and the computation typing judgement Open image in new window are given in Fig. 2. Rules that add a new variable to the typing context implicitly require that the variable does not already appear in the context. The type system admits the usual weakening and substitution properties for both value and computation variables.
Fig. 2.

Typing rules for ECBPV

It should be clear that ECBPV is actually an extension of call-by-push-value. CBPV terms embed as terms that never use the highlighted forms. We translate call-by-need by encoding call-by-need functions as terms of the formwhere \(x'\) is not free in M. This is a call-by-push-value function that accepts a thunk as an argument. The thunk is added to the context, and the body of the function is executed. The first time the argument is used (via Open image in new window ), the computation inside the thunk is evaluated. Subsequent uses do not run the computation again. A translation based on this idea from a call-by-need source language is given in detail in Sect. 3.2.

2.3 Equational Theory

In this section, we present the equational theory of extended call-by-push-value. This is an extension of the equational theory for CBPV given by Levy [17] to support our new constructs. It consists of two judgement forms, one for values and one for computations:These mean both terms are well typed, and are considered equal by the equational theory. We frequently omit the context and type when they are obvious or unimportant.
The definition is given by the axioms in Fig. 3. Note that these axioms only hold when the terms they mention have suitable types, and when suitable constraints on free variables are satisfied. For example, the second sequencing axiom holds only if Open image in new window is not free in N. These conditions are left implicit in the figure. The judgements are additionally reflexive (assuming the typing holds), symmetric and transitive. They are also closed under all possible congruence rules. There are no restrictions on congruence related to evaluation order. None are necessary because ECBPV terms make the evaluation order explicit: all sequencing of computations uses Open image in new window and Open image in new window . Finally, note that enriching the signature with additional constants will in general require additional axioms capturing their behaviour; Sect. 3 exemplifies this for constants Open image in new window representing nontermination.
Fig. 3.

Equational theory of ECBPV

For the equational theory to capture call-by-need, we might expect computation terms that are not of the form Open image in new window to never be duplicated, since they should not be evaluated more than once. There are two exceptions to this. Such terms can be duplicated in the axioms that duplicate value terms (such as the Open image in new window laws for sum types). In this case, the syntax ensures such terms are thunked. This is correct because we should allow these terms to be executed once in each separate execution of a computation (and separate executions arise from duplication of thunks). We are only concerned with duplication within a single computation. Computation terms can also be duplicated across multiple elements of a tuple Open image in new window of computation terms. This is also correct, because only one component of a tuple can be used within a single computation (without thunking), so the effects still will not happen twice. (There is a similar consideration for functions, which can only be applied once.) The remainder of the axioms never duplicate Open image in new window -bound terms that might have effects.

The majority of the axioms of the equational theory are standard. Only the axioms involving Open image in new window are new; these are highlighted. The first new sequencing axiom (in Fig. 3c) is the crucial one. It states that if a computation will next evaluate Open image in new window , where Open image in new window is a computation variable bound to M, then this is the same as evaluating M, and then using the result for subsequent uses of Open image in new window . In particular, this axiom (together with the Open image in new window law for Open image in new window ) implies that Open image in new window .

The second sequencing axiom does garbage collection [22]: if a computation bound by Open image in new window is not used (because the variable does not appear), then the binding can be dropped. This equation implies, for example, thatThe next four sequencing axioms (two from CBPV and two new) state that binding a computation with Open image in new window or Open image in new window commutes with the remaining forms of computation terms. These allow Open image in new window and Open image in new window to be moved to the outside of other constructs except thunks. The final four axioms (one from CBPV and three new) capture associativity and commutativity involving Open image in new window and Open image in new window ; again these parallel the existing simple associativity axiom for Open image in new window .
Note that associativity between different evaluation orders is not necessarily valid. In particular, we do not have(The first term might not evaluate \(M_1\), the second always does.) This is usually the case when evaluation orders are mixed [26].

These final two groups allow computation terms to be placed in normal forms where bindings of computations are on the outside. (Compare this with the translation of source-language answers given in Sect. 3.2.) Finally, the Open image in new window law for Open image in new window (in Fig. 3a) parallels the usual \(\beta \) law for Open image in new window : it gives the behaviour of computation terms that return values without having any effects.

The above equational theory induces a notion of contextual equivalence Open image in new window between ECBPV terms. Two terms are contextually equivalent when they have no observable differences in behaviour. When we discuss equivalences between evaluation orders in Sect. 3, Open image in new window is the notion of equivalence between terms that we consider.

Contextual equivalence is defined as follows. The ground types G are the value types that do not contain thunks:A value-term context Open image in new window is a computation term with a single hole (written \(-\)), which occurs in a position where a value term is expected. We write Open image in new window for the computation term that results from replacing the hole with V. Similarly, computation-term contexts Open image in new window are computation terms with a single hole where a computation term is expected, and Open image in new window is the term in which the hole is replaced by M. Contextual equivalence says that the terms cannot be distinguished by closed computations that return ground types. (Recall that \(\diamond \) is the empty typing context.)

Definition 2

(Contextual equivalence). There are two judgement forms of contextual equivalence.

  1. 1.
     
  2. 2.
    Between computation terms: Open image in new window if Open image in new window , Open image in new window , and for all ground types G and computation-term contexts Open image in new window such that Open image in new window and Open image in new window we have
     

3 Call-by-Name and Call-by-Need

Extended call-by-push-value can be used to prove equivalences between evaluation orders. In this section we prove a classic example: if the only effect in the source language is nontermination, then call-by-name is equivalent to call-by-need. We do this in two stages.

First, we show that call-by-name is equivalent to call-by-need within ECBPV (Sect. 3.1). Specifically, we show that(Recall that Open image in new window is syntactic sugar for Open image in new window .)

Second, an important corollary is that the meta-level reduction strategies are equivalent (Sect. 3.2). We show this by describing a lambda-calculus-based source language together with a call-by-name and a call-by-need operational semantics and giving sound (see Theorem 2) call-by-name and call-by-need translations into ECBPV. The former is based on the translation into the monadic metalanguage given by Moggi [25] (we expect Levy’s translation [17] to work equally well). The call-by-need translation is new here, and its existence shows that ECBPV does indeed subsume call-by-need. We then show that given any source-language expression, the two translations give contextually equivalent ECBPV terms.

To model non-termination being our sole source-language effect, we use the ECBPV signature which contains a constant Open image in new window for each value type A, representing a thunked diverging computation. It is likely that our proofs still work if we have general fixed-point operators as constants, but for simplicity we do not consider this here. The constants \(\bot _A\) enable us to define a diverging computation Open image in new window for each computation type Open image in new window :We characterise nontermination by augmenting the equational theory of Sect. 2.3 with the axiomfor each context Open image in new window , value type A and computation type Open image in new window . In other words, diverging as part of a larger computation causes the entire computation to diverge. This is the only change to the equational theory we need to represent nontermination. In particular, we do not add additional axioms involving Open image in new window .

3.1 The Equivalence at the Object (Internal) Level

In this section, we show our primary result thatAs is usually the case for proofs of contextual equivalence, we use logical relations to get a strong enough inductive hypothesis for the proof to go through. However, unlike the usual case, it does not suffice to relate closed terms. To see why, consider a closed term M of the formIf we relate only closed terms, then we do not learn anything about Open image in new window itself (since Open image in new window may be free in it). We could attempt to proceed by considering the closed term Open image in new window . For example, if this returns a value V then Open image in new window cannot have been evaluated and M should have the same behaviour as Open image in new window . However, we get stuck when proving the last step. This is only a problem because Open image in new window is a nonterminating computation: every terminating computation of returner type has the form Open image in new window (up to Open image in new window ), and when these are bound using Open image in new window we can eliminate the binding using the equationThe solution is to relate terms that may have free computation variables (we do not need to consider free value variables). The free computation variables should be thought of as referring to nonterminating computations (because we can remove the bindings of variables that refer to terminating computations). We relate open terms using Kripke logical relations of varying arity, which were introduced by Jung and Tiuryn [12] to study lambda definability.
We need a number of definitions first. A context \({\varGamma }'\) weakens another context \({\varGamma }\), written Open image in new window , whenever \({\varGamma }\) is a sublist of \({\varGamma }'\). For example, Open image in new window . We define Open image in new window as the set of equivalence classes (up to the equational theory Open image in new window ) of terms of value type A in context \({\varGamma }\), and similarly define Open image in new window for computation types:Since weakening is admissible for both typing judgements, Open image in new window implies that Open image in new window and Open image in new window (note the contravariance).

A computation context, ranged over by \({\varDelta }\), is a typing context that maps variables to computation types (i.e. has the form Open image in new window ). Variables in computation contexts refer to nonterminating computations for the proof of contextual equivalence. A Kripke relation is a family of binary relations indexed by computation contexts that respects weakening of terms:

Definition 3

(Kripke relation). A Kripke relation R over a value type A (respectively a computation type Open image in new window ) is a family of relations Open image in new window (respectively Open image in new window ) indexed by computation contexts \({\varDelta }\) such that whenever Open image in new window we have Open image in new window .

Note that we consider binary relations on equivalence classes of terms because we want to relate pairs of terms up to Open image in new window (to prove contextual equivalence). The relations we define are partial equivalence relations (i.e. symmetric and transitive), though we do not explicitly use this fact.

We need the Kripke relations we define over computation terms to be closed under sequencing with nonterminating computations. (For the rest of this section, we omit the square brackets around equivalence classes.)

Definition 4

A Kripke relation R over a computation type Open image in new window is closed under sequencing if each of the following holds:
  1. 1.
     
  2. 2.

    The pair Open image in new window is in \(R^{\varDelta }\).

     
  3. 3.
    For all Open image in new window and Open image in new window , all four of the following pairs are in \(R^{\varDelta }\):
    $$\begin{aligned} (N \mathbin {\mathsf {need}}\underline{y}.\,M,~N \mathbin {\mathsf {need}}\underline{y}.\,M') \quad&\quad ({M}[{\underline{y}} \mapsto {N}],~{M'}[{\underline{y}} \mapsto {N}]) \\ ({M}[{\underline{y}} \mapsto {N}],~N \mathbin {\mathsf {need}}\underline{y}.\,M') \quad&\quad (N \mathbin {\mathsf {need}}\underline{y}.\,M,~{M'}[{\underline{y}} \mapsto {N}]) \end{aligned}$$
     
For the first case of the definition, recall that the computation variables in \({\varDelta }\) refer to nonterminating computations. Hence the behaviour of M and \(M'\) are irrelevant (they are never evaluated), and we do not need to assume they are related.3 The second case implies (using axiom Omega) thatmirroring the first case. The third case is the most important. It is similar to the first (it is there to ensure that the relation is closed under the primitives used to combine computations). However, since we are showing that Open image in new window is contextually equivalent to substitution, we also want these to be related. We have to consider computation variables in the definition (as possible terms N) only because of our use of Kripke logical relations. For ordinary logical relations, there would be no free variables to consider.
The key part of the proof of contextual equivalence is the definition of the Kripke logical relation, which is a family of relations indexed by value and computation types. It is defined in Fig. 4 by induction on the structure of the types. In the figure, we again omit square brackets around equivalence classes.
Fig. 4.

Definition of the logical relation

The definition of the logical relation on ground types (\(\mathbf {unit}\), sum types and product types) is standard. Since the only way to use a thunk is to force it, the definition on thunk types just requires the two forced computations to be related.

For returner types, we want any pair of computations that return related values to be related. We also want the relation to be closed under sequencing, in order to show the fundamental lemma (below) for Open image in new window and Open image in new window . We therefore define Open image in new window as the smallest such Kripke relation. For products of computation types the definition is similar to products of value types: we require that each of the projections are related. For function types, we require as usual that related arguments are sent to related results. For this to define a Kripke relation, we have to quantify over all computation contexts \({\varDelta }'\) that weaken \({\varDelta }\), because of the contravariance of the argument.

The relations we define are Kripke relations. Using the sequencing axioms of the equational theory, and the \(\beta \) and \(\eta \) laws for computation types, we can show that \(R_{\underline{C}}\) is closed under sequencing for each computation type \(\underline{C}\). These facts are important for the proof of the fundamental lemma.

Substitutions are given by the following grammar:We have a typing judgement \({\varDelta } \vdash \sigma : {\varGamma }\) for substitutions, meaning in the context \({\varDelta }\) the terms in \(\sigma \) have the types given in \({\varGamma }\). This is defined as follows:
We write \(V[\sigma ]\) and \(M[\sigma ]\) for the applications of the substitution \(\sigma \) to value terms V and computation terms M. These are defined by induction on the structure of the terms. The key property of the substitution typing judgement is that if \({\varDelta } \vdash \sigma : {\varGamma }\), then Open image in new window implies Open image in new window and Open image in new window implies Open image in new window . The equational theory gives us an obvious pointwise equivalence relation Open image in new window on well-typed substitutions. We define sets Open image in new window of equivalence classes of substitutions, and extend the logical relation by defining Open image in new window :As usual, the logical relations satisfy a fundamental lemma.

Lemma 1

(Fundamental)
  1. 1.
    For all value terms \({\varGamma } \vdash _\mathrm {v} V : A\),
     
  2. 2.
     

The proof is by induction on the structure of the terms. We use the fact that each Open image in new window is closed under sequencing for the Open image in new window and Open image in new window cases. For the latter, we also use the fact that the relations respect weakening of terms.

We also have the following two facts about the logical relation. The first roughly is that \(\mathsf {name}\) is related to Open image in new window by the logical relation, and is true because of the additional pairs that are related in the definition of closed-under-sequencing (Definition 4).

Lemma 2

The second fact is that related terms are contextually equivalent.

Lemma 3

 
  1. 1.
    For all value terms \({\varGamma } \vdash _\mathrm {v} V : A\) and \({\varGamma } \vdash _\mathrm {v} V' : A\), if Open image in new window for all Open image in new window then
     
  2. 2.
     

This gives us enough to achieve the goal of this section.

Theorem 1

3.2 The Meta-level Equivalence

In this section, we show that the equivalence between call-by-name and call-by-need also holds on the meta-level; this is a consequence of the object-level theorem, rather than something that is proved from scratch as it would be in a term rewriting system.

To do this, we describe a simple lambda-calculus-based source language with divergence as the only side-effect and give it a call-by-name and a call-by-need operational semantics. We then describe two translations from the source language into ECBPV. The first is a call-by-name translation based on the embedding of call-by-name in Moggi’s [25] monadic metalanguage. The second is a call-by-need translation that uses our new constructs. The latter witnesses the fact that ECBPV does actually support call-by-need. Finally, we show that the two translations give contextually equivalent ECBPV terms.

The syntax, type system and operational semantics of the source language are given in Fig. 5. Most of this is standard. We include only booleans and function types for simplicity. In expressions, we include a constant \({\mathsf {diverge}_{A}}\) for each type A, representing a diverging computation. (As before, it should not be difficult to replace these with general fixed-point operators.) In typing contexts, we assume that all variables are distinct, and omit the required side-condition from the figure. There is a single set of variables \(x, y, \dots \); we implicitly map these to ECBPV value or computation variables as required.

The call-by-name operational semantics is straightforward; its small-step reductions are written Open image in new window .
Fig. 5.

The source language

The call-by-need operational semantics is based on Ariola and Felleisen [2]. The only differences between the source language and Ariola and Felleisen’s calculus are the addition of booleans, \({\mathsf {diverge}_{A}}\), and a type system. It is likely that we can translate other call-by-need calculi, such as those of Launchbury [16] and Maraist et al. [22]. Call-by-need small-step reductions are written \(e \overset{\mathrm {need}}{\mathbin {\rightsquigarrow }}e'\).

The call-by-need semantics needs some auxiliary definitions. An evaluation context \(E[-]\) is a source-language expression with a single hole, picked from the grammar given in the figure. The hole in an evaluation context indicates where reduction is currently taking place: it says which part of the expression is currently needed. We write E[e] for the expression in which the hole is replaced with e. A (source-language) value is the result of a computation (the word value should not be confused with the value terms of extended call-by-push-value). An answer is a value in some environment, which maps variables to expressions. These can be thought of as closures. The environment is encoded in an answer using application and lambda abstraction: the answer \((\lambda x.\,a)\,e\) means the answer a where the environment maps x to e. Encoding environments in this way makes the translation slightly simpler than if we had used a Launchbury-style [16] call-by-need language with explicit environments. In the latter case, the translation would need to encode the environments. Here they are already encoded inside expressions. Answers are terminal computations: they do not reduce.

The first two reduction axioms (on the left) of the call-by-need semantics (Fig. 5d) are obvious. The third axiom is the most important: it states that if the subexpression currently being evaluated is a variable x, and the environment maps x to a source-language value v, then that use of x can be replaced with v. Note that E[v] may contain other uses of x; the replacement only occurs when the value is actually needed. This axiom roughly corresponds to the first sequencing axiom of the equational theory of ECBPV (in Fig. 3c). The fourth and fifth axioms of the call-by-need operational semantics rearrange the environment into a standard form. Both use a syntactic restriction to answers so that each expression has at most one reduct (this restriction is not needed to ensure that Open image in new window captures call-by-need). The rule on the right of the Fig. 5d states that the reduction relation is a congruence (a needed subexpression can be reduced).
Fig. 6.

Translation from the source language to ECBPV

The two translations from the source language to ECBPV are given in Fig. 6. The translation of types (Fig. 6a) is shared between call-by-name and call-by-need. The two translations differ only for contexts and expressions. Types A are translated into value types Open image in new window . The type Open image in new window becomes the two-element sum type \(\mathbf {unit}+ \mathbf {unit}\). The translation of a function type \(A \rightarrow B\) is a thunked CBPV function type. The argument is a thunk of a computation that returns an Open image in new window , and the result is a computation that returns a Open image in new window .

For call-by-name (Fig. 6b), contexts \({\varGamma }\) are translated into contexts Open image in new window that contain thunks of computations. We could also have used contexts containing computation variables (omitting the thunks), but choose to use thunks to keep the translation as close as possible to previous translations into call-by-push-value. A well-typed expression Open image in new window is translated into a ECBPV computation term Open image in new window that returns Open image in new window , in context Open image in new window . The translation of variables just forces the relevant variable in the context. The diverging computations \({\mathsf {diverge}_{A}}\) just use the diverging constants from our ECBPV signature. The translations of \(\mathsf {true}\) and \(\mathsf {false}\) are simple: they are computations that immediately return one of the elements of the sum type \(\mathbf {unit}+ \mathbf {unit}\). The translation of Open image in new window first evaluates Open image in new window , then uses the result to choose between Open image in new window and Open image in new window . Lambdas are translated into computations that just return a thunked computation. Finally, application first evaluates the computation that returns a thunk of a function, and then forces this function, passing it a thunk of the argument.

For call-by-need (Fig. 6c), contexts \({\varGamma }\) are translated into contexts Open image in new window , containing computations that return values. The computations in the context are all bound using Open image in new window . An expression Open image in new window is translated to a computation Open image in new window that returns Open image in new window in the context Open image in new window . The typing is therefore similar to call-by-name. The key case is the translation of lambdas. These become computations that immediately return a thunk of a function. The function places the computation given as an argument onto the context using Open image in new window , so that it is evaluated at most once, before executing the body. The remainder of the cases are similar to call-by-name.

Under the call-by-need translation, the expression Open image in new window is translated into a term that executes the computation Open image in new window , and executes Open image in new window only when needed. This is the case because, by the \(\beta \) rules for thunks, functions, and returner types:As a consequence, translations of answers are particularly simple: they have the following form (up to Open image in new window ):which intuitively means the value V in the environment mapping each Open image in new window to \(M_i\).

It is easy to see that both translations produce terms with the correct types. We prove that both translations are sound: if \(e \overset{\mathrm {name}}{\mathbin {\rightsquigarrow }}e'\) then Open image in new window , and if \(e \overset{\mathrm {need}}{\mathbin {\rightsquigarrow }}e'\) then Open image in new window . To do this for call-by-need, we first look at translations of evaluation contexts. The following lemma says the translation captures the idea that the hole in an evaluation context corresponds to the term being evaluated.

Lemma 4

Define, for each evaluation context \(E[-]\), the term Open image in new window by:For each expression e we have:

This lemma omits the typing of expressions for presentational purposes. It is easy to add suitable constraints on typing. Soundness is now easy to show:

Theorem 2 (Soundness)

For any two well-typed source-language expressions Open image in new window :
  1. 1.
     
  2. 2.

    If \(e \overset{\mathrm {need}}{\mathbin {\rightsquigarrow }}e'\) then Open image in new window .

     

Now that we have sound call-by-name and call-by-need translations, we can state the meta-level equivalence formally. Suppose we are given a possibly open source-language expression Open image in new window . Recall that the call-by-need translation uses a context containing computation variables (i.e. Open image in new window ) and the call-by-name translation uses a context containing value variables, which map to thunks of computations. We have two ECBPV computation terms of type Open image in new window in context Open image in new window : one is just Open image in new window , the other is Open image in new window with all of its variables substituted with thunked computations. The theorem then states that these are contextually equivalent.

Theorem 3 (Equivalence between call-by-name and call-by-need)

For all source-language expressions e satisfying Open image in new window

Proof

The proof of this theorem is by induction on the typing derivation of e. The interesting case is lambda abstraction, where we use the internal equivalence between call-by-name and call-by-need (Theorem 1).

4 An Effect System for Extended Call-by-Push-Value

The equivalence between call-by-name and call-by-need in the previous section is predicated on the only effect in the language being nontermination. However, suppose the primitives of language have various effects (which means that in general the equivalence fails) but a given subprogram may be statically shown to have at most nontermination effects. In this case, we should be allowed to exploit the equivalence on the subprogram, interchanging call-by-need and call-by-name locally, even if the rest of the program uses other effects. In this section, we describe an effect system [20] for ECBPV, which statically estimates the side-effects of expressions, allowing us to exploit equivalences which hold only within subprograms. Effect systems can also be used for other purposes, such as proving the correctness of effect-dependent program transformations [7, 29]. The ECBPV effect system also allows these.

Call-by-need makes statically estimating effects difficult. Computation variables bound using Open image in new window might have effects on their first use, but on subsequent uses do not. Hence to precisely determine the effects of a term, we must track which variables have been used. McDermott and Mycroft [23] show how to achieve this for a call-by-need effect system; their technique can be adapted to ECBPV. Here we take a simpler approach. By slightly restricting the effect algebras we consider, we remove the need to track variable usage information, while still ensuring the effect information is not an underestimate (an underestimate would enable incorrect transformations). This can reduce the precision of the effect information obtained, but for our use case (determining equivalences between evaluation orders) this is not an issue, since we primarily care about which effects are used (rather than e.g. how many times they are used).

4.1 Effects

The effect system is parameterized by an effect algebra, which specifies the information that is tracked. Different effect algebras can be chosen for different applications. There are various forms of effect algebra. We follow Katsumata [15] and use preordered monoids, which are the most general.

Definition 5

(Preordered monoid). A preordered monoid Open image in new window consists of a monoid Open image in new window and a preorder Open image in new window on Open image in new window , such that the binary operation Open image in new window is monotone in each argument separately.

Since we do not track variable usage information, we might misestimate the effect of a call-by-need computation variable evaluated for a second time (whose true effect is Open image in new window ). To ensure this misestimate is an overestimate, we assume that the effect algebra is pointed (which is the case for most applications).

Definition 6

(Pointed preordered monoid). A preordered monoid Open image in new window is pointed if for all Open image in new window we have Open image in new window .

The elements Open image in new window of the set Open image in new window are called effects. Each effect abstractly represents some potential side-effecting behaviours. The order Open image in new window provides approximation of effects. When Open image in new window this means behaviours represented by Open image in new window are included in those represented by \(f'\). The binary operation Open image in new window represents sequencing of effects, and \(1\) is the effect of a side-effect-free expression.

Traditional (Gifford-style) effect systems have some set \({\varSigma }\) of operations (for example, Open image in new window ), and use the preordered monoid Open image in new window . In these cases, an effect \(f\) is just a set of operations. If a computation has effect Open image in new window then Open image in new window contains all of the operations the computation may perform. They can therefore be used to enforce that computations do not use particular operations. Another example is the preordered monoid Open image in new window , which can be used to count the number of possible results a nondeterministic computation can return (or to count the number of times an operation is used).

In our example, where we wish to establish whether the effects of an expression are restricted to nontermination for our main example, we use the two-element preorder Open image in new window with join for sequencing and Open image in new window . The effect \(\mathsf {diveff}\) means side-effects restricted to (at most) nontermination, and \(\top \) means unrestricted side-effects. Thus we would enable the equivalence between call-by-name and call-by-need when the effect is \(\mathsf {diveff}\), and not when it is Open image in new window . All of these examples are pointed. Others can be found in the literature.

4.2 Effect System and Signature

The effect system includes effects within types. Specifically, each computation of returner type will have some side-effects when it is run, and hence each returner type Open image in new window is annotated with an element f of \(\mathcal {F}\). We write the annotated type as Open image in new window . Formally we replace the grammar of ECBPV computation types (and similarly, the grammar of typing contexts) with(The highlighted parts indicate the differences.) The grammar used for value types is unchanged, except that it uses the new syntax of computation types.
Fig. 7.

Subtyping in the ECBPV effect system

The definition of ECBPV signature is similarly extended to contain the effect algebra as well as the set of constants:

Definition 7

(Signature). A signature Open image in new window consists of a pointed preordered monoid Open image in new window of effects and, for each value type A, a set Open image in new window of constants of type A, including Open image in new window .

We assume a fixed effect system signature for the remainder of this section.

Since types contain effects, which have a notion of subeffecting, there is a natural notion of subtyping. We define (in Fig. 7) two subtyping relations: \({A} <:_\mathrm {v} {B}\) for value types and Open image in new window for computation types.

We treat the type constructor Open image in new window as an operation on computation types by defining computation types Open image in new window .This is an action of the preordered monoid on computation types. Its purpose is to give the typing rule for sequencing of computations. The sequencing of a computation with effect \(f\) with a computation of type \(\underline{C}\) has type Open image in new window .
The typing judgements have exactly the same form as before (except for the new syntax of types). The majority of the typing rules, including all of the rules for value terms, are also unchanged. The only rules we change are those for computation variables, \(\mathop {\mathsf {return}} \), Open image in new window and Open image in new window , which are replaced with the first four rules in Fig. 8. We also add two subtyping rules, one for values and one for computations. These are the last two rules of Fig. 8.
Fig. 8.

Effect system modifications to ECBPV

The equational theory does not need to be changed to use it with the new effect system (except that the types appearing in each axiom now include effect information). For each axiom of the equational theory, the two terms still have the same type in the effect system. In particular, for the axiomif Open image in new window and Open image in new window then the left-hand side has type Open image in new window . For the right-hand-side, we have Open image in new window , because of the assumption that the preordered monoid is pointed (which implies \(\mathop {\mathsf {return}} y\) can have any effect by subtyping, not just the unit effect \(1\)). Hence the right-hand-side also has type Open image in new window . This axiom is the reason for our pointedness requirement. In particular, if we drop Open image in new window from the language, the pointedness requirement is not required. Thus the rules we give also describe a fully general effect system for CBPV in which the effect algebra can be any preordered monoid.

4.3 Exploiting Effect-Dependent Equivalences

Our primary goal in adding an effect system to ECBPV is to exploit (local, effect-justified) equivalences between evaluation orders even without a whole-language restriction on effects. We sketch how to do this for our example.

When proving the equivalence between call-by-name and call-by-need in Sect. 3 we assumed that the only constants in the language were \({()}\) and Open image in new window . To relax this restriction, we use the effect algebra with preorder Open image in new window described above, and change the type of Open image in new window to Open image in new window . We can include other effectful constants, and give them the effect Open image in new window (e.g. Open image in new window ).

The statement of the internal (object-level) equivalence becomes:The premise restricts the effect of M to \(\mathsf {diveff}\) so that nontermination is its only possible side-effect. To prove this equivalence, we need a logical relation for the effect system, which means we have to define a Kripke relation Open image in new window for each effect \(f\). For Open image in new window we use the same definition as before (the definition of Open image in new window ). The definition of Open image in new window depends on the specific other effects included.
To state and prove a meta-level equivalence for a source language that includes other side-effects, we need to define an effect system for the source language. This would use the same effect algebra as the ECBPV effect system, and be such that the translation of source language expressions preserves effects. To do this for the source language of Sect. 3, we replace the syntax of function types with Open image in new window , where \(f\) is the effect of the argument (required due to lazy evaluation), and \(f'\) is the latent effect of the function (the effect it has after application). The translation is thenJust as for the object-level equivalence, the statement of the meta-level equivalence similarly requires the source-language expression to have the effect \(\mathsf {diveff}\). We omit the details here.

5 Related Work

Metalanguages for Evaluation Order. Call-by-push-value is similar to Moggi’s monadic metalanguage [25], except for the distinction between computations and values. Both support several evaluation orders, but neither supports call-by-need. Polarized type theories [34] also take the approach of stratifying types into several kinds to capture multiple evaluation orders. Downen and Ariola [10] recently described how to capture call-by-need using polarity. They take a different approach to ours, by splitting up terms according to their evaluation order, rather than whether they might have effects. This means they have three kinds of type, resulting in a more complex language than ours. They also do not apply their language to reasoning about the differences between evaluation orders, which was the primary motivation for ECBPV. It is not clear whether their language can also be used for this purpose.

Multiple evaluation orders can also be captured in a Moggi-style language by using joinads instead of monads [28]. It is possible that there is some joinad structure implicit in extended call-by-push-value.

Reasoning About Call-by-Need. The majority of work on reasoning about call-by-need source languages has concentrated on operational semantics based on environments [16], graphs [30, 32], and answers [2, 3, 9, 22]. However, these do not compare call-by-need with other evaluation orders. The only type-based analysis of a lazy source language we know of apart from McDermott and Mycroft’s effect system [23] is [31, 33].

Logical Relations. Kripke logical relations have previously been applied to the problems of lambda definability [12] and normalization [1, 11]. Previous proofs of contextual equivalence relate only closed terms. We were forced to relate open terms because of the Open image in new window construct.

Reasoning about effects using logical relations often runs into a difficulty in ensuring the relations are closed under sequencing of computations. We are able to work around this due to our specific choice of effects. It is possible that considering other effects would require a technique such as Lindley and Stark’s leapfrog method [18, 19].

Effect Systems. Effect systems have a long history, starting with Gifford-style effect systems [20]. We use preordered monoids as effect algebras following Katsumata [15]. Almost all of the previous work on effect systems has concentrated on call-by-value only. Kammar and Plotkin [13, 14] describe a Gifford-style call-by-push-value effect system, though their formulation does not generalise to other effect algebras. Our effect system is the first general effect system for a CBPV-like language. The only previous work on call-by-need effects is [23].

There has also been much work on reasoning about program transformations using effect systems, e.g. [4, 5, 6, 7, 8, 29]. We expect it to be possible to recast much of this in terms of extended call-by-push-value, and therefore apply these transformations for various evaluation orders.

6 Conclusions and Future Work

We have described extended call-by-push-value, a calculus that can be used for reasoning about several evaluation orders. In particular, ECBPV supports call-by-need via the addition of the construct Open image in new window . This allows us to prove that call-by-name and call-by-need reduction are equivalent if nontermination is the only effect in the source language, both inside the language itself, and on the meta-level. We proved the latter by giving two translations of a source language into ECBPV: one that captures call-by-name reduction, and one that captures call-by-need reduction. We also defined an effect system for ECBPV. The effect system statically bounds the side-effects of terms, allowing equivalences between evaluation orders to be used without restricting the entire language to particular effects. We close with a description of possible future work.

Other Equivalences Between Evaluation Orders. We have proved one example of an equivalence between evaluation orders using ECBPV, but there are others that we might also expect to hold. For example, we would expect call-by-need and call-by-value to be equivalent if the effects are restricted to nondeterminism, allocating state, and reading from state (but not writing). It should be possible to use ECBPV to prove these by defining suitable logical relations. More generally, it might be possible to characterize when particular equivalences hold in terms of the algebraic properties of the effects we restrict to.

Denotational Semantics. Using logical relations to prove contextual equivalence between terms directly is difficult. Adequate denotational semantics would allow us to reduce proofs of contextual equivalence to proofs of equalities in the model. Composing the denotational semantics with the call-by-need translation would also result in a call-by-need denotational semantics for the source language. Some potential approaches to describing the denotational semantics of ECBPV are Maraist et al.’s [21] translation into an affine calculus, combined with a semantics of linear logic [24], and also continuation-passing-style translations [27]. None of these consider side-effects however.

Footnotes

  1. 1.

    The only difference is that eliminators of product and sum types are value terms rather than computation terms (which makes value terms slightly more general). Levy [17] calls this CBPV with complex values.

  2. 2.

    Computation variables are not strictly required to support call-by-need (since we can use Open image in new window instead of Open image in new window ), but they simplify reasoning about evaluation order, and therefore we choose to include them.

  3. 3.

    This is why it suffices to consider only computation contexts. If we had to relate M to \(M'\) then we would need to consider relations between terms with free value variables.

Notes

Acknowledgements

We gratefully acknowledge the support of an EPSRC studentship, and thank the anonymous reviewers for helpful comments.

References

  1. 1.
    Altenkirch, T., Hofmann, M., Streicher, T.: Categorical reconstruction of a reduction free normalization proof. In: Pitt, D., Rydeheard, D.E., Johnstone, P. (eds.) CTCS 1995. LNCS, vol. 953, pp. 182–199. Springer, Heidelberg (1995).  https://doi.org/10.1007/3-540-60164-3_27CrossRefGoogle Scholar
  2. 2.
    Ariola, Z.M., Felleisen, M.: The call-by-need lambda calculus. J. Funct. Program. 7(3), 265–301 (1997)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Ariola, Z.M., Maraist, J., Odersky, M., Felleisen, M., Wadler, P.: Acall-by-need lambda calculus. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 233–246. ACM (1995).  https://doi.org/10.1145/199448.199507
  4. 4.
    Benton, N., Hofmann, M., Nigam, V.: Effect-dependent transformations for concurrent programs. In: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, pp. 188–201. ACM (2016).  https://doi.org/10.1145/2967973.2968602
  5. 5.
    Benton, N., Kennedy, A.: Monads, effects and transformations. Electron. Notes Theor. Comput. Sci. 26, 3–20 (1999).  https://doi.org/10.1016/S1571-0661(05)80280-4CrossRefzbMATHGoogle Scholar
  6. 6.
    Benton, N., Kennedy, A., Hofmann, M., Nigam, V.: Counting successes: effects and transformations for non-deterministic programs. In: Lindley, S., McBride, C., Trinder, P., Sannella, D. (eds.) A List of Successes That Can Change the World. LNCS, vol. 9600, pp. 56–72. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-30936-1_3CrossRefzbMATHGoogle Scholar
  7. 7.
    Benton, N., Kennedy, A., Russell, G.: Compiling standard ML to Java bytecodes. In: Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming, pp. 129–140. ACM (1998).  https://doi.org/10.1145/289423.289435
  8. 8.
    Birkedal, L., Sieczkowski, F., Thamsborg, J.: A concurrent logical relation. In: Cégielski, P., Durand, A. (eds.) 21st EACSL Annual Conference on Computer Science Logic, CSL 2012. Leibniz International Proceedings in Informatics (LIPIcs), vol. 16, pp. 107–121. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl (2012).  https://doi.org/10.4230/LIPIcs.CSL.2012.107
  9. 9.
    Chang, S., Felleisen, M.: The call-by-need lambda calculus, revisited. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 128–147. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-28869-2_7CrossRefGoogle Scholar
  10. 10.
    Downen, P., Ariola, Z.M.: Beyond polarity: towards a multi-discipline intermediate language with sharing. In: 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, pp. 21:1–21:23 (2018).  https://doi.org/10.4230/LIPIcs.CSL.2018.21
  11. 11.
    Fiore, M.: Semantic analysis of normalisation by evaluation for typed lambda calculus. In: Proceedings of the 4th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 26–37. ACM (2002).  https://doi.org/10.1145/571157.571161
  12. 12.
    Jung, A., Tiuryn, J.: A new characterization of lambda definability. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 245–257. Springer, Heidelberg (1993).  https://doi.org/10.1007/BFb0037110CrossRefzbMATHGoogle Scholar
  13. 13.
    Kammar, O.: Algebraic theory of type-and-effect systems. Ph.D. thesis, University of Edinburgh, UK (2014)Google Scholar
  14. 14.
    Kammar, O., Plotkin, G.D.: Algebraic foundations for effect-dependent optimisations. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 349–360. ACM (2012).  https://doi.org/10.1145/2103656.2103698
  15. 15.
    Katsumata, S.: Parametric effect monads and semantics of effect systems. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 633–645. ACM (2014).  https://doi.org/10.1145/2535838.2535846
  16. 16.
    Launchbury, J.: A natural semantics for lazy evaluation. In: Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 144–154. ACM (1993).  https://doi.org/10.1145/158511.158618
  17. 17.
    Levy, P.B.: Call-by-push-value: a subsuming paradigm. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol. 1581, pp. 228–243. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48959-2_17CrossRefGoogle Scholar
  18. 18.
    Lindley, S.: Normalisation by evaluation in the compilation of typed functional programming languages. Ph.D. thesis, University of Edinburgh, UK (2005)Google Scholar
  19. 19.
    Lindley, S., Stark, I.: Reducibility and \(\top \)-lifting for computation types. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 262–277. Springer, Heidelberg (2005).  https://doi.org/10.1007/11417170_20CrossRefzbMATHGoogle Scholar
  20. 20.
    Lucassen, J.M., Gifford, D.K.: Polymorphic effect systems. In: Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 47–57. ACM (1988).  https://doi.org/10.1145/73560.73564
  21. 21.
    Maraist, J., Odersky, M., Turner, D.N., Wadler, P.: Call-by-name, call-by-value, call-by-need, and the linear lambda calculus. In: Proceedings of the Eleventh Annual Mathematical Foundations of Programming Semantics Conference, pp. 370–392 (1995).  https://doi.org/10.1016/S0304-3975(98)00358-2
  22. 22.
    Maraist, J., Odersky, M., Wadler, P.: The call-by-need lambda calculus. J. Funct. Program. 8(3), 275–317 (1998).  https://doi.org/10.1017/S0956796898003037MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    McDermott, D., Mycroft, A.: Call-by-need effects via coeffects. Open Comput. Sci. 8, 93–108 (2018).  https://doi.org/10.1515/comp-2018-0009CrossRefGoogle Scholar
  24. 24.
    Melliès, P.A.: Categorical semantics of linear logic. In: Interactive Models of Computation and Program Behaviour, Panoramas et Synthèses 27, Société Mathématique de France (2009)Google Scholar
  25. 25.
    Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55–92 (1991).  https://doi.org/10.1016/0890-5401(91)90052-4MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Munch-Maccagnoni, G.: Models of a non-associative composition. In: Muscholl, A. (ed.) FoSSaCS 2014. LNCS, vol. 8412, pp. 396–410. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-642-54830-7_26CrossRefzbMATHGoogle Scholar
  27. 27.
    Okasaki, C., Lee, P., Tarditi, D.: Call-by-need and continuation-passing style. LISP Symbolic Comput. 7(1), 57–81 (1994).  https://doi.org/10.1007/BF01019945CrossRefGoogle Scholar
  28. 28.
    Petricek, T., Syme, D.: Joinads: a retargetable control-flow construct for reactive, parallel and concurrent programming. In: Rocha, R., Launchbury, J. (eds.) PADL 2011. LNCS, vol. 6539, pp. 205–219. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-18378-2_17CrossRefGoogle Scholar
  29. 29.
    Tolmach, A.: Optimizing ML using a hierarchy of monadic types. In: Leroy, X., Ohori, A. (eds.) TIC 1998. LNCS, vol. 1473, pp. 97–115. Springer, Heidelberg (1998).  https://doi.org/10.1007/BFb0055514CrossRefGoogle Scholar
  30. 30.
    Turner, D.A.: A new implementation technique for applicative languages. Softw. Pract. Experience 9(1), 31–49 (1979).  https://doi.org/10.1002/spe.4380090105CrossRefzbMATHGoogle Scholar
  31. 31.
    Turner, D.N., Wadler, P., Mossin, C.: Once upon a type. In: Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture, pp. 1–11. ACM (1995).  https://doi.org/10.1145/224164.224168
  32. 32.
    Wadsworth, C.: Semantics and Pragmatics of the Lambda-Calculus. University of Oxford (1971)Google Scholar
  33. 33.
    Wansbrough, K., Peyton Jones, S.: Once upon a polymorphic type. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 15–28. ACM (1999).  https://doi.org/10.1145/292540.292545
  34. 34.
    Zeilberger, N.: The logical basis of evaluation order and pattern-matching. Ph.D. thesis, Carnegie Mellon University, Pittsburgh, PA, USA (2009)Google Scholar

Copyright information

© The Author(s) 2019

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Authors and Affiliations

  1. 1.Computer LaboratoryUniversity of CambridgeCambridgeUK

Personalised recommendations