[E-Lang] ERTP-aware MintMaker

[Mark S. Miller]

At 04:23 PM Wednesday 2/14/01, steve jenson wrote:
>According to "E in a Walnut", and MarkM himself, there is going to be
>a new keyword in the language called "describe" which will take care
>of this sort of self-referencing issue. Therefore my code, while 
>stylistically ugly, is the cleanest to fix upon completion of that
>function to the language.
>
>At least, that was my take on it. And I'll certainly concede to you having
>picked a cleaner way of doing it if I hadn't known of forthcoming changes
>to the language.

Actually, the proposed keyword is "declare", although I think either Dean or 
MarcS suggested "forward" and Dean suggested "promise".  Plausible also is 
"introduce".  Now's as good a time as any to publicly propose this.  For the 
moment I'll say "declare", but let's postpone arguing about the keyword until 
we figure out whether it's a good idea (or invent a variant that is a good 
idea).

Let's also ignore the top-level mutable interactive scope issues for now, 
though we must revisit them before we can consider the proposal to be baked.

Generally I like to define the semantics of E simply by defining the 
semantics of Kernel-E, and then defining the syntactic expansion of E to 
Kernel-E.  This approach is often adequate.  But sometimes it's good to also 
try to define semantics directly at the user level as well, to see if the 
rules are regular and predictable enough to be used reliably, without having 
to mentally expand to Kernel-E.  The left-to-right scoping rules, which the 
"declare" proposal extends, was our main example of this, so we continue the 
tradition of defining the scoping rules first at the user level language.


                       Informal User-Level Semantics


"declare foo" introduces "foo" into a scope without defining it.  It's a 
forward declaration.

A forward-declared variable must be defined in the same scope, and must be 
defined as final.

If you use a variable before it's defined, you get a promise for what it 
will be defined as.

The variable definition resolves these promises to the variable's value.

So our original example:

>     var delayedMint := null
>     define issuer {
>         to makePurse() :any {          
>            delayedMint makePurse(0)
>         }
>         ...
>      }
>     define mint { ... }
>     delayedMint := mint

could instead be:

>     declare mint
>     define issuer {
>         to makePurse() :any {          
>            mint makePurse(0)
>         }
>         ...
>      }
>     define mint { ... }

At the time issuer is defined, its "mint" is a promise,  For typical 
patterns (including our MintMaker), by the time the issuer might try to use 
the variable, it will simply be the mint (ie, resolved to the mint).


                          Semi-Formal User-Level Semantics


"declare foo" introduces the name "foo" into a scope-box 
http://www.erights.org/elang/blocks/ifExpr.html .  We say this "foo" is an 
"introducing" occurrence of "foo".  There may not be more than one introducing
occurrence of an identifier directly in any one scope box.  (Another introducing
occurrence of "foo" may still occur in a nested scope box.  Hence "directly" 
above.)

"declare foo" is an expression, but for now let's restrict it to expression
contexts for which it's value is never needed, such as a non-last expression 
in a sequence-expression (a sequence of expressions separated by ";" or "\n").

The name "foo" is "in scope" from an introducing occurrence, left-to-right, 
until the end of the scope box, including within nested scope boxes, except 
where shadowed by introducing occurrences in those nested scope boxes, in 
the usual manner.  A use occurrence of "foo" must occur only where "foo" is 
in scope, and is bound to the corresponding introducing occurrence.

A "defining" occurrence of "foo" is exactly what it is now -- "foo" used as 
a DefinerPattern, possibly preceded by "var", and followed by a guard 
expression (eg, "foo :guardExpr").  There may not be more than one defining 
occurrence of an identifier directly contained in any one scope box.

If a scope box does not directly contain a "declare "foo", then everything 
works as it does now, and is therefore fully upwards compatible.  ("declare" 
is already a reserved keyword.)  In particular, if such a box does directly 
contain a defining occurrence of "foo", then this is also an introducing 
occurrence, and, as always, "foo" is "in scope" from the introducing 
occurrence, left-to-right, until the end of the scope box.


If a scope box directly contains a "declare "foo", then a defining 
occurrence of "foo" must occur left-to-right between the declaring 
occurrence and the end of the scope box, ie, within the area where foo is in 
scope.  The scope box must directly contain the defining occurrence.

Among text directly contained within a scope box (equivalently, the leaves 
of the tree of expressions and patterns not including those in nested scope 
boxes), there is both the left-to-right order (LRO) as used above, as well 
as Static Temporal Order (STO).  Static because it doesn't depend on runtime 
conditions, and so is easily statically apparent.  Note that all flow 
control boundaries are also scope-box boundaries, which is why STO is 
possible so long as we restrict our view to direct containment.  Mostly, STO 
follows LRO, which is why defining a variable textually before (to the left 
of) using it typically implies that the variable will actually be 
initialized temporally before it's used.

