[wg-camlp4] Against the use of syntactically-valid OCaml code for syntax extension purposes

[Gabriel Scherer]

> What's missing is maybe the ability to annotate either the binding itself as
> opposed to the whole expression (more interesting when the whole expression
> has multiple bindings: let p1 = e1 and p2 = e2 and ...).  But is that really
> necessary?  One can always use the convention that an annotation on the
> binding would actually need to be put at the toplevel of the pattern itself.

My understanding is that this is precisely what type-conv does:
annotate the type declaration itself, rather than the type expression
or the whole phrase. I'm not sure what kind of annotations are being
considered here, but a pragma-style @ignore_unused_variable for
example should be bound to the declaration itself. Finally, using a
convention to annotate the pattern may give rise to critical pairs /
ambiguities where the semantics of the program depends of whether we
consider the annotation to cover the pattern or the declaration (for
annotations that make sense in both, eg. @profile).

On Wed, Jan 30, 2013 at 7:17 AM, Alain Frisch <alain at frisch.fr> wrote:
> On 1/29/2013 7:53 PM, Gabriel Scherer wrote:
>>
>> I'm not sure the idea of having "postfix" and "prefix" annotations
>> makes sense for all grammar rules (and mixing them with a modality of
>> "external or ocaml-syntax" feels like conflating separate concerns).
>
>
> I agree.  If we have a syntax for embedding arbitrary syntax (basically, a
> new kind of string literals in expressions and patterns, with adifferent
> lexing rules, and rejected by the type-checker), let's say {{ ... }}, we
> could use it either as a stand-alone expression
>
>  {{ ... }}
>
> or as an attribute on another expression:
>
>  (@{{ ... }}) e
>
> So I don't think we need to provide parsed and non-parsed variants of
> attributes.
>
> What makes sense is maybe to distinguish attributes which can be dropped
> silently by the compiler (but used by other tools like ocamldoc, for
> instance) and those on which the type-checker needs to fail.  This is not
> strictly necessary if we already have a new kind of expressions on which the
> type-checkers fail, and it does not really bring much security because the
> user could easily use the other syntax of attributes and get (probably)
> simply a type error instead of a "remaining attribute" error.
>
>
>
>> I'd rather consider where annotation may happen for grammar rules
>> individually. For example, in the case of "let p = e1 in e2", I'm
>> quite sure we may want to annotate either the whole expression or
>> specifically the declaration, and while I see how prefix and postfix
>> both make sense for the whole expression, I'm not sure they would both
>> make sense to annotate the binding, and considering only those cases
>> could lead them to being dropped.
>
>
>
>>
>> Still in this case 'let p = e1 in e2', how should we distinguish:
>> - an annotation on the expressions 'e1' and 'e2'
>> - an annotation on the pattern 'p' (possibly seen as an expressions)
>> - an annotation on the binding itself
>> - an annotation on the expression as a whole?
>
>
> We need of course to define priority rules, but I don't see why postfix and
> prefix couldn't make sense for all constructions (maybe with some more
> parentheses):
>
> On the whole expression:
>  (@ ..) (let p = e1 in e2)
>  (let p = e1 in e2) (% ..)
>
> On the pattern:
>  let (@ ..) p = e1 in e2
>  let p (% ..) = e1 in e2
>
> On e1:
>  let p = (@ ..) e1 in e2
>  let p = e1 (% ..) in e2
>
> On e2:
>  let p = e1 in (@ ..) e2
>  let p = e1 in e2 (% ..)
>
> What's missing is maybe the ability to annotate either the binding itself as
> opposed to the whole expression (more interesting when the whole expression
> has multiple bindings: let p1 = e1 and p2 = e2 and ...).  But is that really
> necessary?  One can always use the convention that an annotation on the
> binding would actually need to be put at the toplevel of the pattern itself.
>
>
>
> Alain