HTDP Stepper does not generate fresh names for local defs

[klauso]

Consider this program in ISL+

(define y_0 77)
(define f (lambda (x)
            (+ 2
               (local
                 [(define y 88)]
                 (* y_0 2)))))
(f 2)

When reducing this program in the stepper there is a confusing name clash with two definitions of y_0 in the program, and the y_0 in the expression (* y_0 2) is substituted by 77 and not 88 (which is correct but contradicts the program that gets generated during reduction).

Here is an image of the decisive reduction step.
https://cdn.pbrd.co/images/H4zbeg2.png

[jbclements]

Yep, sigh... my bug. Known.

[klauso]

Maybe this is not the right place for discussing this, but wouldn't it be possible to define the meaning of local expressions in a different way - one that does not involve the synthesis of new top-level definitions?

I've taught several big courses using HTDP, and I like the stepper a lot in general, but I really hate the treatment of local expressions. It is just too complicated for most students, and it gives wrong intuitions about what actually happens (for instance, students are worried about performance problems due to synthesizing new top-level expressions all the time).

I'd much prefer if ISL would either feature only non-recursive let (which could be dealt with by ordinary substitution) instead of local, or a less syntactic presentation of the reduction rules using environments and closures.

[jbclements]

Are you thinking here about a change to the stepper, or to the ISL language? I see a bit of both.

[mfelleisen]

On Jan 25, 2018, at 4:02 PM, Klaus Ostermann ***@***.***> wrote: Maybe this is not the right place for discussing this, but wouldn't it be possible to define the meaning of local expressions in a different way - one that does not involve the synthesis of new top-level definitions? I've taught several big courses using HTDP, and I like the stepper a lot in general, but I really hate the treatment of local expressions. It is just too complicated for most students, and it gives wrong intuitions about what actually happens (for instance, students are worried about performance problems due to synthesizing new top-level expressions all the time). I'd much prefer if ISL would either feature only non-recursive let (which could be dealt with by ordinary substitution) instead of local, or a less syntactic presentation of the reduction rules using environments and closures.

1. The stepper illustrates cleanly the difference between ‘what a function computes’ (the implementation of ISL) and ‘how a function computes its result’ (compile, then the x86 interprets but it could be something completely different). I emphasize this in my courses and I constantly tell them that they can understand computation with everything they learned in school (“gymnasium” if that still teaches anything). Of course it is a stretch for many freshman kids to remember what they learned in high school, because that’s so long ago :-) [[ I also poke fun at my “know it all” students who think “stacks are important". Why stop at stack models when there’s quantum physics? It really is an amazing teachable moment about models and the right amount of hiding. ]] 2. The syntactic representation is critical because it is exactly how K-12 explains calculation. You don’t want to require more. Mixing in environments would cause a complete break down of understanding because all previous rules would have to go away. I consider this a pedagogic disaster propagated by old texts. 3a. LOCAL exists for two distinct reasons: — it assigns the exact same meaning to define as the module tip level — it has the exact same syntax as a sequence of defines so you can easily switch back and forth 3b. The semantics of LOCAL as presented is totally correct. What one could do is run an analysis of LOCAL’s body and if definitions are provably 1st order non-recursive we could substitute them away and 1st order recursive definitions could be left in place until the body is reduced to a value. BUT looking up a variable would have to change. I suspect that integrating this idea with the current stepper execution model is research and may even yield a paper.

[klauso]

Matthias, thanks for the explanation. I fully understand your points, and I agree with everything (except 3b - you think the situation I described above is correct?). I'm merely reporting my experience in teaching a sizeable number of courses using HTDP - right now a course with over 600 students. You can of course argue that maybe I'm teaching it the wrong way, but my experience is that 90% of my students don't understand what the stepper does with local expressions.

I do appreciate that local definitions are so similar to top-level definitions, as you point out, but I'm asking you to also consider the downsides. In addition to the issues I describe above, there's also the issue of local define-struct, which further complicates the semantics (different invocations yield distinct struct instances) without a particularly convincing case why they are needed (apart from uniformity with top-level definitions).

(By the way, the stepper also does not seem to support local structs. For instance, this example crashes the stepper:

(define (f x)
  (local [(define-struct a (b c))]
    (list make-a a?)))

Another small gripe I have with local:
(local [(define (f x) ...)] f) (with f non-recursive) behaves very different from (lambda (x) ...) in the stepper and it is not at all obvious to students that the semantics is the same.

Having let instead of local would be bad from the perspective of uniformity with top-level and slightly decrease expressiveness (because recursive functions would need to be top-level), but it would make it significantly simpler for students to understand what is going on. Knowing Matthias, I guess my chances of convincing him to consider a change to the language and/or stepper are slim, but it's worth a try ;)

[jbclements]

Just to pick up on one point: local define-structs are a known bug. Mea culpa, and on the list.

[mfelleisen]

On Jan 25, 2018, at 4:44 PM, Klaus Ostermann ***@***.***> wrote: In addition to the issues I describe above, there's also the issue of local define-struct, which further complicates the semantics (different invocations yield distinct struct instances) without a particularly convincing case why they are needed (apart from uniformity with top-level definitions).

We made the decision to include the generative version of define-struct in the teaching languages, and this decision might have been a mistake. It is the form of structs that provide the same conceptual power (at run time) as datatype in ML. The decision had nothing to do with wishing to make the "syntactic semantics” work well; we could have gone either way here. ;; - - - You might misunderstand the first sentence in 3b. What I am saying is (1) the semantic treatment of local covers all possible cases (including the not uncommon one that the body of local returns a function) and (2) that we should check whether local is just a let and then provide a simpler, substitution-based stepping semantics. ** ;; - - - I assume you know that let and let* exist in ISL. You can teach with them instead of local. But, sadly the stepper deals with let as if it were a local. So sadly, right now we get this wrong. ;; - - - ** [[ But you may also be saying that your students no longer understand how to evaluate f(5) when f is defined via f(x) = x + 42 that is via substitution. In that case, I am not sure how to deal with your problem. FWIW, Northeastern’s first course enrolled 800 students last semester but admittedly we run around 8 sections to keep things manageable for instructors.]]

[samth]

I will agree with @klauso that I also find the stepper less useful in ISL (especially ISL+lambda) than in BSL. One aspect of this is the additional reduction to add a lambda expression in every application, which is basically never what I want. A second aspect is that the combination of existing definitions plus new definitions created by the stepper is confusing. Since I regularly use the recursive aspect of local, I wouldn't want that to go away. But instead, here's a few suggestions for how it could be presented differently.

1. Bindings that are no longer needed could be removed.
2. Lifted bindings could be colored differently, or otherwise indicated.
3. local expressions could be kept during reduction of their bodies, just like the entire definitions window contents is kept around during reduction.

[klauso]

Wouldn't there also be a syntactic way of explaining local in the stepper without the synthesis of new top-level definitions, namely by treating expressions like (local [(define x v1)..] v) as values and then having a hierarchical lookup instead of the current top-level lookup of names? I'm sure Matthias wrote some paper explaining letrec in a purely syntactic way using evaluation contexts in a clever way ;)

edit: I think I'm merely proposing the same thing as item 3. in @samth 's list.

[mfelleisen]

On Jan 25, 2018, at 5:06 PM, Klaus Ostermann ***@***.***> wrote: Wouldn't there also be a syntactic way of explaining local in the stepper without the synthesis of new top-level definitions, namely by treating expressions like (local [(define x v1)..] v) as values and then having a hierarchical lookup instead of the current top-level lookup of names? I'm sure Matthias wrote some paper explaining letrec in a purely syntactic way using evaluation contexts in a clever way ;)

Precisely! That paper explains LOCAL exactly in the way John implemented it and proved correct in his dissertation (much underappreciated). It merely summarizes several steps (from my original paper) into one and does not spell out the module-level sequences as (local ((define f-globak …) (define g-global ..)) .. module expression ..). I did not prove this but I am convinced there is no other uniform way to explain local in general, which is why I am proposing 3b.

[mfelleisen]

On Jan 25, 2018, at 5:04 PM, Sam Tobin-Hochstadt ***@***.***> wrote: One aspect of this is the additional reduction to add a lambda expression in every application, which is basically never what I want.

Agreed.

A second aspect is that the combination of existing definitions plus new definitions created by the stepper is confusing. Since I regularly use the recursive aspect of local, I wouldn't want that to go away. But instead, here's a few suggestions for how it could be presented differently. • Bindings that are no longer needed could be removed. • Lifted bindings could be colored differently, or otherwise indicated. • local expressions could be kept during reduction of their bodies, just like the entire definitions window contents is kept around during reduction.

I understand the first two proposals (but John would know whether they can be implemented with the existing stepper strategy. I think yes for bullet 2, no for bullet 1). I do not understand the third bullet. Are you repeating my proposal 3b?

[klauso]

I'm not sure whether my proposal is the same as @samth 's, but I was considering a semantics that would reduce

(local [(define (f x) (+ 1 (f x)))]
  (f 7))

to

(local [(define (f x) (+ 1 (f (sub1 x))))]
  (+ 1 (f (sub1 7))))

[mfelleisen]

On Jan 25, 2018, at 5:23 PM, Klaus Ostermann ***@***.***> wrote: I'm not sure whether my proposal is the same as @samth 's, but I was considering a semantics that would reduce (local [(define (f x) (+ 1 (f x)))] (f 7)) to (local [(define (f x) (+ 1 (f (sub1 x))))] (+ 1 (f (sub1 7))))

This is 3b (which is not AT ALL whatI think you proposed initially with ‘environment’ based semantics.) That’s what 3b says. You can’t do this in general, only with a static analysis. None of this fits easily with the stepper implementation framework.

[mfelleisen]

Let me illustrate my responses re 3b with an example:

(define (d/dx f)
   (local ((define (f-prime x) 42)) ;; this is not the numerical differentiation of f! 
       f-prime))

(define (g x) (+ x 5))

(define g-prime (d/dx g))

(map g-prime '(1 2 3 4 5))

Without the general local rule, this program cannot be explained.

Once the last expression is completed, bindings for f-prime and g-prime could be eliminated assuming no other references exist, which is the local-gc rule from our original paper and one of Sam's bullets. And yes, they f-prime could be colored differently (cool idea).

[samth]

My suggestion 3 is more like the \lambda_vCS calculus. ;)

I would add another value production:

v ::= ... | (local [(define x v_rhs) ....]  v)

and reduction rules that reduce in the body of (and on the RHS of) local. As @mfelleisen says, this requires a small change to the semantics of variable reference, but this change is already in the reduction rules for local (they aren't substituted until needed because they're top-level bindings).

Another way of thinking of this is as taking the metaphor in HtDP, that a local expression is like having a mini definitions window, and continuing it in the stepper. Preserve the definitions window, and keep it around in the reductions.

Note that you could of course reduce (local [(define x 1)] 2) to 2, which is like a GC rule, but that doesn't affect the semantics.

[mfelleisen]

From an implementation perspective, I have the distinct sense that none of this will work with the current framework. I will have to defer to John for details. From a semantics pov, you are asking for 3b. [I do know my semantics.] In detail, you don’t need the new grammatical production rule in the grammar, you need instead 1. a different lookup rule: E_1[(local ( .. defines ..) E_2 [x])] —> E_1[(local ( .. defines ..) E_2 [v])] if defines includes (x v) and E_2 does not contain a local that shadows x 2. a return rule E[(local ( .. defines ..) v)] —> .. lifted defines .. E[v] IF v makes reference to the defines (which is the static analysis I spoke of, basically an escape analysis) 3. a separate return rule for ‘plain v’: E[(local ( .. defines ..) v)] —> E[v] IF v makes no reference to defines. The way John instruments things, this can’t work.

[klauso]

But couldn't you achieve the same without any top-level lifting by a rule like this:

E[(local (... defines ..) v)] -> E[v']
whereby v' is like v except that for every (define x ...) in defines every x in v is replaced by (local (... defines ...) x)

That rule would subsume both rule 2 and rule 3.

[mfelleisen]

The introduction of set! would invalidate the rule.

[jbclements]

What about mutation?

The existing model works great for mutation, and it looks to me like this one would not.

(Feel free to make snarky comments about whether I'll get to mutation before I die.)

[jbclements]

Ah! I took a bathroom break to compose my message, and Matthias beat me.

[klauso]

True, but I for one would be happy to have a simpler semantics for ISL. I don't use ASL and set! in my courses, and I assume many others who teach with the *SL languages don't use it either. Why not just have a semantics for ASL that is not a direct extension of the ISL semantics?

[mfelleisen]

Because you’re not the only who uses the teaching languages. Part of the idea of hierarchies of languages is that we never need to say “oh this one rule there was plain wrong. Forget it now.”

[klauso]

Fair enough, my opinion is just one data point. However, unless I'm mistaken even your own book doesn't use mutation anymore. Also, I think it would be illuminating for students to illustrate that some rules ("equational reasoning") are destroyed by the introduction of mutation, i.e., there is a price to be paid for adding mutation. Finally, it is a little sad if the reduction rules, if read as equations, do not validate program refactorings that are in fact valid in ISL, just for compatibility with ASL.

[mfelleisen]

The reduction rules, read as equations, are valid refactoring rules in ISL/+.

[klauso]

I meant that the reduction rule I proposed above, read as equation, is a valid refactoring in ISL/+, but it's not easily derivable from your reduction rules 1-3.

[mfelleisen]

Well yeah, the ‘truth’ (meaning the full set of valid equations) on ISL/+ is Pi^1_1, way beyond a computable set. There is no finite axiomatization.

[jbclements]

Closed by racket/htdp@d7620a37ed7864fa8c18fb151.