Types by Need

Duplications and erasures have always been considered as key phenomena in the \(\lambda \)-calculus—the \(\lambda I\)-calculus, where erasures are forbidden, is an example of this. The advent of linear logic [38] gave them a new, prominent logical status. Forbidding erasure and duplication enables single-use resources, i.e. linearity, but limits expressivity, as every computation terminates in linear time. Their controlled reintroduction via the non-linear modality recovers the full expressive power of cut-elimination and allows a fine analysis of resource consumption. Duplication and erasure are therefore the key ingredients for logical expressivity, and—via Curry-Howard—for the expressivity of the \(\lambda \)-calculus. They are also essential to understand evaluation strategies.

In a \(\lambda \)-term there can be many \(\beta \)-redexes, that is, places where \(\beta \)-reduction can be applied. In this sense, the \(\lambda \)-calculus is non-deterministic. Non-determinism does not affect the result of evaluation, if any, but it affects whether evaluation terminates, and in how many steps. There are two natural deterministic evaluation strategies, call-by-name (shortened to CbN) and call-by-value (CbV), which have dual behaviour with respect to duplication and erasure.

Call-by-Name = Silly Duplication + Wise Erasure. CbN never evaluates arguments of \(\beta \)-redexes before the redexes themselves. As a consequence, it never evaluates in subterms that will be erased. This is wise, and makes CbN a normalising strategy, that is, a strategy that reaches a result whenever one exists¹. A second consequence is that if the argument of the redex is duplicated then it may be evaluated more than once. This is silly, as it repeats work already done.

Call-by-Value = Wise Duplication + Silly Erasure. CbV, on the other hand, always evaluates arguments of \(\beta \)-redexes before the redexes themselves. Consequently, arguments are not re-evaluated—this is wise with respect to duplication—but they are also evaluated when they are going to be erased. For instance, on , where \(\varOmega \) is the famous looping \(\lambda \)-term, CbV evaluation diverges (it keeps evaluating \(\varOmega \)) while CbN converges in one \(\beta \)-step (simply erasing \(\varOmega \)). This CbV treatment of erasure is clearly as silly as the duplicated work of CbN.

Call-by-Need = Wise Duplication + Wise Erasure. It is natural to try to combine the advantages of both CbN and CbV. The strategy that is wise with respect to both duplications and erasures is usually called call-by-need (CbNeed), it was introduced by Wadsworth [57], and dates back to the ’70s. Despite being at the core of Haskell, one of the most-used functional programming languages, and—in its strong variant—being at work in the kernel of Coq as designed by Barras [16], the theory of CbNeed is much less developed than that of CbN or CbV.

One of the reasons for this is that it cannot be defined inside the \(\lambda \)-calculus without some hacking. Manageable presentations of CbNeed indeed require first-class sharing and micro-step operational semantics where variable occurrences are replaced one at a time (when needed), and not all at once as in the \(\lambda \)-calculus. Another reason is the less natural logical interpretation.

Linear Logic, Names, Values, and Needs. CbN and CbV have neat interpretations in linear logic. They correspond to two different representations of intuitionistic logic in linear logic, based on two different representations of implication².

The logical interpretation of CbNeed—studied by Maraist et al. in [47]—is less neat than those of CbN and CbV. Within linear logic, CbNeed is usually understood as corresponding to the CbV representation where erasures are generalised to all terms, not only those under the scope of a modality. So, it is seen as a sort of affine CbV. Such an interpretation however is unusual, because it does not match exactly with cut-elimination in linear logic, as for CbN  and CbV.

Call-by-Need, Abstractly. The main theorem of the theory of CbNeed is that it is termination equivalent to CbN, that is, on a fixed term, CbNeed evaluation terminates if and only if CbN evaluation terminates, and, moreover, they essentially produce the same result (up to some technical details that are irrelevant here). This is due to the fact that both strategies avoid silly divergent sequences such as that of \((\lambda x.\lambda y.y) \varOmega \). Termination equivalence is an abstract theorem stating that CbNeed erases as wisely as CbN. Curiously, in the literature there are no abstract theorems reflecting the dual fact that CbNeed duplicates as wisely as CbV—we provide one, as a side contribution of this paper.

