Level tracking & bindings in escapes

[yallop]

(Thanks for this very exciting ppx-extension!)

Binding analysis doesn't keep track of levels or track bindings in escapes, which leads to some surprising behaviour. Here are some examples:

1. Shadowing a quoted binding in an escaped expression:

   The following code is rejected

   [%code fun x -> [%e let y = [%code 3] in [%code y]]]

   with the following error:

   Error: Unbound value y
   

   I can imagine a design where this is acceptable, in which only bindings from quotations are in scope within quotations. It's different from MetaOCaml, where both x and y are in scope in the body of the let, and where the equivalent expression would build code for a function that returns a future-stage e via cross-stage persistence.

   However, that design not quite what's going on here, as the following example shows. The following code is accepted

   [%code fun x -> [%e let x = [%code 3] in [%code x]]]

   and produces the code value

   fun x -> 3

   The fact that second example is accepted while the first is rejected illustrates that only the environment of quotation-bound variables is considered when checking free variables in the subexpression [%code x]. However, the generated code illustrates that the escape-bound variable actually shadows the quotation-bound variable during execution. The treatment of binding in the two situations is not consistent.

2. Using a quoted binding in an escaped expression:

   All of the following expressions produce code for the identity function, which is rather surprising:

   [%code fun x -> x]
   [%code fun x -> [%e x]]
   [%code fun x -> [%e [%code x]]]

   In MetaOCaml x is a future-stage binding, so it can't be used in the present; only the first and third examples are allowed. (Perhaps the design in which x can appear either escaped or quoted works out, but it seems a bit less uniform and extensible.)

Possible solution

Here's one way to fix the problems above:

1. Keep track of the level of each expression (i.e. whether it appears inside or outside a quotation), and the level of each bound variable.

2. Analyse both quoted and escaped expressions, keeping track of variables bound at both stages, and their levels.

3. Enforce the following rules:

   1. Quotation-bound variables are at level 1. Escape bound variables are at level 0.
   2. Only level-1 variables can be used at level 1 (i.e. no cross-stage persistence).
   3. Only level-0 bound variables can be used at level 0 (i.e. no accessing the future from the present)
   4. Scope is normal OCaml scope -- i.e. variable shadowing does not consider levels.

Let me know if a pull request would be of interest!

[stedolan]

Number #1 is a bug, specifically this bug. ppx_stage does not use fresh variable names for plumbing values in the staged environment through escapes, and it should. I don't think it's hard to fix. ppx_stage does not support transparent CSP (at the moment, anyway), so I think it is correct for it to reject your first example. It's inconsistent and wrong to accept the second, though.

Number #2 is a feature, although a debatably useful one. It's not documented and I'm not set on keeping it forever, but I'm curious to play with it a bit. The idea is that future-stage bound variables are in scope in the present, but a future variable of type 'a has a present type of 'a code. It certainly cuts down on some of the annotation noise (no more .~x), but I haven't used it enough to know whether it makes things simpler or more complicated in practice.

[yallop]

Let me check whether I understand the design. Is the idea that the scope should be normal OCaml scope (so that every variable refers to the closest enclosing binding, ignoring quotations/escapes for scoping purposes)?

The undocumented feature you describe sounds like it can be emulated by inserting a let binding into every splice that occurs within a binding quotation in MetaOCaml -- for example, this ppx_stage code

[%code fun x -> [%e exp]]

behaves like this MetaOCaml code:

.< fun x -> .~(let x = .<x>. in exp) >.

[Edit: the translation into MetaOCaml should be a little more elaborate to ensure that x is in scope both in the escape and in nested quotations at the appropriate levels.]

[stedolan]

Yes to both: the scope should be the normal OCaml scope, and inserting lets in MetaOCaml has the same effects as this feature in ppx_stage.