[plt-scheme] RE: to define, or to let

> You're making a good point, that there are advantages to unspecified
> order of evaluation.  I'm surprised you were able to convince me of
> this.

Keep in mind that I'm not saying mzscheme should have unspecified order of
evaluation.  R5RS says it can define eval order any way it wants.  However,
I am saying that there's value in treating constructs like function
application and LET as not being intended for sequencing of side effects.

> But surely these advantages are too small in this PLT context:
>
> 1) MF's crew of theorem provers must have a fixed order of evaluation,
> for otherwise, as you say, the semantics are ambiguous, i.e. the
> compiler is not a function/algorithm.

Which is why they should fix the eval order, but not encourage dependency on
that order in function application, LET etc.

> 2) As you explained, the historical reason for unspecified eval order
> is C compiler speed.  It's not even a Scheme idea!

I don't think I explained that, since I don't believe that's the "historical
reason for unspecified eval order" in general.  I've previously given C as
an example of a language with unspecified eval order.  Haskell also has
unspecified eval order, but it can (probably) afford to, since it's supposed
to be side-effect free.  However, OCaml is another language with side
effects, and with deliberately unspecified eval order in its language
specification.

Here's an example of an evaluation order error in OCaml:
http://caml.inria.fr/archives/200106/msg00135.html

Note that the OCaml spec says eval order is unspecified, exactly like R5RS;
but the single OCaml implementation uses right-to-left evaluation.  The
program in the above link would have worked successfully if OCaml used
left-to-right eval order.

So, does that mean we should all use left-to-right order and be thankful
that our unintentional, unnoticed order dependencies usually work out the
way we expect?  Would you take a ride into orbit on a space shuttle if you
knew the code hadn't been checked for this issue?

Checking for order of evaluation issues is a standard part of what software
quality assurance people do.  It helps if there's a way to tell where
evaluation order is supposed to be depended on, and where it's not.

> Again, MF's crew
> of theorem provers are sharp enough to overcome the disadvantage of
> fixed left->right eval order.  So they do it.  They can & they must.

PLT isn't analyzing user programs for side effect sequence dependencies.

> 3) Your let vs let* modification of my code looks better to me.  It
> brings out your message: p and q both depend on x, but not on each
> other.  But let has similar expressiveness problems!  In the code
>
> (let ([x foo]
>       [y goo]
>       [z zoo])
>   ...)
>
> the order of evaluation of foo, goo & zoo may well matter!  To us, it
> might look like it shouldn't, but all we know by not using let* is
> that x can't occur freely in goo or zoo, etc.  Mzscheme is gonna
> evaluate foo, goo & zoo in order.

True.  And that's an aspect of the concern here.  There's potential for a
problem which has effectively been defined out of the domain of mzscheme's
semantics, by fixing eval order.  However, defining the problem out of the
language semantics doesn't eliminate it entirely.  A program with an
unintentional order dependency will be semantically legal.  However, it may
violate its specification.

It's common to use assertions in programs to make testable claims about the
properties of the program.  In addition to the testability aspect, these
assertions also provide a way to include aspects of the program's
specification within the program source code.  In a sense, they're a kind of
executable documentation, but they're a rigorous sort of documentation
because they have to follow a syntax checked by the compiler.  Comments
don't work as well for this sort of thing.  [As an aside, you can see this
in PLT's procedure type comments like "X number (number X -> true) (X ->
true) -> true".  Unless something like MrFlow reads these comments, they may
not even be syntactically correct, let alone semantically meaningful.]

Now as a thought experiment, imagine that the normal assertions you put in a
program can't ever be activated for some reason, so you can never actually
test them automatically.  Would you then remove them from the source code?

Constructs which are not intended to support sequencing of side effects make
an assertion about the code they contain.  Automatically testing this
assertion is more difficult than testing many other kinds of assertions.  So
should we remove the assertion from the code?  In other words, let's
document and be rigorous about the easy stuff, but for the tricky stuff,
pretend it's not there?

There's no simple way to address this.  If Scheme were a stricter about side
effects, it could perhaps ban side effects in specified cases, along the
lines of the C++ 'const' declaration for methods.  Because of these
declarations, C++ can statically disallow mutation of objects, where
specified.  Scheme currently doesn't support that.

But having no simple way to address this doesn't justify pretending there's
no such issue.  You might say that for the most part, we're not writing
space shuttle code and it doesn't matter enough.  That comes back to what
you wrote, "these advantages are too small in this PLT context".  That's a
judgement call, perhaps, but see below.

> 4) I feel that the real issue isn't expressiveness, but compatibility.
> Mzscheme is a fundamentally different language than R5RS Scheme.  As
> John Clements explained, an R5RS Scheme isn't valid until the
> programmer proves to him or herself that their program does not depend
> on order of evaluation!

In mzscheme, your program isn't proved valid, with respect to its
requirements, until you've proved that there are no places where you have
depended on order of evaluation unintentionally.  It's difficult to do that
if the program doesn't even contain any indication of where order of
evaluation dependencies are or aren't intended.  Remember, too, that in our
functionally-oriented programs, we want to keep side effects to a minimum.
They should be the exception, not the rule.

Because of this, it make sense to use special constructs, like BEGIN, LET*,
LETREC* when we want to depend not only on side effects, but the sequence of
those side effects.

That's actually a pretty basic point!  We're not writing Python here, in
which state is primarily communicated by side effects.  Even fairly
imperative Scheme programs include lots of big nested expressions, most of
which do not actually depend on side effect sequence.

> In Mzscheme, you don't have to prove it, and
> as you say, the programmers won't prove it, and then their programs
> will misfire on other fine Scheme interpreters.

They might misfire on Mzscheme, too.  Exercise for the reader: come up with
a scenario in which an unrecognized side effect order dependency, as in the
OCaml example above, works in testing but fails in live operation.  For
inspiration, you might look at Ariane 5, the $7 billion poster child for
latent bugs.

> (Actually I don't
> know: Do Larceny, Gambit & Trotsky do left->right eval order?)

SISC does right->left.

> But I'm in favor of deviation myself.  As Shriram posted a long time ago,
> we don't think of Python and Pearl as being dialects of the same
> language, so why Mzscheme & Guile?

You want I should shoot those fish?  I guess not:

> That's kinda like shooting fish in
> a barrel, but think big: why Mzscheme & anyscheme?

Aside from the now-notorious letrec/letrec* issue, I'm all in favor of the
extensions that PLT provides.  Afaik, most of them are allowed by R5RS -
actually, they're outside its scope, so the question of non-standardness
doesn't arise.  I'd even be in favor of some standard-violating extensions,
if they had a big enough benefit.  However, it's not clear to me what
benefit PLT gets by encouraging the use of function application, LET etc. as
sequencing constructs.  To me, the portability question here is secondary.

Anton