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

> Anton, I said I was out, but you're so sharp & so much fun:

Thanks, I only hope other readers of this list are having as much fun.

>    Remember, too, that in our functionally-oriented programs, we want
>    to keep side effects to a minimum.
>
> I have a related opinion: There's nothing special about Scheme, other
> than the Lambda Calculus, or really, Plotkin/Felleisen LC_v.

I partly agree.  There are some fairly unique things about Scheme, though,
which PLT is taking full advantage of: in particular, macros.  Languages
like Haskell have attempted to do without them, but even leading members of
that community recognize that they're missing something.

> That's why RnRS is busted.  It's not because Clinger et al did did a bad
job.
> It's because we haven't figured out the right language yet.  That is:
>
> LC_v is great, and Scheme is LC_v with some mutation slapped on.
> Users demand mutation, but there's various ways to slap it on, and I
> don't think anyone's figured out the "right" mutation-ality.

I agree with the latter sentence.  I can't agree that R5RS is busted.
Incomplete, sure - there are many things it doesn't address.  And it has its
quirks.  But compared to other language specs??  I think, in some ways,
you're spoiled by R5RS.  You don't realize how good it is, compared to what
else is out there.  There are some specs, like SML's, that are more rigorous
and complete than Scheme's, but they describe a language which in a sense,
is almost domain-specific: SML is a type-oriented language.  Scheme is more
general, and pretty unique in that respect.

> So RnRS isn't a language spec, but a historical description.
> There's no reason to follow it.

That's only true if you come up with something better.  Matthias has talked
about developing a more ambitious spec for Scheme, and I think that would be
great.  I doubt anyone is against that.  But otherwise, there are plenty of
reasons to follow R5RS.

> Mzscheme forges ahead in a new mutation-ality
> direction: uniform left->right eval order, sequencing in letrec, etc.
> These are features to take advantage of, and no longer bugs.
> I don't have an opinion about whether this is better for the Scheme
> programmers.  But it's better for the PLT maintainers, because their
> Math skills require fixed algorithms.

You seem to be missing my point, that I'm not saying Mzscheme shouldn't fix
evaluation order.  What I'm describing doesn't affect PLT's semantic
analysis capabilities.  All I'm saying is that the constructs which R5RS
says have unspecified order should not be treated as being intended for
sequencing of side effects.  They can still actually evaluate left to right,
though!

This has an effect on how code is written, even if some programmers ignore
it.  It allows an assertion to be expressed in code, an assertion which is
being discriminated against because it's not easy to fully test, and because
it's subtle.  PLT can ignore that assertion in semantic analyses, which
makes sense, since it's tricky to deal with automatically.  There's no
reason to eliminate the ability to express it, though, from the semantic
analysis perspective.

What confuses the discussion is that R5RS has unspecified order.  It sounds
like you'd like to see that changed.  That's actually a reason that R5RS
should be respected, though - it reflects more than a single group's
perspective, and it's conservative in a certain sense (not in the sense PLT
would like, perhaps).  That's a good thing.  In this case, the unspecified
order is a red flag that there's something to pay attention to there.  If
R6RS were to fix eval order (although I don't think it should), I'd vote for
right to left, on principle, like the OCaml implementation, MIT Scheme, and
SISC.  Again, that would highlight the issue, and discourage people from
abusing those constructs - and it doesn't cause any problems for semantic
analyses.

> Quite likely, it will turn out
> to be better for schemers.  If not, it will be a good experiment.

Fixing left-right eval order, in a language implementation, isn't an
experiment, it's a common practice.  But it really doesn't have that much to
do with my main point.

>    > 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.
>
> Maybe you misunderstood me.  I meant that the PLT folks can reason
> successfully about algorithms, including their left->right
> interpreter.

I wasn't clear enough myself.  I'm saying that side effect order
dependencies are something programmers do care about, even people who don't
agree with my position on this.  PLT isn't doing anything to analyze or
report on those dependencies.  Given that, programmers should be able to say
something about the issue in their code, since they're the ones who need to
worry about it.  PLT doesn't have to worry about it.  PLT should add text
such as the following to the manual section on evaluation order:

"Although PLT Scheme guarantees left-to-right evaluation order, evaluation
order should not be intentionally relied on in function application, LET,
etc.  Programs can be dynamically checked for violation of this rule by
running test suites using the BrBackwards tool[*]"

The manual would then need to go into a ten-page, closely argued rationale,
intended to demystify that statement for current & future generations.  It
shouldn't be any more difficult than coming up with unambiguous markers to
place around Yucca Mountain so that our great^20-grandchildren will know not
to go digging for root vegetables there.

> As MF posted, they can even optimize Mzscheme, e.g. by
> proving sometimes that they can safely switch the order of evaluation.

Right.  This brings us back to the question of how the program matches its
specification.  MzScheme can, on a good day, prove some parts of something
the programmer already knows about the program, or thinks he knows.
MzScheme is not going to be as good as a good programmer at doing this,
though, not without changes to the Scheme language.  Given that the user is
good at figuring this out - which we know from experience with C, C++,
OCaml, and MIT Scheme - and that the compiler's not so good at it, how does
it make sense to remove the ability to express the issue in question?

You need to express it so that the programmers can do their job, which is
making sure the system works the way it's supposed to -- that there's a
match between the specification, the executable program, and the
programmer's mental model.  How do you ensure that multiple systems match
up?  You compare the things they say, see if they match.  Take out the
ability to say something, you can't compare it any more.

>    > As John Clements explained, an R5RS Scheme program 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.
>
> No, I don't want to say a program is invalid if the user doesn't fully
> understand why the program works.

That's too narrow for the real world, and actively dangerous, not just
related to the issue we're discussing.  All Robbie's work on contracts would
be unnecessary if this was really considered to be the case.  Contracts are
about redundancy, about validating assumptions, about matching the actual
program to other models, like the specification and our mental models.  We
all care about more than just the semantics of the actual, typed-in source
code.

> John's meaning of invalidity is if
> the R5RS program won't run correctly if compilers switch the order.

That's a valid view for an R5RS program.  I don't think PLT needs to worry
about that.  Let programmers who want portability worry about it, or let my
new argument-order torture-testing tool worry about it:

  (module zmscheme mzscheme
    (define-syntax zm-app
      (lambda (stx)
        (syntax-case stx ()
          ((_ f arg ...)
           (with-syntax
               ([(gra ...) (reverse (syntax-e (syntax (arg ...))))])
             (syntax
              (f gra ...)))))))
    (provide
     (all-from-except mzscheme #%app)
     (rename zm-app #%app)))

  (module tset zmscheme
    (define showarg
      (lambda (x)
        (display x)(newline)
        x))

    (display (+ (showarg 5) (showarg 6))))

  (require tset)

=>
   6
   5
  11

Now, the order-independence assertion provided by function application & LET
is dynamically testable.  Future versions will support random shuffling of
arguments, and other neat features.  I hereby dub this new tool
BrBackwards - Brother Backwards - and donate it to the PLT project, which
can mention it in its next funding proposal.  However, it would be a pity if
this tool were to become useless merely because of a de-emphasis of the true
nature of function application and LET...

 :o)

Anton