Call-by-Need and Denotational Semantics. CbNeed is then usually considered as a CbV optimisation of CbN. In particular, every denotational model of CbN is also a model of CbNeed, and adequacy—that is the fact that the denotation of \(t\) is not degenerated if and only if \(t\) terminates—transfers from CbN to CbNeed.

Denotational semantics is invariant by evaluation, and so is insensitive to evaluation lengths by definition. It then seems that denotational semantics cannot distinguish between CbN and CbNeed. The aim of this paper is, somewhat counter-intuitively, to separate CbN and CbNeed semantically. We develop a type system whose type judgements induce a model—this is typical of intersection type systems—and whose type derivations provide exact bounds for CbNeed evaluation—this is usually obtained via non-idempotent intersection types. Unsurprisingly, the design of the type system requires a delicate mix of erasure and duplication and builds on the linear logic understanding of CbN  and CbV.

Multi Types. Our typing framework is given by multi types, which is an alternative name for non-idempotent intersection types³. Multi types characterise termination properties exactly as intersection types, having moreover the advantages that they are closely related to (the relational semantics of) linear logic, their type derivations provide quantitative information about evaluation lengths, and the proof techniques are simpler—no need for the reducibility method.

The seminal work of de Carvalho [23] (appeared in 2007 but unpublished until 2018, see also [22]) showed how to use multi types to obtain exact bounds on evaluation lengths in CbN. Ehrhard adapted multi types to CbV [34], and very recently Accattoli and Guerrieri adapted de Carvalho’s study of exact bounds to Ehrhard’s system and CbV evaluation [8]. Kesner used de Carvalho’s CbN multi types to obtain a simple proof that CbNeed is termination equivalent to CbN [40] (first proved with other techniques by Maraist, Odersky, and Wadler [48] and Ariola and Felleisen [11] in the nineties), and then Kesner and coauthors continued exploring the theory of CbNeed via CbN multi types [14, 15, 42].

Kesner’s use of CbN multi types to study CbNeed is qualitative, as it deals with termination and not with exact bounds. For a quantitative study of CbNeed, de Carvalho’s CbN system cannot really be informative: CbN multi types provide bounds for CbNeed which cannot be exact because they already provide exact bounds for CbN, which generally takes more steps than CbNeed.

Multi Types by Need. In this paper we provide the first multi type system characterising CbNeed termination and whose minimal type derivations provide exact bounds for CbNeed evaluation lengths. The design of the type system is delicate, as we explain in Sect. 6. One of the key points is that, in contrast to Ehrhard’s system for CbV [34], multi types for CbNeed cannot be directly extracted by the relational semantics of linear logic, given that CbNeed does not have a clean representation in it. A by-product of our work is a new denotational semantics of CbNeed, the first one to precisely reflect its quantitative properties.

Beyond the result itself, the paper tries to stress how the key ingredients of our type system are taken from those for CbN and CbV and combined together. To this aim, we first present multi types for CbN and CbV, and only then we proceed to build the CbNeed system and prove its properties.

Along the way, we also prove the missing fundamental property of CbNeed, that is, that it duplicates as efficiently as CbV. The result dualizes the termination equivalence of CbN and CbNeed, which shows that CbNeed erases as wisely as CbN. Careful: the CbV system is correct but of course not complete with respect to CbNeed, because CbNeed may normalise when CbV diverges. The proof of the result is straightforward, because of our presentations of CbV and CbNeed. We adopt a liberal, non-deterministic formulation of CbV, and assuming (without loss of generality, see [1]) that garbage collection is always postponed. These two ingredients turn CbNeed into a fragment of CbV, obtaining the new fundamental result as a corollary of correctness of CbV multi types for CbV evaluation.

Technical Development. The paper is extremely uniform, technically speaking. The three evaluations are presented as strategies of Accattoli and Kesner’s Linear Substitution Calculus (shortened to LSC) [1, 6], a calculus with a simple but expressive form of explicit sharing. The LSC is strongly related to linear logic [2], and provides a neat and manageable presentation of CbNeed, introduced by Accattoli, Barenbaum, and Mazza in [3], and further developed by various authors in [4, 5, 10, 14, 15, 40, 42]. Our type systems count evaluation steps by annotating typing rules in the exact same way, and the proofs of correctness and completeness all follow the exact same structure. While the results for CbN are very minor variations with respect to those in the literature [7, 23], those for CbV are the first ones with respect to a presentation of CbV with sharing.

