[E-Lang] Thanksgiving present for E programmers

[Mark S. Miller]

At 06:54 AM 11/22/00, Jonathan S. Shapiro wrote:
>Language lawyer warning:
>
>> E's :type syntax, as you clearly fully understand from the
>> rest of your message, expresses a check that must be performed at runtime.
>
>I'm sure this is an accurate statement of what is actually required, but it
>is a bad statement of specification. A (possibly) better statement of
>specification is:
>
>    E's :type syntax expresses a predicate that must be true
>    at runtime for execution to follow the normal flow of
>    control. If the predicate is false, an exception is thrown (?).
>    The predicate is normally verified by a runtime check,
>    but the compiler is free to optimize this check away if
>    it can determine statically that the check is unnecessary.
>
>I believe this is consistent with the rest of your note, but I think this
>verbiage makes a clearer statement of the requirement. If you don't like the
>word "predicate" for your readers, substitute "type requirement".

You're going in the right direction.  A clear statement is somewhere between 
yours and mine.  The issue is that the check may be coded in E, and may 
therefore have side effects or other time dependent behavior.  While this 
isn't recommended, the semantics specify a simple sequential run time model 
where the check "happens" at a given time in the computation.  It's exactly 
like the issue of specifying the semantics of

    if (foo()) { ...

in any C-like language.  Depending on compiler cleverness, the actual order 
in which things happen, or whether they can even be said to happen at all, 
can be almost anything.  However, since foo() may effects beyond evaluation 
to a value (cause side effects, read state side effected by others, throw an 
exception), C-like languages specify exactly when foo() must seem to have 
been called.  

How do instruction set designers phrase such things?  The same issue arises, 
and instruction set designers often know how to speak more precisely than do 
most language designers, including myself. 

Since foo() above is assumed to evaluate to a boolean, one might also call 
it a "predicate", but, like the E :type check, it isn't something a 
mathematician would recognize as a predicate. Which reminds me of another 
very cool thing about E: Since E will have checkable confinement by auditing 
(step #2 of http://www.erights.org/elib/capability/factory.html ), when the 
programmer wishes to ensure that a "predicate" he's calling has no side 
effects, and is therefore closer to the mathematician's "predicate", he can 
first check that the predicate is confined:

    def safeFoo :confined := foo
    if (safeFoo()) { ...

If foo is not checkably confined, the attempt to define safeFoo will
throw an exception, and safeFoo will never come to be in scope.  Similarly for

    def safeType :confined := type
    def x :safeType := y

Such code sequences may very well help out the compiler as well as the 
programmer, as it provides more guarantees about what re-orderings cannot 
change the semantics of the program.

>A proper specification, of course, must also specify the interaction between
>the predicate check and the inheritance design, if any. Accompanying
>explanatory notes should identify any hazards associated with this
>interaction -- I'm thinking here about a statement to the effect that
>inheritance frequently obscures contravariance bugs, and that depending on
>the satisfaction criteria the meaning of the type check differs.

All valid points, but fortunately not yet relevant for E.  E has no 
kernel-level inheritance, and the inheritance it does have 
http://www.erights.org/elang/blocks/inheritance.html is just syntactic sugar 
for a pattern of delegation.  E has no separate declaration of a typed 
interface that an implementation could be said to implement or not.  OTOH, E 
needs such a declaration, and the upcoming release will experimentally 
introduce the beginnings of one, so these issues will probably eventually 
become relevant.

Fortunately, the perspective presented by Giuseppe Castagna's amazing paper 
"Covariance and Contravariance: Conflict Without a Cause" 
ftp://ftp.ens.fr/pub/dmi/users/castagna/covariance.ps.Z (found by Eric 
Drexler) suggests that, by starting with a runtime checking approach, we may 
be closer to supporting the right solution than one would have thought.  
However, at this point I'm going to beg off further exploration of this 
topic.  Static type theories make my brain ache, which is one of the reason 
E moves the problem to (apparent) runtime and leaves it to other to build 
static checkers outside the language.


>> By "static" checking, I've always meant rejection sometime before the
>> program is allowed to begin execution.
>
>Nit: I think you mean "...before the program is considered semantically
>meaningful." Or perhaps "...before the program is well-formed."

These others are good as well, but I meant what I said, which is the 
operational issue.  Were I to say, for example, "...before the program is 
well-formed", I'd still need to say that a non-well-formed program may not 
be allowed to start executing.  I'm just cutting out the middle manpage.


    Cheers,
    --MarkM