E has two exceptions to this rule: The DefineExpr ("define pattern := expr") 
and the DefinerPattern ("[var] name :guardExpr").  In both cases, the right 
branch happens first, and then the left branch.  For these LRO and STO are 
different.

A use occurrence of a name may then only occur LRO-after an introducing 
occurrence.  In STO, it may occur before of after the defining occurrence.  

If a use occurrence occurs STO-after the defining occurrence, then it is a 
"direct-use", and refers to an already initialized variable.  As an 
expression, it evaluates to the value of that variable.  

If a use occurrence occurs STO-before the defining occurrence, then it is a 
"promised-use", and may only appear as a name expression (ie, no 
"foo := ..." or "&foo").  A promised-use expression evaluates to a promise 
for the value of the variable.  A variable that has a promised-use may only 
be declared non-var, or equivalently "var foo :final" or 
"var foo :final(valueGuardExpr)".  In other words, only immutable variables 
can be promised.  STO-after the defining occurrence, these promises are 
resolved to the value of the variable.  So if the variable is initialized 
with a NEAR reference, STO-after the definition the promised values are also 
NEAR.

These spec accounts both for the existing to use "define" for circular 
definitions http://www.erights.org/elang/blocks/defVar.html#scopeConsistency 
, as well as the proposed meaning of "declare".


              Expansion to Kernel


This proposal involves no change to Kernel-E, and only an upward compatible 
change to the expansion.  We distinguish two cases: variables for which 
there is a promised-use occurrence, and those for which there is not.  For 
the latter, there is no change to the expansion.  For promised-uses, we 
describe the expansion as two phases.  We believe it can be painlessly 
implemented in one.


      Phase 1:


There are two constructs for which STO != LRO, the DefineExpr and the 
DefinerPattern.  If a promised-use of a variable occurs on the right of one 
of these, for which the introducing use is on the left, then this variable 
use is STO-before its introduction.  Let's call this a cyclic variable use. 
To keep Kernel-E's semantics and implementation simple, Kernel-E rejects any 
programs with cyclic variable uses.  (Kernel-E already does this.  This 
terminology is simply a new way to describe it.)  How do the user-level 
forms of these constructs cope with this restriction?

* The user-level DefineExpr allows cyclic variable use: The expansion of 
these precedes the define with "declare"s of the cyclic variables, to be 
expanded out by Phase 2.  So

    define x := [1, x, 2]

expands to

    declare x; define x := [1, x, 2]

The "x" on the right of the "define" is still a promised-use, but no longer a cyclic-use

* The user-level DefinerPatterns rejects programs with cyclic-use.  There's 
no reason to go out of our way to accept cycles here.


      Phase 2:


The declare turns into an expression for making a promise-pair:

    declare foo

expands to

    define [foo__Promise, foo__Resolver] := PromiseMaker()

A promised-use occurrence (one that is STO-before the defining occurrence) 
refers to the promise facet of the promise pair:

    foo

expands to

    foo__Promise

The defining occurrence also resolves the promise:

    foo :integer

expands to

    foo :integer ? (foo__Resolver resolve(foo); true)

The "?" is read as "such that", meaning that the pattern as a whole succeeds 
at matching a specimen if the left hand pattern matches, and then the right 
hand expression evaluates to true.  Here we are using the such-that pattern 
not to add a test, but to cause an effect at the time we need to cause it.

and non-promised use occurrences are fine as is.



              Minor Fly in the Ointment


This expansion involved turning a definer pattern into a such-that pattern.  
This requires that the grammar be changed to accept a <pattern> (the more 
general production that includes the such-that pattern) everywhere it 
currently accepts <namer> (which corresponds to what I've been calling a 
definer pattern).  I just checked with yacc, and yacc is happy with this 
change.  So the only issue is whether we're happy with it.

The actual requirement is less stringent -- the grammar only has to accept 
patterns for those productions that are also in Kernel-E, in order for 
Kernel-E to remain a subset of E.  However, if we're going to make this 
change, we should do it for the whole language for consistency.  Yacc is 
happy with the change applied to the whole language.

I think this is a good change anyway, as the old grammar's non-uniformity 
wasn't well motivated, and the above case shows that it was less 
compositional than one would like.



                      A Call For Help

There are people on this list who are extraordinary at writing formal 
documentation that is simultaneously clear, unambiguous, readable, and 
non-redundant.  Above I demonstrate my lack of skill in this regard.  But I 
don't know what I'm doing wrong.  If you have any insights that may help, 
please let me know.  Thanks.  As a language designer, this is a skill I need 
to learn.



        Cheers,
        --MarkM