The goal of this lecture note is to review parameter-passing strategies (call by value, call by name, and call by need) and what happens when these strategies are used for data constructors.
The evaluation of x in an environment E that binds names to denotations reduces to the result of looking up for x in E.
For example,
Consider the following (function) application:
e0 e1
In this application,
The evaluation of e0 e1 in an environment E that binds names to denotations amounts to the application of the evaluation of e0 in E to the evaluation e1 in E, a.k.a. the “actual parameter”.
There are two cases – either the evaluation of e0 in E yields a predefined function, or it yields a user-defined function:
if the evaluation of e0 in E yields a predefined function, then the evaluation e0 e1 in E is achieved by applying this predefined function to the actual parameter;
if the evaluation of e0 in E yields a user-defined function, then this user-defined function is the result of the evaluation of a function abstraction fun x1 => e0' in an environment E'; in this function abstraction, x1 is known as its “formal parameter” and e0' is known as its “body”;
then the evaluation of e0 e1 in E is achieved by applying this user-defined function (i.e., the result of evaluating fun x1 => e0' in E') to this actual parameter (i.e., the result of evaluating e1 in E), which reduces to evaluating the body of this user-defined function (i.e., e0') in an extension of E' that binds the formal parameter (i.e., x1) to the actual parameter;
more succinctly, if evaluating e0 in E yields the result of evaluating fun x1 => e0' in E', then evaluating e0 e1 in E reduces to evaluating e0' in an extension of E' that binds x1 to the evaluation of e1 in E.
The previous section described what happens when an application is evaluated. The present section describes when actual parameters are evaluated.
In call by value, the actual parameters are evaluated before the function is applied. The environment then maps names to values, and looking up for a name yields one of these values.
So for example, if Gallina followed call by value, the evaluation of (fun x1 => 0 + 0) (2 + 3) in an environment E would reduce to evaluating 0 + 0 in an extension of E that binds x1 to 5, which is the result of evaluating 2 + 3 in E.
In OCaml, a call-by-value language that unlike Gallina is not a pure language, the evaluation of (fun x1 => 0 + 0) (0 / 0) in an environment E yields a “division by zero” error. (Truth be told, it yields a syntax error since the expression is written in Gallina, not in OCaml, but we are arguing semantics here, not syntax.)
For another example, if Gallina followed call by value, the evaluation of (fun x1 => x1 + x1) (2 + 3) in an environment E would reduce to evaluating x1 + x1 in an extension of E that binds x1 to 5. Then x1 would be evaluated twice in this extended environment, each time yielding 5.
In call by name, the actual parameters are not evaluated before the function is applied. The environment then maps names to computations, and looking up for a name triggers one of these computations.
So for example, if Gallina followed call by name, the evaluation of (fun x1 => 0 + 0) (2 + 3) in an environment E would reduce to evaluating 0 + 0 in an extension of E that binds x1 to the evaluation of 2 + 3 in E.
In Haskell, a call-by-name language, the evaluation of (fun x1 => 0 + 0) (2 / 0) in an environment E yields 0. (Again, truth be told, it yields a syntax error since the expression is written in Gallina, not in Haskell, but we are still arguing semantics here, not syntax.)
For another example, if Gallina followed call by name, the evaluation of (fun x1 => x1 + x1) (2 + 3) in an environment E would reduce to evaluating x1 + x1 in an extension of E that binds x1 to the evaluation of 2 + 3 in E. Then x1 would be evaluated twice in this extended environment, each time triggering the evaluation of 2 + 3 in E.
Call by need is an optimization of call by name where the result of evaluating an actual parameter for the first time is “memoized” (i.e., somehow recorded), and any subsequent evaluation of this actual parameter yields the result of this memoization.
So for example, if Gallina followed call by need, the evaluation of (fun x1 => x1 + x1) (2 + 3) in an environment E would reduce to evaluating x1 + x1 in an extension of E that binds x1 to the evaluation of 2 + 3 in E. The first time x1 is evaluated in this extended environment, it triggers the evaluation of 2 + 3 in E, the result of which is memoized. So henceforth x1 denotes 5 in the extended environment, and the second time x1 is evaluated in this extended environment, looking up for it directly yields 5.
Since Gallina is pure and total, as users, we cannot observe which parameter-passing strategy its implementation uses.
In call by name, if the formal parameter of a function is not evaluated in its body, the corresponding actual parameter is not evaluated. Conversely, an actual parameter is only evaluated when the formal parameter of a function is evaluated in its body.
So in call by name, computation is demand-driven, and so call-by-name programming languages are said to be “lazy” since they only compute actual parameters if the corresponding formal parameter is evaluated.
And in call by value, computation is not demand-driven, and so call-by-value programming languages are said to be “eager” since they compute actual parameters regardless of whether the corresponding formal parameter will be evaluated.
So far, we have implicitly assumed that the parameter-passing strategy for data constructors is call by value. Our data structures were constructed inductively and therefore we could traverse them recursively and eagerly using recursive functions that are declared with Fixpoint, and we could reason about these traversals using induction.
Now suppose that the parameter-passing strategy for data constructors is call by name. Then our data structures are not constructed inductively, since the arguments of their constructors is not evaluated yet – and perhaps never will.
These data structures are said to be constructed coinductively, and in Gallina, they are declared with the keyword CoInductive.
Likewise, coinductive data are traversed “corecursively” and lazily using corecursive functions that are declared with CoFixpoint, and we can reason about these traversals using “coinduction”.
Coinduction is the topic for another chapter next week. The next sections are dedicated to declaring coinductive data structures and programming corecursive functions for traversing these coinductive data structures, lazily, and the next chapter is dedicated to perhaps the most well-known lazy data structure: streams.
To illustrate, here is a declaration for lazy polymorphic binary trees with payloads in the leaves:
CoInductive lazy_binary_tree (V : Type) : Type :=
LLeaf : V -> lazy_binary_tree V
| LNode : lazy_binary_tree V -> lazy_binary_tree V -> lazy_binary_tree V.
And here is the declaration of a mirroring function over lazy binary trees:
CoFixpoint lazy_mirror (V : Type) (lt : lazy_binary_tree V) : lazy_binary_tree V :=
match lt with
LLeaf _ v =>
LLeaf V v
| LNode _ lt1 lt2 =>
LNode V (lazy_mirror V lt2) (lazy_mirror V lt1)
end.
Gallina enforces structural recursion by only allowing recursive calls over structurally smaller parts of the input. Likewise, it enforces structural corecursion by only enabling corecursive calls as arguments of a lazy data constructor.
As illustrated above, it is pretty direct to declare the type of lazy polymorphic binary trees with payloads in the leaves and to implement the corresponding lazy mirror function. And as illustrated in the accompanying .v file, it is just as direct to declare the type of lazy Peano numbers and to implement the corresponding lazy addition function. Implementing a function to compute the lazy number of leaves or the lazy number of nodes of a lazy binary tree, not so much. C’est la vie.