[plt-scheme] Re: to define, or to let (last try)

From: Anton van Straaten (anton at appsolutions.com)
Date: Tue Apr 27 14:19:09 EDT 2004

> - all programs which abide by scheme's syntax are "correct", regardless
>   of their usefulness (and/or ambiguity under R5RS specifications).

This is a very narrow perspective which ignores many important aspects of
real programs in real life.  We've been discussing issues such as ensuring
the correctness of programs relative to their specifications.  The example
you gave:

>    (define (first x y) x)
>    (first (read) (read))

...would most likely be an example of a program that's incorrect with
respect to its specification - although it's hard to say, since no clue
was provided as to specification.

The very fact that we can tell that this program may not match its
specification, without even seeing the actual specification, is an
argument for the assertion capability in question.  The most important
ambiguity above really arises from the lack of a specification, and this
rather demonstrates the point: there's more to programs than the
"back-end" semantics of the code, i.e. what it actually does when it runs.
 It's also important whether that runtime behavior matches what we expect
it to be.

To help achieve that matchup of expectations and actual behavior, in code
we use various techniques, including comments, meaningful names (like
"first"), assertions of various kinds (including Robby's contracts), and
yes, assertions of order independence.

> - the present order-of-evaluation ambiguity as presently specified by
>   R5RS doesn't "assert" anything, it simply enables the specification
>   of "correct" programs which have ambiguous behaviors if any of its
>   arguments which are subject to unspecified evaluation order share
>   mutable state (such as basic as I/O functions do).

Again, this comes from a specific and narrow usage of "correct", which
doesn't apply to this discussion.  Most ambiguous programs, and arguably
all such programs, are in fact erroneous programs when considered in terms
of correctness with respect to the specification.  In that more relevant
and useful context, constructs which do not guarantee an order of
evaluation most certainly do act as an assertion of order-independence. 
There are plenty of references and precedents for this, including the RRRS
post which I referenced the other day.

> - if there is a community interest in enabling scheme to specify
>   immutable functions (i.e. functions which are warranted not to be
>   dependant on locally persistent, or externally mutable state) for the
>   nicety of it, for which violations must be detected, then it should be
>   addressed directly, not by attempting to argue for unspecified
>   evaluation order

Since this has not yet been addressed directly, some ability to address
the underlying issue is needed until such time as it is addressed.  As you
may know, this is an area of ongoing research.

If one is going to be extremist about disallowing features which we don't
have perfectly automatable semantic mechanisms for dealing with, then I'd
strongly recommend disallowing mutation in languages, until such time as
we figure out how best to deal with it.

>   which only ironically enables such function use to be
>   potentially ambiguous, but not deterministically so from implementation
>   to implementation, to no-ones benefit; nor as easily diagnosed as an
>   immutable function definition/assertion would be (which although would
>   be nice, it's not as truly as necessary as eliminating R5RS's presently
>   unspecified evaluation order ambiguity is, as mutable functions are both
>   useful and occasionally necessary, and corresponding their use should
>   not yield ambiguous results under any circumstances).

A program which is correct with respect to its specification should not
depend on evaluation order within constructs not intended to support such
dependence.  The above quote argues for the requirement that programs
which are erroneous with respect to their specifications, should be
consistent in behavior across implementations.  While there are some
reasons to want to do this, they're not so strong as to obviously overcome
the counter-arguments.

I'm curious: would you make the same argument with respect to the C and
C++ standards, which have very similar semantics to Scheme in this
respect?  Or, for that matter, Ada (see e.g.

> - still waiting to see someone produce a explicit code fragment which
>   demonstrates the value of unspecified evaluation order

Joe provided such a fragment, which essentially supported partial
evaluation, i.e. substitution of an argument for a formal parameter prior
to runtime evaluation.  In general, partial evaluators such as Similix,
PGG, and Schism rely on the capability we're discussing.  They're a
perfect example of a class of tools which is able to make use of the exact
information in source code which you want to eliminate.


Posted on the users mailing list.