add sentence about Identity Monad
[lambda.git] / topics / _week7_interpreter_exposition.mdwn
1 A program that interprets untyped lambda terms (and more)
2 =========================================================
3
4 Let's start with an OCaml datatype for untyped lambda terms:
5
6     type identifier = string
7     type term =
8       | Var of identifier
9       | App of term * term
10       | Lambda of identifier * term
11
12 Some examples of `term`s are:
13
14     Var "x"
15     App(Var "x", Var "y")
16     App(Lambda("x",Var "x"), Var "y")
17
18 We're going to want to design an _interpreter_ program that will reduce or evaluate the final term down to:
19
20     Var "y"
21
22 It would be nice if it also knew how to display that in the more user-friendly format:
23
24     y
25
26 And it would be doubly-specially nice if we didn't have to type our input in the long explicit OCaml notation, but could instead just write:
27
28     (\x.x) y
29
30 and behind the scenes that got converted into:
31
32     App(Lambda("x",Var "x"), Var "y")
33
34 which is what the functions of our interpreter program have to deal with.
35
36 You're going to work with a program skeleton where these extra nice features are built in to the infrastructure. It will only be the core reduction or evaluation functions that you need to complete, to get us from:
37
38     App(Lambda("x",Var "x"), Var "y")
39
40 to:
41
42     Var "y"
43
44 As long as we're at it, why don't we make out language a bit more full-featured. We could throw in `let`-terms and `if-then`-terms, too:
45
46     type term =
47       | Var of identifier
48       | App of term * term
49       | Lambda of identifier * term
50       | Let of identifier * term * term
51       | LetRec of (identifier * term) list * term
52       | If of term * term * term
53
54 We're not actually going to implement `LetRec` in this exercise; that's just there as a placeholder for later. 
55
56 Perhaps also some boolean and number constants:
57
58     type literal = Bool of bool | Num of int
59     type term =
60       ...
61       | Literal of literal
62
63 But then once we have those, we are going to want to have some primitive operations to deal with them. Otherwise they'll just be black boxes that we can only pass around, without ever inspecting or making differentiated use of. Thus we might want operations like `zero?` and `pred` for numbers, `not` for negation, and so on. Long story short, we are going to want some *primitive functions*, some *constructors* (like `cons` and `[]` were for lists), and some *deconstructors* or operations appropriate to those constructors (these were `head` and `tail` for lists). Thus our fleshed-out datatype might look like this:
64
65     type term =
66       | Var of identifier
67       | App of term * term
68       | Lambda of identifier * term
69       | Let of identifier * term * term
70       | LetRec of (identifier * term) list * term
71       | If of term * term * term
72       (* Constants, functional and otherwise *)
73       | Primfun of primfun
74       | Constructor of constructor
75       | Destructor of destructor
76       | Literal of literal
77
78 The official term for operations like `head` and `tail` is "deconstructor", not "destructor", but the latter is shorter and more fun to type. In the exercises that follow, the tricky parts that deal with the `Primfun`s and `Constructor`s and `Destructor`s and `Literal`s will always already be supplied for you. You'll just need to think about the `Var`s and `App`s and `Lambda`s and `Let`s and `If`s.
79
80 We're going to explore how to implement the interpreter using two different methods. One is a translation of the method Chris demonstrated for combinatorial logic over to the lambda calculus. You check if any part of a term is reducible, and keep repeating single-step reductions until you can't find any more eligible redexes. The second method works a bit differently. You can begin by thinking of it an improvement on the first method, that tries to get by without having to do all the laborious substitutions that reducing again and again would entail. But its virtues will be more than merely ones of efficiency. It will also start to look a lot more like the kinds of semantics, using assignment functions, that we're more familiar with as formal semanticists. In programming circles, assignment functions are called "environments" and we'll use that terminology here. So the two methods we're going to look at will be, first, a reduce-and-repeat interpreter; and second, an environment-based one.
81
82 Now you could just work this out on paper. That's fine, and will save you some complications. But it will be more fun for you to play with an actual computer implementation. Plus then you will get the benefits of user-friendly input and user-friendly printing of the results.
83
84 But these benefits come at a price. The actual code you're going to look at has some complexity to it. 
85
86 The skeleton program we'll be providing you with is based on source code accompanying Pierce's excellent book _Types and Programming Languages_. (In particular, the files here <http://www.cis.upenn.edu/~bcpierce/tapl/checkers/fulluntyped/>.) We aggressively modified that code to suit our somewhat different needs (and taste). Notably, Pierce's code only provides a reduce-and-repeat interpreter; so part of our refactoring was to make it easier to switch back and forth between that and an environment-based interpreter.
87
88 Now part of the complexity of this can be factored out into extra files that you can just ignore, and we've tried to organize the code to maximize that. But sadly, some of the complexity inevitably ends up polluting our nice simple datatype. We're going to explain where this pollution comes from, in the hope that then you'll be able to see through it to the simple underlying form, that we displayed above.
89
90 A **first source of complexity** is that we want to get friendlier error messages, for example if we run the interpreter on a file `./input` that contains:
91
92     let x = 3 in x + y
93
94 The interpreter will complain:
95
96     ./input:1.17: Unbound variable `y`
97
98 What this means is that while processing the file `./input`, after character 17 on line 1, something gave the interpreter indigestion, and its particular complaint is that it encountered an ``Unbound variable `y` ``. When the code you're feeding the interpreter is non-trivial, it's very helpful to get this kind of information about where in the file the error originated from. But to keep track of that, our datatype has to get messier. We'll have some extra information (we'll call it `info`, don't worry about its internal structure) associated with each term (and subterm) that we're handling. And so our datatypes will look instead like this:
99
100     type bare_term =
101       | Var of identifier
102       ...
103     type term = info * bare_term
104
105 And when we pattern match on the (full, annotated) terms, our code will look like this:
106
107     match term with
108     | _,Var ident -> ...
109     ...
110
111 with the extra `_,` at the start of the pattern to catch and discard the extra information about where the term came from. In some cases we need to retain that information instead of discarding it, so the code will instead look like this:
112
113     match term with
114     | fi,Var ident -> ...
115     ...
116
117 using the variable `fi` for the "source file info".
118
119 A **second complication** has to do with the distinction between `term`s in general and what we want to count as `result`s of our computations.
120
121 In these exercises, unlike the combinatorial logic ones, we are only going to work with "call-by-value" interpreters. That is, we will only apply functions (whether primitives or those expressed by Lambdas) to what we deem as "value"s or "result"s. At a minimum, these must be terms that it is not possible to reduce further. So `1` and `\x. x` count as values. But we will also legislate that terms like `1 (\x. x)`, though non-reducible (our booleans and numbers won't be Church functions, but rather will be non-functional atoms), count as "stuck" and so aren't results either. (As suggested in class, you can think of "stuck" terms as representing or being crashed computations.)
122
123 As a result of never applying functions to non-results, non-results will never get bound to any variables, either.
124
125 Now in the V1/reduce-and-repeat part of the exercise, results will simply be a proper subset of our terms. They will be abstracts, plus literals and all the other primitives. They won't include free/unbound variables. We'll count those as "stuck" or crashed computations, too. (But _bound_ variables are okay, because they'll always be bound to results.)
126
127 However, when we move to the V2/environment-based interpreter, we will need to introduce some results that aren't (just) terms, called `Closure`s. We'll discuss these later; but the upshot is that we're going to need eventually to work with code where the result datatype and the term datatype may be partly disjoint. So we are going to need two parallel datatypes:
128
129     type bare_term =
130       | TermVar of identifier
131       | TermApp of term * term
132       | TermLambda of identifier * term
133       | TermLet of identifier * term * term
134       | TermLetRec of (identifier * term) list * term
135       | TermIf of term * term * term
136       (* Constants, functional and otherwise *)
137       | TermPrimfun of primfun
138       | TermConstructor of constructor
139       | TermDestructor of destructor
140       | TermLiteral of literal
141     type term = info * bare_term
142
143     type bare_result =
144     (*| Symbol of ... *)
145     (*| Closure of ... *)
146       | ResLambda of identifier * term
147       | ResPrimfun of primfun
148       | ResConstructor of constructor
149       | ResDestructor of destructor
150       | ResLiteral of literal
151     type result = info * bare_result
152
153
154 We'll explain the `Symbol` and `Closure` variants on the `bare_result` datatype below.
155
156 Having these two parallel datatypes is rather annoying, and requires us to insert some translation functions `term_of_result` and `result_of_term` at a few places in the program. But the core, non-fancy parts of OCaml don't supply any more elegant way to specify that one datatype is a subtype of another, so this is simply what we'll need to do.
157
158 A **third complication** has to do with environments. On the one hand, we don't have any really compelling need for environments in the first phase of the exercise, when we're just making a reduce-and-repeat interpreter. They don't play any role in the fundamental task we're focusing on. But on the other hand, weaving environments into the system when we *will* need them, for the second phase of the exercise, is not simple and would require lots of code changes. So that is a reason to include them from the beginning, just off to the side not doing any important work until we want them.
159
160 And as long as we've got them at the party, we might just as well give them _something_ to do. Pierce's original code takes a source file, which it expects to contain a sequence of terms or other toplevel declarations separated by semicolons, and prints out the result of maximally reducing each of the terms. Note I said "or other toplevel declarations." In addition to terms like this:
161
162     1 + 2;
163     let x = 1 in x + 2
164
165 that code also accepted toplevel declarations like this:
166
167     let y = 1 + 2 end
168
169 which means that we should reduce the rhs `1 + 2`, and *save* the result to be used for any locally-unbound occurrences of `y` in later terms. If the interpreter encounters *other* locally-unbound variables, where no such toplevel binding has been established, it will fail with an error. Thus:
170
171     let y = 1 + 2 end;
172     let x = 0 in (x,y)
173
174 will evaluate to `(0,3)`, but:
175
176     let y = 1 + 2 end;
177     let x = 0 in (x,w)
178
179 will crash, because `w` has no result bound to it. Note that you can locally rebind variables like `y` that have toplevel bindings. Thus:
180
181     let y = 1 + 2 end;
182     (y, (let y = 0 in y))
183
184 evaluates to `(3,0)`. (You have to enclose the `let y = 0 in y` in parentheses in order to embed it in terms like the pair construction `(_, _)`.)
185
186 Note that what I'm writing above isn't the syntax parsed by Pierce's actual program. He uses a syntax that would be unfamiliar to you, so we've translated his code into a more local dialect; and the above examples are expressed using that dialect.
187
188 Pierce's code had a second kind of toplevel declaration, too, which looks like this (in our dialect, not his):
189
190     symbol w;
191     let x = 0 in (x,w)
192
193 Now that won't crash, but will instead evaluate to `(0,w)`. The code now treats unbound occurrences of `w` as atomic uninterpreted symbols, like Scheme's `'w`. And these symbols do count as results. (They are also available to be rebound; that is, you are allowed to say `symbol w; let w = 0 in ...`. But perhaps we should prohibit that.)
194
195 So these two kinds of toplevel declarations are already handled by Pierce's code, in a form, and it seemed neatest just to clean them up to our taste and leave them in place. And environments are needed, even in the V1/reduce-and-repeat interpreter (which is all Pierce's code provides), to implement those toplevel declarations. But as I said before, you can for now just think of the environments as sitting in the sidelines. They aren't used in any way for interpreting terms like:
196
197     let y = 1 + 2 in
198     let x = y + 10 in
199     (x, y)
200
201 But now *what are* environments? In order to emphasize the essential commitments rather than any one particular implementation of environments, we're going to show you the general interface environments need to satisfy, and then show you a couple of different ways of implementing that interface. These will be just plug-and-play. You should be able to switch the implementations at will, and have everything work out the same.
202
203 TODO selecting an environment
204
205 Okay, that **completes our survey of the complications**.
206
207 The V1/reducuction-based interpreter
208 ------------------------------------
209
210 For phase 1 of this exercise, you're going to write a `reduce1` function that converts OCaml values like:
211
212     TermApp(TermApp(TermLambda("x", TermApp(Var "x", Var "y")), TermLambda("w", Var "w")), ...)
213
214 to:
215
216     TermApp(TermApp(TermLambda("w", Var "w"), Var "y"), ...)
217
218 The further reduction, to:
219
220     TermApp(Var "y", ...)
221
222 has to come from a subsequent re-invocation of the function.
223
224 Before we get down to business, let's think about how we will detect that the term has been reduced as far as we can take it. In the reduce-and-repeat interpreter Chris demonstrated for combinatorial logic, we had the `reduce1` function perform a single reduction *if it could*, and then it was up to the caller to compare the result to the original term to see whether any reduction took place. That worked for the example we had. But it has some disadvantages. One is that it's inefficient. Another is that it's sensitive to the idiosyncracies of how your programming language handles equality comparisons on complex structures; and these details turn out to be very complex and vary from language to language (and even across different versions of different implementations of a single language). We'd be glad to discuss these subtleties offline, but if you're not prepared to master them, it would be smart to foster an ingrained hesitation to blindly applying a language's `=` operator to complex structures. (Some problem cases: large numbers, set structures, structures that contain functions.) A third difficulty is that it's sensitive to the particular combinators we took as basic. With `S` and `K` and `I`, it can never happen that a term has been reduced, but the output is identical to the input. That can happen in the lambda calculus, though (remember `&omega; &omega;`); and it can happen in combinatorial logic if other terms are chosen as primitive (`W W1 W2` reduces to `W1 W2 W2`, so let them all just be plain `W`s).
225
226 So let's consider different strategies for how to detect that the term cannot be reduced any further. One possibility is to write a function that traverses the term ahead of time, and just reports whether it's already a result, without trying to perform any reductions itself. Another strategy is to "raise an exception" or error when we ask the `reduce1` function to reduce an irreducible term; then we can use OCaml's error-handling facilities to "catch" the error at an earlier point in our code and we'll know then that we're finished. Pierce's code used a mix of these two strategies.
227
228 What we're going to do instead is to have our `reduce1` function wrap up its output in a special datatype, that describes how that output was reached. That type looks like this:
229
230       type reduceOutcome = AlreadyResult of result | StuckAt of term | ReducedTo of term
231
232 That is, one possible outcome is that the term supplied is already a result, and so can't be reduced further for that reason. In that case, we use the first variant. We could omit the `of result` parameter, since the code that called `reduce1` already knows what term it was trying to reduce; but in some cases it's a bit more convenient to have `reduce1`  tell us explicitly what the result was, so we make that accompany the `AlreadyResult` tag. A second outcome is that the term is "stuck" and so for that reason also can't be reduced further. In this case, we want to supply the stuck subterm, and propagate that upward through the recursive calls to `reduce1`, so that the callers can see specifically what subterm it was that caused the trouble. Finally, there is also the possibility that we *were* able to reduce the term by one step, in which case we return `ReducedTo newly_reduced_term`.
233
234 The structure of our `reduce1` function, then, will look like this:
235
236     let rec reduce1 (term : term) (env : env) : reduceOutcome =
237       match term with
238       | _, AA -> TODO
239       | _, BB ->
240
241 We've supplied some of the guts of this function, especially the fiddly bits about how to deal with primitives and literals. But you need to fill in the gaps yourself to make it work. As mentioned before, don't worry about the environments. They're needed to see if variables are associated with any toplevel declarations, but we've filled in that part of the code ourselves. You don't need to worry about the primitives or literals, either.
242
243 Now, some function needs to call the `reduce1` function repeatedly and figure out when it's appropriate to stop. This is done by the `reduce` function, which looks like this:
244
245     let rec reduce (term : term) (env : env) : result =
246       match reduce1 term with
247       | AlreadyResult res -> res
248       | StuckAt subterm -> die_with_stuck_term subterm
249       | ReducedTo term' -> reduce term' env (* keep trying *)
250
251 This recursively calls `reduce1` until it gets a result or gets stuck. In the latter case, it calls a function that prints an error message and quits the program. If it did get a result, it returns that to the caller.
252
253
254 One of the helper functions used by `reduce1` is a `substitute` function, which begins:
255
256     let rec substitute (ident : identifier) (replacement : term) (original : term) =
257       match original with ...
258
259 This makes sure to substitute the replacement for any free occurrences of `Var ident` in the original, renaming bound variables in the original as needed so that no terms free in the replacement become captured by binding `Lambda`s or `Let`s in the original. This function is tricky to write correctly; so we're just supplying it for you.
260
261 However, one of the helper functions that *it* calls is `free_in (ident : identifier) (term : term) : bool`, and this was a function that you did write for an earlier homework. You should adapt your implementation of that to the datatype we're using here. Here is a skeleton:
262
263     let rec free_in (ident : identifier) (term : term) : bool =
264       match term with
265       | _,TermVar(var_ident) -> var_ident = ident
266       | _,TermApp(head, arg) ->
267           ...
268       | _,TermLambda(bound_ident, body) ->
269           ...
270       | _,TermLet(bound_ident, arg, body) ->
271           ...
272       | _,TermLetRec _ -> failwith "letrec not implemented"
273       | _,TermIf(test, yes, no) ->
274           ...
275       | _,TermPrimfun _ | _,TermConstructor _ | _,TermDestructor | _,TermLiteral _ -> false
276
277
278 That is, `Var ident` occurs free in `Var var_ident` iff the identifiers `ident` and `var_ident` are the same. The last four cases are easy: primitive functions, constructors, destructors, and literals contain no bindable variables so variables never occur free in them. These values may contain *results*, for instance if we partially apply the primitive function `+` to `3`, what we'll get back is another primitive function that remembers it has already been applied to `3`. But our interpreter is set up to make sure that this only happens when the argument (`3`) is already a result, and in our design that means it doesn't contain any bindable variables.
279
280 But now what about the cases for App, Lambda, Let, and If? You will need to supply the missing code for these. It's just an adaptation/extension of what you did in the previous week's homework.
281
282 For reference, OCaml's disjunction operator is written with an infix `||`; conjunction with `&&`; equality with `=`; and inequality with `<>`. TODO MORE TIPS
283
284 You should also fill in the gaps in the `reduce1` function, as described above. You can do this all with pencil and paper and your brain, and **that will constitute phase 1 of (this part of) the homework.** But you can also download the real source code, as we'll explain below, and try to build/compile your work, and see if OCaml accepts it. Then you can play around with the result.
285
286 If you're not going to do that, then skip down and read about Moving to the V2 interpreter. TODO link
287
288
289 Getting, reading, and compiling the source code
290 -----------------------------------------------
291
292 You can download the source code for the intepreter here: TODO link. That link will always give you the latest version. We will update it as we find any issues. Let us know about any difficulties you experience.
293
294 When you unpack the downloaded source code, you will get a folder with the following contents, sorted here by logical order rather than alphabetically.
295
296     interface.mli
297     types.ml
298     engine.ml
299     main.ml
300     primitives.ml
301     hilevel.ml
302     lolevel.ml
303     lexer.mll
304     parser.mly
305     types.mli
306     engine.mli
307     primitives.mli
308     hilevel.mli
309     lolevel.mli
310     Makefile
311     .depend
312
313 The first three files in this list are the only ones you need to worry about.
314
315 An `.mli` file like `interface.mli` specifies types for OCaml, in a way that gets published for other files in the same program to see. This `interface.mli` file contains the basic datatypes the program works with. And even this file (necessarily) has some complexity you can ignore. All you really need to pay attention to at first are the datatypes we described before. For phase 1 of the exercise TODO, you shouldn't need to change anything in this file anyway.
316
317 The second file, `types.ml`, contains different implementations for the environments. If you like, you can look at how these work, since they will play an important role in phase 2 of the exercise. The common interface these implementations have to supply is: TODO Each implementation is itself pretty simple, though this file also needs to have some trickery in it to work around constraints imposed by OCaml. (The trickery is marked as such.)
318
319 The third file, `engine.ml`, is where you should be focusing your attention. That contains the skeleton of the `reduce1` and `free_in` functions that you need to complete for phase 1 of the exercise, and also contains the skeleton of the `eval` function that you need to complete for phase 2 of the exercise. At the bottom of the file are also instructions on how to shift the interpreter between using the V1 or the V2 functions.
320
321 After you've edited the `engine.ml` file to complete the `reduce1` function, you can try building it and running the interpreter like this. First, make sure you're in a Terminal and that you're working directory is the folder that the source code unpacked to. Then just type `make`. That should take care of everything. If you see errors that you don't think are your fault, let us know about them.
322
323 Possibly some Windows computers that _do_ have OCaml on them might nonetheless fail to have the `make` program. (It isn't OCaml-specific, and will be found by default on Macs and many Linux systems.) In that case, you can try entering the following sequence of commands by hand:
324
325     ocamllex lexer.mll
326     ocamlyacc -v parser.mly
327     ocamlc -c lolevel.mli
328     ocamlc -c lolevel.ml
329     ocamlc -c interface.mli
330     ocamlc -c types.mli
331     ocamlc -c types.ml
332     ocamlc -c hilevel.mli
333     ocamlc -c hilevel.ml
334     ocamlc -c primitives.mli
335     ocamlc -w -8 -c primitives.ml
336     ocamlc -c engine.mli
337     ocamlc -c engine.ml
338     ocamlc -c parser.mli
339     ocamlc -c parser.ml
340     ocamlc -c lexer.ml
341     ocamlc -c main.ml
342     ocamlc -o interp.exe lolevel.cmo types.cmo hilevel.cmo primitives.cmo engine.cmo parser.cmo lexer.cmo main.cmo 
343
344 If your computer doesn't ... TODO
345
346
347 OK, I built the interpeter. How can I use it?
348 ---------------------------------------------
349
350 The interpreter you built is called `interp` (or on Windows, `interp.exe`). You can see its help message by running `./interp --help`.
351
352 The interpreter takes input that you feed it, by any of various methods, and passes it through a _parser_. The parser expects the input to contain a sequence of terms (plus possibly the other toplevel declarations we described before), separated by semicolons. It's optional whether to have a semicolon after the last term.
353
354 If the input doesn't parse correctly, you will have a Syntax error TODO. If it does parse, then the parser hands the result off to your interpretation functions (either `reduce`/`reduce1` in V1 of the interpreter, or `eval`/`evaluate`, in V2 described below). If they are able to reduce/evaluate each term to a result, they will print those results in a user-friendly format, and then move to the next result. If they ever encounter a stuck term or unbound variable, they will instead fail with an error.
355
356 So how do you supply the interpreter with input. Suppose the file `./input` contains:
357
358     let x = 3 in
359     (x, 0);
360     5*2 - 1;
361     \x. x
362
363 Then here is a demonstration of three methods for supplying input. These will all give equivalent results:
364
365  *  `./interp input`
366  *  `echo 'let x = 3 in (x, 0); 5*2 - 1; \x. x' | ./interp -`
367  *  `./interp -e 'let x = 3 in (x, 0)' -e '5*2 - 1' -e '\x. x'`
368
369 In the last method, the different `-e` elements are concatenated with `;`s; and then it works just like the preceding methods.
370
371 The format the parser accepts should look somewhat familiar to you. Lambda expressions work as normal, except that they must always be "dotted". You can also use some infix operators in the ways you can in Kapulet and Haskell:
372
373     2-1
374     (-) 2 1
375     (2-) 1
376     (-1) 2 /* this works as in Kapulet not Haskell; it means 2-1 */
377     flip (-) 1 2
378
379 All giving the same result.
380
381 As an experiment, the parser accepts two kinds of numeric input. Numbers like `0`, `1`, and so on are handled as native OCaml numbers; whereas numbers like `0.`, `1.` and so on are handled as abbreviations for `Zero`, `Succ Zero` and so on, with the implied OCaml datatype:
382
383     type dotted_number = Zero | Succ of dotted_number
384
385 The supplied primitives `pred`, `succ`, and `zero?` work only on the dotted numbers; whereas the supplied infix primitives `+`, `-`, and `*` work only on the undotted numbers. There are also `<` and `<=` and `==` for the undotted numbers. (The parser will also accept `>` and `>=`, but will translate them into the corresponding uses of `<` and `<=`.)
386
387 Here is some more sample inputs, each of which the parser is happy with:
388
389     /* these are comments */
390     if zero? x then 1 else pred x
391     zero? 0. /* zero? and pred and succ work with dotted numbers */
392     x == 0 /* the infix comparison operators and + - * work with undotted numbers */
393     /* both of the following get translated into if-terms */
394     x and y
395     x or y
396     lambda x. x
397     \x. x
398     \x y. y (x y)
399     let x = 1 + 2 in 2 * x
400     let x = 1 + 2; y = x+1 in y
401     let f = \x.x+1 in f 0
402     let f x = x + 1 in f 0
403     true
404     (false,1)
405     (,1) true
406     (,) true 1
407     (,,) x y z /* but only up to triples, there are no bigger tuples */
408     box 1 /* this is a 1-tuple */
409     /* it won't be clear yet why it's useful, but wait for later weeks */
410     fst (1,2) /* evaluates to 1 */
411     /* you can use fst on boxes, pairs, and triples */
412     /*   snd also on pairs and triples */
413     /*   and trd on triples */
414     id x
415     const x y /* our friend the K combinator */
416     flip f x y /* gives f y x */
417     g comp f /* comp is an infix composition operator */
418     f pmoc g /* this is flip comp, that is \x.g(f x) */
419     f x $ g y $ h z /* as in Haskell, this is f x (g y (h z)) */
420     /* note that it's not f x (g y) (h z) */
421     "strings" /* you can input these and pass them around, but can't perform any operations on them */
422
423 The parser also accepts `letrec ... in ...` terms, but currently there is no implementation for how to reduce/interpret these (that's for a later assignment), so you'll just get an error.
424
425 As explained before, you can also include toplevel declarations like:
426
427     let y = ... end;
428
429 Calling them "toplevel" means they can't be embedded inside terms. The above declaration interprets the rhs as a term, and then binds the variable `y` to the result, making it available in later terms where `y` hasn't been locally rebound. Thus:
430
431     let y = 1 + 2 end;
432     let x = 0 in (x,y)
433
434 gets interpreted as `(0,3)`.
435
436 Another toplevel declaration `symbol w` tells the interpreter that you want to specially designate `w` as okay to appear uninterpreted in terms you use.
437
438 If the interpreter encounters other locally-unbound variables, where no toplevel declaration has already been given, it will fail with an error.
439
440
441
442 Moving to the V2/environment-based interpreter
443 ----------------------------------------------
444
445 ...
446