The goal of this lecture note is to describe demand-driven computation and how to express it in OCaml.
OCaml provides language support for demand-driven computation (a.k.a. laziness) in the form of
These built-in tools do not only provide laziness, as in call by name, they also provide memoization, as in call by need: the first time a delayed expression is evaluated, the resulting value is recorded and subsequently reused if the delayed expression is re-evaluated.
Let us illustrate this point with the tracing identify function for integers:
let an_int n =
let () = Printf.printf "processing %d...\n" n
in n;;
If we delay the application of an_int to an integer, its trace is not emitted until the first time the corresponding suspended computation is triggered. Henceforth this suspended computation is completed, no matter how many times we attempt to trigger it:
# let thirty_three = lazy (an_int 33);;
val thirty_three : int lazy_t = <lazy>
# thirty_three;;
- : int lazy_t = <lazy>
# Lazy.force thirty_three;;
processing 33...
- : int = 33
# Lazy.force thirty_three;;
- : int = 33
# Lazy.force thirty_three;;
- : int = 33
# thirty_three;;
- : int lazy_t = lazy 33
#
Conversely, if a computation is suspended and not triggered, it does not take place:
# let _ = lazy (an_int 100) in 10;;
- : int = 10
# (fun _ -> 10) (lazy (an_int 100));;
- : int = 10
#
Furthermore, demands can be nested.
In the following example, z denotes a suspended computation that, when triggered, triggers the suspended denotation denoted by y, which in turn triggers the suspended denotation denoted by x:
let add n1 n2 =
let () = Printf.printf "adding %d to %d...\n" n1 n2
in n1 + n2;;
let x = lazy (an_int 1);;
let y = lazy (add (Lazy.force x) (an_int 10));;
let z = lazy (add (Lazy.force y) (an_int 100));;
Step by step,
forcing z triggers the evaluation of add (Lazy.force y) (an_int 100);
evaluating add (Lazy.force y) (an_int 100) emits "processing 100..." and then forces y;
forcing y triggers the evaluation of add (Lazy.force x) (an_int 10);
evaluating add (Lazy.force x) (an_int 10) emits "processing 10..." and then forces x;
forcing x triggers the evaluation of an_int 1;
1 is memoized in the denotation of x and is returned;
add is called, which emits adding 1 to 10..., adds 1 to 10, and returns 11;
11 is memoized in the denotation of y and is returned;
add is called, which emits adding 11 to 100..., adds 11 to 100, and returns 111;
111 is memoized in the denotation of z and is returned.
Henceforth, any further forcing of z, y, and x will yield 111, 11, and 1, silently:
# Lazy.force z;;
processing 100...
processing 10...
processing 1...
adding 1 to 10...
adding 11 to 100...
- : int = 111
# Lazy.force z;;
- : int = 111
# Lazy.force y;;
- : int = 11
# Lazy.force x;;
- : int = 1
#
In the following analogous example, c denotes a suspended computation that, when triggered, triggers the suspended denotation denoted by b, which in turn triggers the suspended denotation denoted by a:
let a = lazy (an_int 1);;
let b = lazy (add (Lazy.force a) (an_int 10));;
let c = lazy (add (Lazy.force b) (an_int 100));;
The original example had x instead of a, y instead of b, and z instead of c, and we forced z.
Here, let us first force b twice in a row, and then a, and then c twice in a row:
# Lazy.force b;;
processing 10...
processing 1...
adding 1 to 10...
- : int = 11
# Lazy.force b;;
- : int = 11
# Lazy.force a;;
- : int = 1
# Lazy.force c;;
processing 100...
adding 11 to 100...
- : int = 111
# Lazy.force c;;
- : int = 111
#
Analysis:
forcing b triggers the evaluation of add (Lazy.force a) (an_int 10);
evaluating add (Lazy.force a) (an_int 10) emits processing 10... and then forces a;
forcing a triggers the evaluation of an_int 1;
1 is memoized in the denotation of a and is returned;
add is called, which emits adding 1 to 10..., adds 1 to 10, and returns 11;
11 is memoized in the denotation of b and is returned;
forcing b yields the memoized result of evaluating add (Lazy.force a) (an_int 10), i.e., 11 and is returned;
forcing a yields the memoized result of evaluating an_int 1, i.e., 1 and is returned;
forcing c triggers the evaluation of add (Lazy.force b) (an_int 100);
evaluating add (Lazy.force b) (an_int 100) emits "processing 100..." and then forces b;
add is called, which emits adding 11 to 100..., adds 11 to 100, and returns 111;
111 is memoized in the denotation of c and is returned.
forcing c yields the memoized result of evaluating add (Lazy.force b) (an_int 100), i.e., 111 and is returned.
To sum up:
Harald: I kind of like this idea of demand-driven computation. It sounds economical.
Loki: Actually, that’s how I read the lecture notes, and yes, it is economical.
Harald: Beg pardon? That’s how you read the lecture notes?
Loki: Well yes: I first look at the mandatory exercises. If there isn’t any, then there is no need to read the lecture note, which is a big time saver, considering how many other lectures I am following this term.
Harald (stunned): You don’t read the lecture note? But what if there is a question about it at the exam?
Loki (definite): There can’t be any, because thanks to modern teaching methods, the exam has to be aligned with the mandatory exercises. If we don’t have a mandatory exercise about something, that something cannot be at the exam.
Harald (appalled): That simple, eh. OK... After all, most lecture notes do have mandatory exercises.
Loki: Yes they do. But the demand-driven idea still applies: I look at the mandatory exercises, and if I can solve them there and then, I am done, which is good because remember the many other lectures I am following this term?
Harald (floundering): But er... Does that happen often? I mean can you solve the mandatory exercises without reading the lecture note? These exercises are supposed to test our understanding of the material presented in the lecture note.
Loki (sauntering): Right, and that’s where the demand-driven idea is useful: you identify what you don’t know in the exercise, and then you grope for it in the lecture notes. Usually you find what you need a bit before the text of the exercise. And then you’re done.
Harald: And what if what you need requires something that was explained much earlier in the note?
Loki: Harald, that’s exactly the idea of being demand-driven: every time you find something you don’t know, you look earlier in the note. Just use the search facility of your browser, and look backward.
Harald: Usually I use the index for that.
Loki: Right. Because not everything is defined earlier in the current lecture note: some things are defined in a previous lecture note. If you have already read the definition in that other lecture note, you are done. If you haven’t, then you go read it. If you find it unclear, it always comes with some examples: read them too. And if you find something else you don’t know, keep looking backward for definitions until you find one you have read already. I tell you, demand-driven reading is a great idea. Going forward and only looking backward when you need it is so much quicker. Quite many times you don’t need to look backward at all.
Harald: But aren’t you missing, like, the narrative, and the side notes? Do you even follow the Wikipedia pointers?
Life can only be understood backward;but it must be lived forward.
Loki: Details, Harald, details. Don’t mind the small stuff: go forward and only look backward if it is needed.
Brynja (jumping in): I’d rather mind. These particular lecture notes are not the Internet: they are constructed inductively and so they are made to be read forward, even though they come with an index for direct access.
Loki (astute): But then it shouldn’t make any difference if you read them forward or backward, should it? If the lecture notes are well written, then you and I will learn just as much. I’d rather first see why we need to learn what we are instructed to learn.
Brynja: True. But still, the exercises in the lecture notes are part of the lecture notes, so they don’t tell you why we need to learn what we are instructed to learn – and neither does the exam. We will only realize that once this course is over. If we need it then, then we’ll already know it: learn now, know later.
Loki: Forewarned is forearmed, for sure. But if we don’t need it?
Culture is what remainswhen you have forgotten everything.
Brynja: Even so. Someone who graduated is supposed to have a modicum of, you know, knowledge? And meanwhile they should, like, study?
Loki: Brynja, you are so driven.
Brynja: Thank you – I guess. My point is that when possible, we should not only be driven by necessity, especially if it is for the short term only.
Loki (teasingly): You mean it’s not sufficient to be driven by necessity?
Brynja (tit for tat): You mean you don’t want to drive your life at all? It’s your call.
Loki (splendidly): And it is a call by need: we only live once.
Alfrothul (whispering to Harald): Loki has read the previous lecture note, the one about Call by need.
Harald (whispering back): Naah – one of the people in his group solved Exercise 2 and now he is bragging about it.
Do you feel Loki?
Harald: So, from now on, we should identify what we don’t know in each exercise, and then grope the lecture notes.
Vigfus (unsure): grope?
Alfrothul (soberly): grep.
Vigfus (looking at Alfrothul sideways): Hum. Unix much?
Ken Thompson: You guys need a chairperson?
Mimer: Mr. Thompson, thanks for stopping by!
Removed the mention of the resource file, since there isn’t any, thanks to Syed Muhammad Maaz’s eagle eye [26 Mar 2020]
Added the post-postlude [14 Sep 2019]
Fixed a typo in the narrative, thanks to Yunjeong Lee’s eagle eye [11 Jun 2019]
Adjusted the summary [17 Apr 2019]
Added the examples [12 Apr 2019]
Added the postlude [10 Apr 2019]
Created [28 Mar 2019]