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.
-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.
+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 then keep repeating single-step reductions until you can't find any more eligible redexes. This involves substituting the argument of a redex into any free occurrences of the variable bound in the head. 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 substitute-and-repeat interpreter; and second, an environment-based one.
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.
But these benefits come at a price. The actual code you're going to look at has some complexity to it.
-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.
+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 substitute-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.
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.
As a result of never applying functions to non-results, non-results will never get bound to any variables, either.
-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.)
+Now in the V1/substitute-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.)
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:
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.
-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.
+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 substitute-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.
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:
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.)
-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:
+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/substitute-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:
let y = 1 + 2 in
let x = y + 10 in
The V1/reducuction-based interpreter
------------------------------------
-For phase 1 of this exercise, you're going to write a `reduce1` function that converts OCaml values like:
+For phase 1 of this exercise, you're going to write a `reduce_head_once` function that converts OCaml values like:
TermApp(TermApp(TermLambda("x", TermApp(Var "x", Var "y")), TermLambda("w", Var "w")), ...)
has to come from a subsequent re-invocation of the function.
-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 `ω ω`); 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).
+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 `reduce_head_once` 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 `ω ω`); 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).
-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.
+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 `reduce_head_once` 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.
-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:
+What we're going to do instead is to have our `reduce_head_once` function wrap up its output in a special datatype, that describes how that output was reached. That type looks like this:
type reduceOutcome = AlreadyResult of result | StuckAt of term | ReducedTo of term
-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`.
+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 `reduce_head_once` already knows what term it was trying to reduce; but in some cases it's a bit more convenient to have `reduce_head_once` 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 `reduce_head_once`, 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`.
-The structure of our `reduce1` function, then, will look like this:
+The structure of our `reduce_head_once` function, then, will look like this:
- let rec reduce1 (term : term) (env : env) : reduceOutcome =
+ let rec reduce_head_once (term : term) (env : env) : reduceOutcome =
match term with
| _, AA -> TODO
| _, BB ->
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.
-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:
+Now, some function needs to call the `reduce_head_once` function repeatedly and figure out when it's appropriate to stop. This is done by the `reduce` function, which looks like this:
let rec reduce (term : term) (env : env) : result =
- match reduce1 term with
+ match reduce_head_once term with
| AlreadyResult res -> res
| StuckAt subterm -> die_with_stuck_term subterm
| ReducedTo term' -> reduce term' env (* keep trying *)
-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.
+This recursively calls `reduce_head_once` 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.
-One of the helper functions used by `reduce1` is a `substitute` function, which begins:
+One of the helper functions used by `reduce_head_once` is a `substitute` function, which begins:
let rec substitute (ident : identifier) (replacement : term) (original : term) =
match original with ...
For reference, OCaml's disjunction operator is written with an infix `||`; conjunction with `&&`; equality with `=`; and inequality with `<>`. TODO MORE TIPS
-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.
+You should also fill in the gaps in the `reduce_head_once` 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.
If you're not going to do that, then skip down and read about Moving to the V2 interpreter. TODO link
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.)
-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.
+The third file, `engine.ml`, is where you should be focusing your attention. That contains the skeleton of the `reduce_head_once` 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.
-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.
+After you've edited the `engine.ml` file to complete the `reduce_head_once` 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.
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:
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.
-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.
+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`/`reduce_head_once` 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.
So how do you supply the interpreter with input. Suppose the file `./input` contains: