[plt-scheme] PLAI question (closures)

> Now, quoting the text:
>
> "The moral is, to properly defer substitution, the value of the function
> should be not only its text, but also the substitutions that were due to
> be performed on it."
>
> The phrase "the substitutions that were due to be performed on it" seems
> rather mysterious to me. But I take it to mean substitutions of already
> bound variables (beta reductions?) that could occur given the bindings
> in effect at that time, and not (say) a substitution that might occur
> for a variable free in the expression being considered, but possibly
> bound in a larger expression containing it? Is that right?


Hi Greg,

The key example at the top, where it says:

    {with {x 3}
      {with {f {fun {y} {+ x y}}}
        {with {x 5}
          {f 4}}}}

is the one I think we need to keep in mind.  We don't want "f"  to get its
"x"  value from the innermost "with" binding, but from the outermost one.

Under a pure substitution model, when we see something like:

    {with {x 3}
      {with {f {fun {y} {+ x y}}}
        {with {x 5}
          {f 4}}}}

then we'd resolve things by reducing as:

==> {with {f {fun {y} {+ 3 y}}}       ;; substituting x throughout
      {with {x 5}
        {f 4}}}}

==> {with {x 5}                       ;; substituting f throughout
      {{fun {y} {+ 3 y}} 4}}

==> {{fun {y} {+ 3 y}} 4}

==> {+ 3 4}

==> 7


And the first reduction above shows that the 'x' in "f" needs to be bound
to 3.  In lieu of actual substitution, if we use our substitution cache to
simulate substitution, then we have to make sure that it maintains the
same effect as if we had actually done the substitution in the first
place.  That's why closures need to hold onto their environment when
they're constructed.  If they don't, then as the book shows, we suddenly
get dynamic scope instead of lexical scope.


> I find the type definition in the text
>
> (define-type FAE-Value
> [numV (number?)]
> [closureV (param symbol?)
>    (body FAE?)
>    (ds DefnSub?)]
>
> hard to follow (because I haven't seen this language spelled out, I
> suppose). But in the context of the above example (in my own ad hoc
> notation), I take \x . x + y to be body and the "table" [x <- 3] to be
> ds. I'm also guessing that FAE? and DefnSub? are type predicates, and
> closureV is being defined as the product of the types defined by the
> predicates, and that "body" and "ds" are essentially field names.

Yes, it's doing what in Ocaml might look like:

    type fae_value = Num of number
                   | Closure of symbol * fae * defn_sub

in building a discriminated record type, where the Closure is made up of
three components: a parameter, a body, and a substitution cache.