"Pushing down" let bindings

[dhess]

Discussed in https://github.com/hackworthltd/vonnegut/discussions/638

^{Originally posted by dhess June 30, 2021}
Generally speaking, I really like the reduction rule in our evaluation semantics that converts applications to let bindings, as this rule obviates the need for environments (which are not first class in any programming language I'm aware of). However, in Keybase chat today, I pointed out the following limitation of this rule. Consider the following evaluation step in the application of map to a list:

Now let's evaluate the APP redex such that we get a lettype β = Nat in ... in its place:

The problem here is that I have to reduce the lettype β = Nat in ... for all occurrences of β in the subtree under the lettype before I can perform the function application (λf. ...) (λy.Zero). So if I want to mimic the call-by-name evaluation strategy, I can't. I can effectively only do call-by-value.

(Here I use our slightly odd lettype form, but the same goes for lets for term bindings.)

I proposed that, instead of the current rule which replaces the application with a single lettype at the application location in the tree, we push the lettype β down to each occurrence of β in the subtree, which would allow the student to explore different evaluation strategies.

@georgefst pointed out that in Harry's original "Evaluation steps in Vonnegut" document in Craft (the Apple URI scheme link to the relevant section of that document is craftdocs://open?blockId=CECD7E89-232B-4F44-9A6F-53DF188B9212&spaceId=8b43f204-aeeb-b8ce-45cc-73a653745299), under the "Making substitution incremental" heading, the major rationale for this reduction rule was to not change too much in the tree at once, making application easier to follow; or, as @georgefst put it, "it keeps the evaluation step small and local." By pushing the let or lettype down to each occurrence of the bound variable, we would be harming this nice pedagogical affordance.

@brprice then had the really interesting thought that by providing another reduction rule that "floats lets downwards" towards their occurrences, and changing the rule that allows lets to be eliminated once there are no more uses in their subtree to something more like, "a let can be eliminated once it's adjacent to its bound variable's use" (or similar), the student could explore these ideas themselves, all while following our small-step principles of evaluation.

Obviously after some deliberate practice and eventual understanding of this small-step let elimination, we'd probably want to change the rules to something more like what we have now, to keep this from being too tedious. (@georgefst raised the possibility of allowing the student to drag the let down the tree to its occurrence, to match it up and eliminate it in one gesture.) We could even eventually remove the "function-application-as-let-binding" rule and simply do substitution in one go.

[dhess]

As I mentioned in https://github.com/hackworthltd/vonnegut/discussions/638, I might be using call-by-value/call-by-name incorrectly, but perhaps only because our reduction step here is unusual. As I understand it, the consequences of not being able to push down the let bindings are similar to the limitations of call-by-value. Anyway, let's discuss this soon in person so we can hash this out.

[dhess]

I'm going to close this issue, as it simply motivates why we want to do this, and I think we've unanimously decided that it's a good idea and therefore requires no more discussion. The work will be tracked in #44.