As it is standard for CbNeed, we restrict our study to closed terms and weak evaluation (that is, out of abstractions). The main consequence of this fact is that normal forms are particularly simple (sometimes called answers in the literature). Compared with other recent works dealing with exact bounds such as Accattoli, Graham-Lengrand, and Kesner [7] and Accattoli and Guerrieri [8] the main difference is that the size of normal forms is not taken into account by type derivations. This is because of the simple notions of normal forms in the closed and weak case, and not because the type systems are not accurate.

Related Work About CbNeed. Call-by-need was introduced by Wadsworth [57] in the ’70s. In the ’90s, it was first reformulated as operational semantics by Launchbury [46], Maraist, Odersky, and Wadler [48], and Ariola and Felleisen [11, 12], and then implemented by Sestoft [55] and further studied by Kutzner and Schmidt-Schauß [45]. More recent papers are Garcia, Lumsdaine, and Sabry [36], Ariola, Herbelin, and Saurin [13], Chang and Felleisen [26], Danvy and Zerny [29], Downen et al. [33], Pédrot and Saurin [53], and Balabonski et al. [14].

Related Work About Multi Types. Intersection types are a standard tool to study \(\lambda \)-calculi—see Coppo and Dezani [27, 28], Pottinger [54], and Krivine [44]. Non-idempotent intersection types, i.e. multi types, were first considered by Gardner [37], and then by Kfoury [43], Neergaard and Mairson [50], and de Carvalho [23]—a survey is Bucciarelli, Kesner, and Ventura [20].

Many recent works rely on multi types or relational semantics to study properties of programs and proofs. Beyond the cited ones, Diaz-Caro, Manzonetto, and Pagani [32], Carraro and Guerrieri [21], Ehrhard and Guerrieri [35], and Guerrieri [39] deal with CbV, while Bernadet and Lengrand [17], de Carvalho, Pagani, and Tortora de Falco [24] provide exact bounds. Further related work is by Bucciarelli, Ehrhard, and Manzonetto [18], de Carvalho and Tortora de Falco [25], Tsukada and Ong [56], Kesner and Vial [41], Piccolo, Paolini and Ronchi Della Rocca [52], Ong [51], Mazza, Pellissier, and Vial [49], Bucciarelli, Kesner and Ronchi Della Rocca [19]—this list is not exhaustive.

Proofs. Proofs are omitted. They can be found in the technical report [9].

In this section we define the CbN, CbV, and CbNeed evaluation strategies. We present them in the context of the Accattoli and Kesner’s linear substitution calculus (LSC) [1, 6]. We mainly follow the uniform presentation of these strategies given by Accattoli, Barenbaum, and Mazza [3]. The only difference is that we adopt a non-deterministic presentation of CbV, subsuming both the left-to-right and the right-to-left strategies in [3], that makes our results slightly more general. Such a non-determinism is harmless: not only CbV evaluation is confluent, it even has the diamond property, so that all evaluations have the same length. Moreover, the non-deterministic presentation, together with the postponement of erasing steps discussed below, allows us to see CbNeed as a fragment of CbV, which shall provide a free proof that CbNeed duplicates as wisely as CbV.

Terms and Contexts. The set of terms \(\varLambda _{\mathtt{lsc}}\) of the LSC is given by the grammar below, where \(t[x{\leftarrow }s]\) is an explicit substitution (shortened to ES), that is a more compact notation for \(\mathtt{let}\ x=s\ \mathtt{in}\ t\) (intuitively, “\(t\) where \(x\) will be substituted by \(s\)”). Both \(\lambda x.t\) and \(t[x{\leftarrow }s]\) bind \(x\) in \(t\), with the usual notion of \(\alpha \)-equivalence.The set \(\mathtt{fv}(t)\) of free variables of a term \(t\) is defined as expected, in particular, . A term \(t\) is closed if \(\mathtt{fv}(t) = \emptyset \), open otherwise. As usual, terms are identified up to \(\alpha \)-equivalence.

