Lecture Notes onCall-by-Need and Futures15-312: Foundations of Programming LanguagesFrank PfenningLecture 22November 16, 2004In this lecture we first examine a technique to specify the operational se-mantics for call-by-need, sometimes called lazy evaluation. This is an imple-mentation technique for a call-by-name semantics that avoids re-evaluatingexpressions multiple times by memoizing the result of the first evaluation.Then we use a similar technique to specify the meaning of futures, a con-struct that introduces parallelism into evaluation. Futures were first devel-oped for Multilisp, a dynamically typed, yet statically scoped version ofLisp specifically designed for parallel computation. A standard referenceon futures is:Robert H. Halstead, Jr. Multilisp: A language for concurrentsymbolic computation. ACM Transactions on Programming Lan-guages and Systems, 7(4):501-538, October 1985.One advantage of call-by-name function application over call-by-valueis that it avoids the work of evaluating the argument if it is never needed.More broadly, lazy constructors avoid work until the data are actually used.In turn, this has several drawbacks. One of them is that the efficiency modelof such a language is more difficult to understand than for a call-by-valuelanguage. The second is that lazy constructors introduce infinite values ofdata types which complicate inductive reasoning about programs. How-ever, the most obvious problem is that if an expression is used several timesit will be computed several times unless we can find an implementationtechnique to avoid this.There are two basic approaches to avoid re-evaluation of the argumentof a function application. The first is to analyze the function body to de-termine if the argument is really needed. If so, we evaluate it eagerly andLECTURE NOTES NOVEMBER 16, 2004L22.2 Call-by-Need and Futuresthen work with the resulting value. This is semantically transparent, butthere are many cases where we cannot tell statically if an argument will beneeded. The other is to create a so-called thunk1and pass a reference tothe thunk as the actual argument. When the argument is needed we eval-uate the thunk and memoize the resulting value. Further reference to thethunk now just returns the value instead of evaluating it again. Note thatthis strategy is only a correct implementation of call-by-name if there areno effects in the language (or, if there are effects, they are encapsulated in amonad).We can think of a thunk as a reference that we can write only once (thefirst time it is accessed) and henceforth will continue to be the same value.So our semantic specification for call-by-need borrows from the ideas inthe operational semantics of mutable references. We generalize the basicjudgment e 7→ e0to hH, ei 7→ hH0, e0i where H and H0contains all thunks,and e and e0can refer to them by their labels.Thunks H : : = · | H, l=eNote thunks may be expressions; after they have been evaluated thefirst time, however, they will be replaced by values. First, the rules forcall-by-name application.hH, e1i 7→ hH0, e01ihH, apply(e1, e2)i 7→ hH0, apply(e01, e2)ihH, apply(fn(x.e1), e2)i 7→ h(H, l=e2), {l/x}e1iIn the second rule, the label l must be new with respect to H. When thevalue of l is actually accessed, we need to force the evaluation of the thunkand then record that value.h(H1, l=e, H2), ei 7→ h(H01, l=e∗, H02), e0ih(H1, l=e, H2), li 7→ h(H01, l=e0, H02), liv valueh(H1, l=v, H2), li 7→ h(H1, l=v, H2), viNote that in the first rule, the result e∗must actually be equal to e. If itwere not, that means the evaluation of e would actually require the thunk1The name is a whimsical past tense of think derived from “something that has beenthought of before”.LECTURE NOTES NOVEMBER 16, 2004Call-by-Need and Futures L22.3l, which would lead to an infinite loop. This particular form of infinite loopis called a black hole can be detected, while other forms of non-terminationremain.It is left as an exercise to extend the statements of progress and preserva-tion, or to show in which sense the call-by-name semantics coincides withthe call-by-need semantics. Note also that there are other rules that can cre-ate thunks: essentially every time we need to substitute for a variable. Weshow one of these cases, namely recursion.hH, rec(x.e)i 7→ h(H, l={l/x}e), liAs an example of a black hole, consider fix f.f. As an example of an expres-sion that is not a black hole, yet fails to terminate consider (fix f.λy.f (y +1)) 1. It is instructive to simulate the execution of this expression.h·, (fix f.λy.f (y + 1))1i7→ h(l = λy.l (y + 1)), l 1i7→ h(l = λy.l (y + 1)), (λy.l(y + 1)) 1i7→ h(l = λy.l (y + 1), l1= 1), l (l1+ 1)i7→ h(l = λy.l (y + 1), l1= 1), (λy.l(y + 1)) (l1+ 1)i7→ h(l = λy.l (y + 1), l1= 1, l2= l1+ 1), l (l2+ 1)i7→ . . .In order to detect black holes and take appropriate action we wouldallow thunks of the form l=• and replace the first rule byh(H1, l=•, H2), ei 7→ h(H01, l=•, H02), e0ih(H1, l=e, H2), li 7→ h(H01, l=e0, H02), lih(H1, l=•, H2), li 7→ h(H1, l=•, H2), BlackHoleiwhere BlackHole is a new error expression that must be propagated to thetop level as shown in a previous lecture on run-time exceptions and errors.Futures. Next we consider futures. The idea is that an expression future(e)spawns a parallel computation of e while returning immediately a pointerto the resulting value. If the resulting value is ever actually needed we saywe are touching the future. When we touch the future we block until theparallel computation of its value has succeeded. However, in most situa-tions we can pass around the future, construct bigger values, etc.LECTURE NOTES NOVEMBER 16, 2004L22.4 Call-by-Need and FuturesThere are two principal differences to call-by-need as shown above. Thefirst is that a future is treated as a value. This is important because unlike incall-by-need, we are here in a call-by-value setting. Secondly, the computa-tion of the future may proceed asynchronously, instead of being completedin full exactly the first time it is accessed. However, it is similar in the sensethat once a future has been computed, its value is available everywhere itis referenced.The typing rule for futures in source programs is exceedingly simple,since we consider futures related only to how a program executes (sequen-tially or in parallel), but not what it computes.Γ ` e : τΓ ` future(e) : τProcess labels l that arise during