[E-Lang] List of core E features?

Vijay Saraswat vijay@saraswat.org
Tue, 02 Oct 2001 23:32:30 -0400


Mark S Miller wrote:

> At 07:05 PM Saturday 9/29/01, Vijay Saraswat wrote:
> >Talking about language definitions, it might be good to get a Scheme-like
> >language definition document going for E...
>
> Ever since you brought this up, I've been very excited by the prospect!  As
> with Walnut, I probably don't have the right talents to be the first author
> on such a document (I'm weak on formalisms), but I'd greatly enjoy helping
> someone who's taking the lead on this.
>
> Should we call it R0RE?  (That's a zero, btw).

Sounds fine :-)

> At 05:28 AM Monday 10/1/01, Vijay Saraswat wrote:
> >I am trying to get my head around the core set of E-featues (at say the
> >level of Kernel E) so that one can start thinking about an abstract
> >syntax, and a structural operational semantics.
>
> For a start on an abstract syntax, see
> http://www.erights.org/elang/kernel/index.html and
> http://www.erights.org/javadoc/org/erights/e/elang/visitors/ETreeVisitor.html
> .  Is this approximately what you mean by abstract syntax?

Yes, but the idea with the abstract syntax is not to worry too much about
concrete syntax (e.g. details of literals, comments, dot versus space etc.. stuff
that is important for readability of large programs but distracts from the task
at hand which is to capture the essential syntactic structure of the language so
that the semantic structure can be tied to it).

> What's a "structural operational semantics"?

A style of giving operational semantics to a programming language popularized by
Gordon Plotkin in the early 80s which really brings a similar elegance and taste
to bear on the treatment of syntax as logicians had been bringing to the
treatment of semantics. In particular, transformations are defined on finite
inductively defined configurations via inductively defined rules which are
generally intended to be very easy to understand.

>
>
> >I have repeatedly found
> >that doing such a semantics helps elucidate many notions, and helps
> >separate out ideas that perhaps belong in the implementation (and hence
> >are primarily useful to language implementers)  from ideas that belong
> >in the specification (and hence are primarily useful to programmers
> >writing in the language, and people who want to reason about programs in
> >the language).
>
> Sounds great.  I would certainly expect to see such benefits.
>
> >(There is no dearth of strong claims on the E-rights website that would
> >be great to get some formal backing for!!)
>
> Indeed!  I believe I have a good eye for claims that can be backed formally,
> but I don't have the background to actually produce these formal backings.
> Once they are produced, I hope I'll be able to follow them ;) !
> I'm *very* excited.
>
> One of my biggest difficulties getting into most formalisms in CS is a
> seemingly trivial matter -- notation.  I find programming language
> conventions to be vastly more readable than math conventions.  If you don't
> mind, could we write these formalisms as follows?
> 1) Readable identifiers rather than single letters.
> 2) Stick with ASCII and avoid Greek.
> 3) Be "positional" only in the left-to-right sense, with no subscripts,
> superscripts, line-spanning brackets, etc.
> 4) Follow simple principled scoping rules -- just straight lexical scoping
> if possible.
> Such rules would greatly aid my ability to follow along.  Thanks.
>

We shall endeavour to please :-). Avoiding subscript and superscripts could be a
bit hard though :-). Greek we can avoid :-) (I take it by Greek you also mean
Sanskrit... I always wondered why, given that its all Greek and Latin anyway, we
couldnt use Sanskrit symbols :-))

>
> >So here is my current list of "features"... please let me know if I am
> >missing something.
>
> More later...
>
> >The next step would be to get an abstract syntax
> >together that doesnt miss out on anything critical, but is simple enough
> >that one can give a formal presentation of its semantics.
> >
> >  Vats (cc)
>
> What does "cc" mean?

Just a note to myself that these ideas were treated earlier in the concurrent
constraint programming work as well. Not particularly illuminating in the current
context, more a note to myself.

> >  Lexical, nested scope (cc)
> >  Multiple "methods" per object
> >  Pattern-matching selection (cc)
>
> Might not mean what you think it means.  In an object expression, method
> dispatch is based purely on message name and arity.  An object definition
> may have at most one method definition of a given name and arity.  I easily
> could have dispatched by matching on the "head" -- the parameter patterns,
> but for reasons explained below, I decided not to.
>

Fine.

>
> If you want this effect, you can use the optional "match" clause[s] at the
> end of the object definition to achieve it:
>
>     def obj {
>         match [`run`, [x :integer]] {
>             # ...
>         }
>         match [`run`, [[car] + cdr]] {
>             # ...
>         }
>     }
>
> This is like an object with two 1-arity run methods, where the first is
> invoked if the argument coerces to an integer, and the second if it coerces
> to a non-empty list.
>
> This expands to
>
>     def {
>         match temp {
>             switch (temp) {
>                 match [`run`, [x :integer]] {
>                     # ...
>                 }
>                 match [`run`, [[car] + cdr]] {
>                     # ...
>                 }
>             }
>         }
>     }
>
> which expands to
>
>     def {
>         match temp {
>             if (temp =~ [`run`, [x :integer]]) {
>                 # ...
>             } else if (temp =~ [`run`, [[car] + cdr]) {
>                 # ...
>             } else {
>                 throw("no match: " + temp)
>             }
>         }
>     }
>
> which is how Kernel-E gets away with having at most one match clause in an
> object definition.
>
> The reason a "to"-defined method is not expanded into yet another branch of
> the switch is so a failure of parameter match can be treated as an error,
> rather than falling through to the match.  A clever expansion can get the
> best of both of these worlds while being fully upwards compatible from the
> current E, but the need hasn't yet arisen.
>
> >  References and promises (cc)
> >    near, far and broken
> >    partial order on bindings
>
> "bindings"?  Partial order on message delivery
>

Fine -- at some level these might become bindings of variables to values that are
commuincated from one site to another site. Again, I am thinking of how we were
modeling distributed cc (dcc) back in the early 90s at PARC.

>
> >  Control structures
> >   Mutable object-local state (assignment)
> >   Synchronous calls on near references
> >   Send
> >   Sequencing
> >   Throw/catch/finally
> >   Conditionals
> >
> >  Primitives
> >   Timers
>
> Depends what you mean my "Primitives".  I would say "3" is a primitive, but
> Timers and Files are "devices".
>

By primitive I mean constructs that are not reducible to other constructs in the
language but must be treated in their own right. 3 gets treated the same as 41
:-).. as a "built in literal", which for purposes of semantics we can probably
ignore, unless something magical is being done with them :-)

>
> >   Seal/unseal (rights amplification)
>
> MarcS figured out how to write these in unprivileged E.  (Need link to long
> discussion on e-lang.)  The result has slightly different semantics, and
> MarcS' semantics are better.  Unfortunately, due to layering considerations,
> these will continue to be primitive, but they need to be made equivalent to
> MarcS' code.
>

OK cool, I will take that as given for now, and not focus on this.

>
> >  (Persistence? Not much description yet!)
>
> Not much of anything yet.  Don't hold your breath on this one.  Although I
> will try to post some descriptions fairly soon, it probably won't be ready
> for this kind of formalization for a while.
>
>         Cheers,
>         --MarkM

OK, so we will punt on this for now.