Well, the list has been quiet of late, partly because I've been pushing at
implementation. There has been a bunch of useful chat on the IRC channel
recently; most of the live traffic has been going on over there for the last
two weeks. Very helpful, but it's time to stir things up over here again so
that we can archive the food fight.
My view on mixfix is evolving. Partly because I'm coming to understand how
to do it, and partly because it will make the transition from the
S-expression syntax easier to do. I want to describe why, and then describe
where I think I want to go with mixfix in BitC and *why* my views are
evolving.
I do continue to have some concerns about audit, but I'm coming to the view
that the combination of lexical scoping and audit support tools resolves my
major concerns as far as mixfix is concerned. I'll be damned if I know what
emacs-mode should do in the presence of mixfix, though. Anyway...
*What Started My Shift?*
Ironically, it may have been the syntax transition that pushed me over the
edge.
For the moment, the tokenizer assumes that any given top-level form is
either fully an S-expression form or fully a new-syntax form. The tokenizer
behaves in a modally different way for the two types of forms. Most notably,
things like "==" are returned in new mode as tokens, where in the
S-expression mode they are just identifiers. In order to transition the
syntax, it really helps to re-converge the tokenizer. The part of
convergence that is tricky (as opposed to laborious) is that I need to
eliminate the modal behavior in the tokenizer first.
One view of mixfix is that this is how Haskell eliminates keywords - by
separating parse structure from the parse-time keyword/identifier
distinction. So one approach to converging the tokenizer is to adopt mixfix.
In poking around the various approaches to mixfix, I feel that I like the
richness of Agda on general mixfix (but see below about precedence
ordering). That said, Haskell's infix-only mechanism mostly suffices in the
near term. It's relatively simple, and extensible in pretty much any of the
other directions we might later want to go (because it's a subset).
My other thought is that if we couple the "lightweight lambda" idea with
mixfix, we gain much of the power of macros without most of the problems. It
doesn't replace macros, but it covers a large and useful class of things
that macros are commonly used to achieve. More so if we (eventually) extend
mixfix to let the holes specify associated syntactic categories.
*Lightweight Lambdas*
The lightweight lambda idea is simply that every block (bracketed expression
sequence) is treated as sugar for a lambda introduction having type
unit->'a, where 'a is the result value of the block. In this view, the LET
construct takes a *nested procedure* as its body and evaluates that
procedure in the let-bound environment. The only impact this has on the
current language is that it changes the behavior of things like:
expr;
{ // introduce new block. This now forms a lambda
// rather than introducing a sub-context
expr;
expr
};
expr
In C, we would do something like this to control variable scoping. In BitC,
blocks aren't associated with scopes, so the corresponding code should
instead be written as:
expr;
let *bindings* in {
// introduce new block. This now forms a lambda
// rather than introducing a sub-context
expr;
expr
};
expr
That is: if lightweight lambdas break your code, the code was doing
something suspicious in any case.
To take advantage of lightweight lambdas, the mixfix syntax needs to be able
to do implicit thunkification. We do this widely in any case. For example,
the layout engine "knows" that it should insert '{' after LET and IN, which
is how:
let *bindings* in
*expr*
turns in to
let { *bindings* } in {
*expr*
}
But if we add brace injection to the mixfix notation (say, using '#' instead
of '_'), we can then to things like:
mixfix *precedence* while#do#;
def `while#do#`(tst, body) =
loop while tst() do body();
and we've just introduced the simplified "while" loop as a non-primitive
construct.
I'm not sure that implicit thunkification is actually a good idea. Mark
Miller argues that it is not. But I think it's a worthwhile thing to play
with briefly. What we're *not* getting here, in comparison to macros, is
anything that lets us rewrite ASTs.
*The Conceptual Logic of MixFix*
Long term, I like the more syntactically complete view of mixfix that Agda
is introducing. What seems odd to me is how complicated the current
literature on mixfix processing models makes the issue seem. If there is a
clear discussion of how to *think* about the interaction of mixfix with
conventional parsing, I haven't seen it anywhere - and I really have looked.
Parser combinators may or may not be a clever implementation technique, but
they aren't the right way to think about how mixfix behavior is specified!
My current (probably ignorant) sense is that the complexity of mechanism
being discussed is a bit silly.
>From a specification perspective, I believe that the right way to view
something like
mixfix *precedence* while#do#
is that it is adding a production to the language grammar at compile time.
This production is inserted in a well-defined part of the grammar, and it
should be processed according to the same rules as any other production.
That is: we end up specifying that the BitC grammar is processed [as if] by
a prioritized LALR(1) algorithm, that the processing of a mixfix form is
simply adding a new rule to the grammar, and that the lexical expiration of
a mixfix form is removing that form.
In reading through the various discussions of mixfix, the main issues I see
in the literature *seem* to boil down to two questions:
1. Should precedence relations be transitive? Danielsson's Agda slides
give some examples where this leads to funny outcomes.
2. When should ambiguities introduced by mixfix introductions be
diagnosed? The choices seem to be:
1. At the point of introduction (early), or
2. At the point where ambiguous input is actually encountered (late)
Late diagnosis is undeniably useful, but it violates *decades* of wisdom in
software engineering, which is something nobody seems to talk about. The
arguments for late diagnosis seem to be that:
1. It is often the case that ambiguous translations exist, but are never
encountered in practice. All well-formed examples of this involve precedence
ambiguities between operator pairs that are never observed together in the
input.
2. It is sometimes the case that there is a shift/reduce ambiguity. In
all examples I have seen, the general rule holds: the right thing to do
always turns out to be "shift", but in any case, the ambiguity can be
resolved by prioritization.
The part of the argument that I find interesting is the "never encountered
in practice" part. What I think is *really* going on is something more
subtle:
1. Most uses of mixfix "fit" the regular precedence hierarchy
comfortably. That is: you can find an available spot for them in the
available precedence hierarchy *and* applying the precedence rules in a
transitive way doesn't result in any surprises.
2. A few uses of mixfix are sophisticated, and are introducing completely
different syntactic schemas than the ones that are conventional in
programming languages. Either there aren't enough levels available to insert
the right operators in the desired ways, or it is truly necessary to change
the *relative* precedences of certain operators in the context of the new
sub-language. That is: you are designing a new, specialized expression
language rather than tweaking an existing one.
The second case, I believe, is the one where people are getting in trouble
with transitivity. The argument in the Agda paper, in my view, that
there *shouldn't
be* a transitive precedence resolution between logical and arithmetic
operators is mistaken If there is no valid typing of the expression (as is
true in those examples), then by all means let them fail to type check. For
the sake of layering, we really want parsing to be type- and semantics-
oblivious. Basically, I'm arguing that non-transitivity of precedence
amounts to solving a problem in the wrong layer, and that precedence orders
should always be associative.
*First-Class Syntax*
The evident *problem* with my view is that you sometimes (lexically) inherit
operator bindings or precedence choices that don't work for your specialized
embedded language, and there isn't really a way to get rid of them. It seems
to me that the right solution here is to introduce a notion of a "syntax
table", so that you can write something like:
with syntax *mySyntax*
*sequence of forms*
The interpretation of a mixfix introduction is that it modifies the current,
lexically-prevailing syntax.
>From an implementation perspective, this amounts to exposing in the syntax a
mechanism that the compiler must already have internally. The only new
element here is to have a new defining form for introducing syntaxes. But
that's just something like:
syntax *mySyntax* {
*sequence of mixfix introductions*
}
the only difference being that mixfix introductions appearing within a
syntax construction are durable: they are added to the syntax as-written,
but they aren't removed at the closing curly brace.
But this has a consequence: the introduction of syntax has to be a binding
construct, because different operators may end up binding the same function
in different syntaxes. So we need to use something like:
mixfix *precedence* _+_ = add*;*
where "add" is a function of two arguments. If we take the view that a
mixfix introduction adds a production to the parser, note that we have just
defined the associated parse action, and further, that the parse action is
pure (side-effect free). This means that the "mixfix just adds a production"
rule does not inherently place any constraint on our choice of parse
algorithm - though it does mean that we have to specify one as part of the
language specification.
I suppose that what I find interesting about all this is several points that
I haven't seen touched on in the literature:
- The idea that mixfix introduces productions in the existing grammar,
rather than an isolated sub-grammar. This view seems necessary for mixfix to
be coherent with the surrounding language.
- The idea that a mixfix "hole" has an associated syntactic category, and
that there is no inherent reason to limit this to just one syntactic
category.
- The idea that a collection of mixfix introductions can be gathered in a
first-class language construction (which I have called a "syntax table")
- The idea that the *concept* of mixfix can and should be described and
framed independent of any particular implementation strategy.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
