Re: [Caml-list] ANN: BER MetaOCaml N104, for OCaml 4.04.0

[Oleg <oleg@okmij.org>]

Thank you, Gabriel. Sorry for a late reply.

> I wondered why attributes were used instead of
> extensions. 
I have thought about this issue and have documented the reasoning
behind settling on attributes in the NOTES.txt file of the metalib
directory. That file describes many other design decisions, possible
alternatives, and future work.

> In my book, (e [@attr]) is supposed to be an OCaml term
> that behaves as the expression (e), with some extra (tooling- or
> optimization- related) expression of intent. On the contrary, [%ext e]
> is allowed to have any semantics at all. 

That is precisely the reason. The type-checker traverses an expression
several times (e.g., to collect variables, to check expansiveness,
etc.) It totally ignores the extension nodes. But it traverses inside
the nodes with attached attributes. This is the behavior I want. The
expression inside the brackets is meant to be a regular OCaml
expression (only evaluated with a `delay', so to speak), so the
typechecker should go inside and check it, etc. If I used extensions,
I would need to emulate these extra typechecking traversals somehow.
Incidentally, staging literature very often calls brackets and escapes
``staging _annotations_''. There is a reason for that.

> One interesting thing with the addition of the two new syntactic
> classes "pattern" and "value" is that, from a syntactic point of view,
> the idea of using extensions directly instead of home-grown syntax
> starts looking more reasonable: [%quote e], [%quote.pat e],
> [%quote.val e] (plus long forms metaocaml.quote*). Moving from .< e >.
> to [%quote e] is still arguably a bad deal for readability, but for
> the other two forms it would actually be an improvement over the
> current syntax. So I guess the benefit would depend a lot on how often
> these two new forms end up being used by MetaOCaml programmers. Using
> the extension syntax directly would certainly simplify a few things
> around MetaOCaml -- zero need for non-standard parsing, for example.

I fully agree with that. [%quote.pat e] is certainly very
appealing. Perhaps we can check carefully how OCaml traverses
expressions (besides the normal typechecking pass) and if using
extension will be sufficient in the end. If so, one can easily switch
to it.

> It is interesting that you mention that "function" allows to
> easily represent sets of clauses as expressions, as I was recently
> thinking about which kind of constructions would be made possible by
> taking "sets of clauses" as a first-class syntactic category.
We can discuss this further in a couple of days. Some unification will
be nice.

> I was professionally obligated to remark your formulation on
> where (genlet exp) actually places its definition: "The `let` is
> inserted right under the binder for the "latest" free variable
> contained in `exp`". This is exactly the style of placement used in
> sum-equivalence algorithms (and, I suppose, work on partial
> evaluation), typically the delimited-control-using presentation of
> "Extensional normalisation and type-directed partial evaluation for
> typed lambda calculus with sums" by Vincent Balat, Roberto Di Cosmo
> and Marcelo Fiore, 2004. Interestingly, these algorithms do not (only)
> place let-bindings in this way, but also case statements -- they want
> the case-distinction on the bound value to have as large a scope as
> possible. This suggests that maybe the "finding the earliest place to
> introduce an expression" is a really useful primitive to have for
> metaprogramming, and that your "genlet" could be reconstructed from
> it, but right now I don't see how to expose it without letting the
> user do delimited control -- which is what you started from.
As you probably expect, I am well familiar with Balat works and NBE
and the problem of placing let and case statements. Before I used
delimited control. But the current implementation of MetaOCaml does
something different. Internally, a code value is represented as
AST along with a set of `virtual' let-bindings. That is, essentially
in the form
        let x1 = e1 and x2 = e2 ... in e
That should remind you of `answers' used in call-by-need calculi.
The virtual bindings are converted to real let-bindings when the
binder is applied to the expression. If the bound variable occurs
within ei, the corresponding virtual let-binding must be made real.
Others remain virtual and float out. Of course there are
complications: an expression may be spliced in
several times. So, one has to deal with duplicates. Further, genlet
may nest (that is, each ei itself contains virtual let-bindings. When
actualizing let-bindings, we have to `straighten them up'). The
comments in the main code file trx.ml describe the algorithm in some
detail. It should be written up of course. Again, this is something we
can talk about in a day.