From: jim Date: Mon, 23 Mar 2015 23:06:40 +0000 (-0400) Subject: edits X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=d21da604a8eb2fef87dce34085814784a1021d48 edits --- diff --git a/topics/closures.mdwn b/topics/closures.mdwn index 8e36db69..9cbded23 100644 --- a/topics/closures.mdwn +++ b/topics/closures.mdwn @@ -1,28 +1,13 @@ -## Evaluation in the untyped lambda calculus: environments +One strategy for evaluating or interpreting terms avoids the tedious and inefficient _substituting_ +we've become familiar with. Instead, when a variable becomes bound to a result value, we'll +keep track of that binding in a separate scorecard, that we'll call an "environment." -The previous interpreter strategy is nice because it corresponds so closely to the -reduction rules we give when specifying our lambda calculus. (Including -specifying evaluation order, which redexes it's allowed to reduce, and -so on.) But keeping track of free and bound variables, computing fresh -variables when needed, that's all a pain. - -Here's a better strategy. Instead of keeping all of the information -about which variables have been bound or are still free implicitly -inside of the terms, we'll keep a separate scorecard, which we will call an "environment". This is a -familiar strategy for philosophers of language and for linguists, -since it amounts to evaluating terms relative to an assignment -function. The difference between the substitute-and-repeat approach -above, and this approach, is one huge step towards monads. - -The skeleton code for this is at the [[same link as before|/code/untyped_evaluator.ml]]. -This part of the exercise is the "VB" part of that code. - -You'll see that in the `eval` function, a new kind of value `Closure (ident) (term) (env)` -is used. What's that about? - -The `Closure`s are for handling the binding of terms that have locally free variables in them. Let's +This strategy has to introduce a new kind of structure, called a `Closure`, to handle +binding to terms that have locally free variables in them. Let's see how this works. For exposition, I'll pretend that the code you're working with has -primitive numbers in it, though it doesn't. (But the fuller code it's simplified from does; see below.) +primitive numbers in it, though [[the homework assignment|/exercises/assignment7]] doesn't. +(But [[the fuller code|/topics/week7_untyped_evaluator]] it's simplified from does.) + Now consider: term environment @@ -140,9 +125,3 @@ but instead with the `Closure` structure: Closure("y", BODY, SAVED_ENV) where `BODY` is the term that constituted the body of the corresponding `Lambda`, and `SAVED_ENV` is the environment in place when `f` is being bound. (In this simple implementation, we will just save the _whole environment_ then in place. But in a more efficient implementation, we'd sift through it and only keep those bindings for variables that are free in `BODY`. That would take up less space.) - -So that's what's going on with those `Closure`s. In the simple code we gave you to work with, we just made these another clause in the `term` datatype. That's really not correct. `Closure`s aren't terms. The syntax for our language doesn't have any constituents that get parsed into `Closure`s. `Closure`s are only created *during the course of evaluating terms*: specifically, when a variable gets bound to an abstract, which may itself contain variables that are locally free (not bound by the abstract itself). So really we should have two datatypes, one for terms, and another for the *results* (sometimes called "values") that terms can evaluate to. `Closure`s are results, but they aren't terms. `App`s are terms, but not results. If we had primitive numbers or other constants in our language, they might be both terms and results. In the fuller code from which your homework is simplified, this is how the types are in fact defined. But it makes things more complicated. So to keep things simple for the homework, we just pretended like `Closure`s were a new, exotic kind of `term`. - -In any case, now you know what's going on with the `Closure`s, and you should be able to complete the missing pieces of the `eval` function in the code skeleton linked above. - -If you've completed all the missing parts correctly (there are six gaps for the previous stage of the homework, and two gaps for this stage), then you should be able to compile the code skeleton, and use it as described in the comments at the start of the code.