Contexts are terms with exactly one occurrence of the hole \(\langle \cdot \rangle \), an additional constant. We shall use many different contexts. The most general ones are weak contexts \(W\) (i.e. not under abstractions). The (evaluation) contexts \(C\), \(V\) and \(E\)—used to define CbN, CbV and CbNeed evaluation strategies, respectively—are special cases of weak contexts (in fact, CbV contexts coincide with weak contexts, the consequences of that are discussed on p. 8). To define evaluation strategies, substitution contexts (i.e. lists of explicit substitutions) also play a role.

We write \(W\langle t\rangle \) for the term obtained by replacing the hole \(\langle \cdot \rangle \) in context \(W\) by the term \(t\). This plugging operation, as usual with contexts, can capture variables—for instance \(((\langle \cdot \rangle t)[x{\leftarrow }s])\langle x\rangle = (xt)[x{\leftarrow }s]\). We write \(W\langle \! \langle t \rangle \! \rangle \) when we want to stress that the context \(W\) does not capture the free variables of \(t\).

Micro-step Semantics. The rewriting rules decompose the usual small-step semantics for \(\lambda \)-calculi, by substituting linearly one variable occurrence at the time, and only when such an occurrence is in evaluation position. We emphasise this fact saying that we adopt a micro-step semantics. We now give the definitions, examples of evaluation sequences follow right next.

Formally, a micro-step semantics is defined by first giving its root-steps and then taking the closure of root-steps under suitable contexts.

where, in the root-step \(\mapsto _{\mathtt m}\) (resp. \(\mapsto _{{\mathtt e}_\mathrm{cbv}}\); \(\mapsto _{{\mathtt e}_\mathrm{need}}\)), if for some \(n \in \mathbb {N}\), then \(\mathtt{fv}(s)\) (resp. \(\mathtt{fv}(V\langle \! \langle x \rangle \! \rangle )\); \(\mathtt{fv}(E\langle \! \langle x \rangle \! \rangle )\)) and \(\{y_1, \dots , y_n\}\) are disjoint. This condition can always be fulfilled by \(\alpha \)-equivalence.

The evaluation strategies \( \ {\xrightarrow {}}{}_{{\mathrm{cbn}}}^{} \) for CbN, \( \ {\xrightarrow {}}{}_{{\mathrm{cbv}}}^{} \) for CbV, and \( \ {\xrightarrow {}}{}_{{\mathrm{need}}}^{} \) for CbNeed, are defined as the closure of root-steps under CbN, CbV and CbNeed evaluation contexts, respectively (so, all evaluation strategies do not reduce under abstractions, since all such contexts are weak):

where the notation means that, given a root-step \(\mapsto \), the evaluation \( \ {\xrightarrow {}}{}_{{}}^{} \) is defined as follows: \(t \ {\xrightarrow {}}{}_{{}}^{} s\) if and only if there are terms \(t'\) and \(s'\) and a context \(W\) such that \(t= W\langle t'\rangle \) and \(s= W\langle s'\rangle \) and \(t' \mapsto s'\).

Note that evaluations \( \ {\xrightarrow {}}{}_{{\mathrm{cbn}}}^{} \), \( \ {\xrightarrow {}}{}_{{\mathrm{cbv}}}^{} \) and \( \ {\xrightarrow {}}{}_{{\mathrm{need}}}^{} \) can equivalently be defined as \( \ {\xrightarrow {}}{}_{{{\mathtt m}_\mathrm{cbn}}}^{} \cup \ {\xrightarrow {}}{}_{{{\mathtt e}_\mathrm{cbn}}}^{} \), \( \ {\xrightarrow {}}{}_{{{\mathtt m}_\mathrm{cbn}}}^{} \cup \ {\xrightarrow {}}{}_{{{\mathtt e}_\mathrm{cbv}}}^{} \) and \( \ {\xrightarrow {}}{}_{{{\mathtt m}_\mathrm{need}}}^{} \cup \ {\xrightarrow {}}{}_{{{\mathtt e}_\mathrm{need}}}^{} \), respectively.

Given an evaluation sequence \(d:t \ {\xrightarrow {}}{}_{\mathrm{cbn}}^{*} s\) we note with \(|d|\) the length of \(d\), and with \(|d|_{{\mathtt m}}\) and \(|d|_{{\mathtt e}}\) the number of multiplicative and exponential steps in \(d\), respectively—and similarly for \( \ {\xrightarrow {}}{}_{{\mathrm{cbv}}}^{} \) and \( \ {\xrightarrow {}}{}_{{\mathrm{need}}}^{} \).

Erasing Steps. The reader may be surprised by our evaluation strategies, as none of them includes erasing steps, despite the absolute relevance of erasures pointed out in the introduction. There are no contradictions: in the LSC—in contrast to the \(\lambda \)-calculus—erasing steps can always be postponed (see [1]), and so they are often simply omitted. This is actually close to programming language practice, as the garbage collector acts asynchronously with respect to the evaluation flow. For the sake of clarity let us spell out the erasing rules—they shall nonetheless be ignored in the rest of the paper. In CbN and CbNeed every term is erasable, so the root erasing step takes the following formand it is then closed by weak evaluation contexts.

In CbV only values are erasable; so, the root erasing step in CbV is:and it is then closed by weak evaluation contexts.

CbV Diamond Property. CbV contexts coincide with weak ones. As a consequence, our presentation of CbV is non-deterministic, as for instance one can havebut it is easily seen that diagrams can be closed in exactly one step (if the two reducts are different). For instance,Moreover, the kind of steps is preserved, as the example illustrates. This is an instance of the strong form of confluence called diamond property. A consequence is that either all evaluation sequences normalise or all diverge, and if they normalise they have all the same length and the same number of steps of each kind. Roughly, the diamond property is a form of relaxed determinism. In particular, it makes sense to talk about the number of multiplicative/exponential steps to normal form, independently of the evaluation sequence. The proof of the property is an omitted routine check of diagrams.

Normal Forms. We use two predicates to characterise normal forms, one for both CbN and CbNeed normal forms, for which ES can contain whatever term, and one for CbV normal forms, where ES can only contain normal terms:

The simple structure of normal forms is the main point where the restriction to closed calculi plays a role in this paper.

From the syntactic characterization of normal forms (Proposition 1) it follows immediately that among closed terms, normal forms for CbN and CbNeed coincide, while normal forms for CbV are a subset of them. Such a subset is proper since the closed term \(I [x{\leftarrow }\delta \delta ]\) (where and ) is normal for CbN and CbNeed but not for CbV (and it cannot normalise in CbV).

In this section we define basic notions about multi types, type contexts, and (type) judgements that are shared by the three typing systems of the paper.

Multi-sets. The type systems are based on two layers of types, defined in a mutually recursive way, linear types \(L\) and finite multi-sets \(M\) of linear types. The intuition is that a linear type \(L\) corresponds to a single use of a term, and that an argument \(t\) is typed with a multi-set \(M\) of n linear types if it is going to end up (at most) n times in evaluation position, with respect to the strategy associated with the type system. The three systems differ on the definition of linear types, that is therefore not specified here, while all adopt the same notion of finite multi-set \(M\) of linear types (named multi type), that we now introduce:

where \([\ldots ]_{{}}\) denotes the multi-set constructor. The empty multi-set \([\,]\) (the multi type obtained for \(J = \emptyset \)) is called empty (multi) type and denoted by the special symbol \(\mathbf {0}\). An example of multi-set is \([L, L, {L'}]_{{}}\), that contains two occurrences of \(L\) and one occurrence of \({L'}\). Multi-set union is noted .

Type Contexts. A type context is a (total) map from variables to multi types such that only finitely many variables are not mapped to . The domain of is the set . The type context is empty if .

Multi-set union is extended to type contexts point-wise, i.e. for each variable \(x\). This notion is extended to a finite family of type contexts as expected, so that denotes a finite union of type contexts—it stands for the empty context when \(J = \emptyset \). A type context is denoted by \(x_1 \,{:}\,M_1, \dots , x_n \,{:}\,M_n\) (for some \(n \in \mathbb {N}\)) if and for all \(1 \le i \le n\). Given two type contexts and \(\varPi \) such that , the type context is defined by if , if \(x\in \mathtt{dom}({\varPi })\), and otherwise.

Judgements. Type judgements are of the form or (noted also \( {}\ {\pmb \vdash }_{}^{(m, e)} {t} \,{:}\,{L}\) and \( {}\ {\pmb \vdash }_{}^{(m, e)} {t} \,{:}\,{M}\), respectively, when is the empty context), where the indices \(m\) and \(e\) are natural numbers whose intended meaning is that \(t\) evaluates to normal form in \(m\) multiplicative steps and \(e\) exponential steps, with respect to the evaluation strategy associated with the type system.

To make clear in which type systems the judgement is derived, we write if \(\varPhi \) is a derivation in the CbN system ending in the judgement , and similarly for CbV and CbNeed.

In this section we introduce the CbN multi type system, together with intuitions about multi types. We also prove that derivations provide exact bounds on CbN evaluation sequences, and define the induced denotational model.

CbN Types. The system is essentially a reformulation of de Carvalho’s system \(\mathtt R\) [23], itself being a type-based presentation of the relational model of the CbN \(\lambda \)-calculus induced by relational model of linear logic via the CbN translation of \(\lambda \)-calculus into linear logic. Definitions:Subtleties and Easy Facts. Let us overview some facts about our presentation of the type system.

Lemma 1 implies that derivations of closed terms have empty type context. Note that there can be free variables of \(t\) not in : the ones only occurring in subterms not touched by the evaluation strategy.

Key Ingredients. Two key points of the CbN system that play a role in the design of the CbNeed one in Sect. 6 are:Tight Derivations. A term may have several derivations, indexed by different pairs \((m, e)\). They always provide upper bounds on CbN evaluation lengths. The interesting aspect of our type systems, however, is that there is a simple description of a class of derivations that provide exact bounds for these quantities, as we shall show. Their definition relies on the \(\mathsf{{normal}} \) type constant.

The next two subsections prove the two halves of the properties of the CbN type system, namely correctness and completeness.

Here we introduce Ehrhard’s CbV multi type system [34] adapted to our presentation of CbV in the LSC, and prove its properties. The system is similar, and yet in many aspects dual, to the CbN one, in particular the grammar of types is different. Linear types for CbV are defined by:

Multi(-sets) types are defined as in Sect. 3, relatively to CbV linear types. Note that linear types now have a multi type both as source and as target, and that the \(\mathsf{{normal}} \) constant is absent—in CbV, its role is played by \(\mathbf {0}\).

The typing rules are in Fig. 2. It is a type-based presentation of the relational model of the CbV \(\lambda \)-calculus induced by relational model of linear logic via the CbV translation of \(\lambda \)-calculus into linear logic. Some remarks:

Intuitions: The Empty Type \(\mathbf {0}\). The empty multi-set type \(\mathbf {0}\) plays a special role in CbV. As in CbN, it is the type of terms that can be erased, but, in contrast to CbN, not every term is erasable in CbV.

In the CbN multi type system every term, even a diverging one, is typable with \(\mathbf {0}\). On the one hand, this is correct, because in CbN every term can be erased, and erased terms can also be divergent, because they are never evaluated. On the other hand, adequacy is formulated with respect to non-empty types: a term terminates if and only if it is typable with a non-empty type.

In CbV, instead, terms have to be evaluated before being erased; and, of course, their evaluation has to terminate. Thus, terminating terms and erasable terms coincide. Since the multi type system is meant to characterise terminating terms, in CbV a term is typable if and only if it is typable with \(\mathbf {0}\), as we shall prove in this section. Then the empty type is not a degenerate type excluded for adequacy from the interesting types of a term, as in CbN, it rather is the type, characterising (adequate) typability altogether. And this is also the reason for the absence of the constant \(\mathsf{{normal}} \)—one way to see it is that in CbV \(\mathsf{{normal}} = \mathbf {0}\).

Note that, in particular, in a type judgement the type context may give the empty type to a variable \(x\) occurring in \(t\), as for instance in the axiom \(x\,{:}\,\mathbf {0}\vdash x\,{:}\,\mathbf {0}\)—this may seem very strange to people familiar with CbN multi types. We hope that instead, according to the provided intuition that \(\mathbf {0}\) is the type of termination, it would rather seem natural.

Correctness (i.e. typability implies normalisability) and completeness (i.e. normalisability implies typability) of the CbV type system with respect to CbV evaluation (together with quantitative information about evaluation lengths) follow exactly the same pattern of the CbN case, mutatis mutandis.

CbNeed as a Blend of CbN and CbV. The multi type system for CbNeed is obtained by carefully blending ingredients from the CbN and CbV ones:

It seems then that a type system for CbNeed can easily be obtained by basically adopting the CbV system plus

Therefore, the grammar of linear types is:

Multi(-sets) types are defined as in Sect. 3, relatively to CbNeed linear types. The rules of this naïve system for CbNeed are in Fig. 3.

Issue with the Naïve System. Unfortunately, the naïve system does not work: tight derivations—defined as expected: empty type context and the term typed with \([ \mathsf{{normal}} ] \)—do not provide exact bounds. The problem is that the naïve blend of ingredients allows derivations of \(\mathbf {0}\) with strictly positive indices \(m\) and \(e\). Instead, derivations of \(\mathbf {0}\) should always have 0 in both indices—as is the case when they are derived with a \(\mathsf {many} _0\) rule with 0 premises—because they correspond to terms to be erased, that are not evaluated in CbNeed. For any term \(t\), indeed, one can for instance derive the following derivation \(\varPhi \):

Note that introducing \({} \vdash ^{(0,1)} x \,{:}\,\mathbf {0}\) with rule \(\mathsf {ax} \) rather than via \(\mathsf {many} _0\) (the typing context \(x\,{:}\,\mathbf {0}\) is equivalent to the empty type context) would give a derivation with final judgement \({} \vdash ^{(1,1)} (\lambda x.{x}) t \,{:}\,\mathbf {0}\)—thus, the system messes up both indices.

Such bad derivations of \(\mathbf {0}\) are not a problem per se, because in CbNeed one expects correctness and completeness to hold only for derivations of non-empty multi types. However, they do mess up also derivations of non-empty multi types because they can still appear inside tight derivations, as sub-derivations of sub-terms to be erased; consider for instance:

The term normalises in just 1 \({\mathtt m}_\mathrm{need}\)-step to \(I [y{\leftarrow }(\lambda x.{x}) t]\) but the multiplicative index of the derivation is 2. The mismatch is due to a bad derivation of \(\mathbf {0}\) used as right premise of an \(\mathsf{app} \) rule. Similarly, the induced typing of \(I [y{\leftarrow }(\lambda x.{x}) t]\) is an example of a bad derivation used as right premise of a rule \(\mathsf{ES} \):

The Actual Type System. Our solution to such an issue is to modify the system as to avoid derivations of \(\mathbf {0}\) to appear as right premises of rules \(\mathsf{app} \) and \(\mathsf{ES} \). We follow the schema of the rules for counting erasing steps given right after Theorem 2.

Therefore, we add two dedicated rules \(\mathsf{app} _{\text {gc}} \) and \(\mathsf{ES} _{\text {gc}} \), and constrain the right premise of rules \(\mathsf{app} \) and \(\mathsf{ES} \) to have a non-empty type. The system is in Fig. 4 and it is based on the same grammar of types of the naïve system. Note that rules \(\mathsf {many} \) and \(\mathsf {ax} \) can still introduce \(\mathbf {0}\). These \(\mathbf {0}\)s, however, can no longer mess up the indices of tight derivations, as we are going to show.

Note that the indices \(m\) and \(e\) are incremented and summed exactly as in the CbN and CbV type systems.

Remarkably, the technical development to prove correctness and completeness of the CbNeed type system with respect to CbNeed evaluation follows smoothly along the same lines of the two other systems, mutatis mutandis.

CbNeed Erases Wisely. In the literature, the theorem about CbNeed is the fact that it is operationally equivalent to CbN. This result was first proven independently by two groups, Maraist, Odersky, and Wadler [48], and Ariola and Felleisen [11], in the nineties, using heavy rewriting techniques.

Recently, Kesner gave a much simpler proof via CbN multi types [40]. She uses multi types to first show termination equivalence of CbN and CbNeed, from which she then infers operational equivalence. Termination equivalence means that a given term terminates in CbN if and only if terminates in CbNeed, and it is a consequence of our slogan that CbN and CbNeed both erase wisely.

With our terminology and notations, Kesner’s result takes the following form.

Note that, with respect to the other similar theorems in this paper, the result does not cover tight derivations and it does not provide exact bounds. In fact, the CbN system cannot provide exact bounds for CbNeed, because it does provide them for CbN evaluation, that in general is slower than CbNeed. Consider for instance the term \(t\) in Example 1 and its CbN tight derivation in Example 2: the derivation provides indices (5, 5) for \(t\) (and so \(t\) evaluates in 10 CbN steps), but \(t\) evaluates in 8 CbNeed steps. Closing such a gap is the main motivation behind this paper, achieved by the CbNeed multi type system in Sect. 6.

CbNeed Duplicates Wisely. Curiously, in the literature there are no dual results showing that CbNeed duplicates as wisely as CbV. One of the reasons is that it is a theorem that does not admit a simple formulation such as operational or termination equivalence, because CbNeed and CbV are not in such relationships. Morally, this is subsumed by the logical interpretation according to which CbNeed corresponds to an affine variant of the linear logic representation of CbV. Yet, it would be nice to have a precise, formal statement establishing that CbNeed duplicates as wisely as CbV—we provide it here.

Our result is that the CbV multi type system is correct with respect to CbNeed evaluation. In particular, the indices \((m, e)\) provided by a CbV type derivation provide bounds for CbNeed evaluation lengths. Two important remarks before we proceed with the formal statement:CbV Correctness with Respect to CbNeed. Pleasantly, our presentations of CbV and CbNeed make the proof of the result straightforward. It is enough to observe that, since we do not consider garbage collection and we adopt a non-deterministic formulation of CbV, CbNeed is a subsystem of CbV. Formally, if \(t \ {\xrightarrow {}}{}_{{\mathrm{need}}}^{} s\) then \(t \ {\xrightarrow {}}{}_{{\mathrm{cbv}}}^{} s\), as it is easily seen from the definitions (CbNeed reduces only some subterms of applications and ES, while CbV reduces all such subterms). The result is then a corollary of the correctness theorem for CbV.

Since the CbNeed system provides exact bounds (Theorem 5), we obtain that CbNeed duplicates as wisely as CbV, when the comparison makes sense, that is, on CbV normalisable terms.

The technical development is simple, and uniform with respect to those of CbN and CbV multi type systems. The typing rules count evaluation steps following exactly the same schema of the CbN and CbV rules. The proofs of correctness and completeness also follow exactly the same structure.

A further side contribution of the paper is a new fundamental result of CbNeed, formally stating that it duplicates as wisely as CbV. More precisely, the CbV multi type system is (quantitatively) correct with respect to CbNeed evaluation. Pleasantly, our presentations of CbV and CbNeed provide the result for free. This result dualizes the other fundamental theorem stating that CbNeed erases as wisely as CbN, usually formulated as termination equivalence, and recently re-proved by Kesner using CbN multi types [40].

Future Work. Recently, Barenbaum et al. extended CbNeed to strong evaluation [14], and it is natural to try to extend our type system as well. The definition of the system, in particular the extension of tight derivations to that setting, seems however far from being evident. Barembaum, Bonelli, and Mohamed also apply CbN multi types to a CbNeed calculus extended with pattern matching and fixpoints [15], that might be interesting to refine along the lines of our work.

An orthogonal direction is the study of the denotational models of CbNeed. It would be interesting to have a categorical semantics of CbNeed, as well as a categorical way of discriminating our quantitative precise model from the quantitatively lax one given by CbN multi types. It would also be interesting to obtain game semantics of CbNeed, hopefully satisfying a strong correspondence with our multi types in the style of what happens in CbN [30, 31, 51, 56].

A further, unconventional direction is to dualise the inception of the CbNeed type system trying to mix silly duplication from CbN and silly erasure from CbV, obtaining—presumably—a multi types system measuring a perpetual strategy.