The status of type rules in Standard ML

[William D Clinger <will@ccs.neu.edu>]

> > (Standard) ML as _a language_ is defined with a particular static type
> > discipline -- programs that violate it are illegal.
> 
> i unfortunately have not seen the language definition. do you remember
> offhand how it is specified exactly?

In its Preface, "The Definition of Standard ML", by Robin Milner,
Mads Tofte, and Robert Harper, introduces the

    B |- P => M

notation, and then says in italics:

    The formal purpose of this Definition is no more, and no less,
    than to decree exactly which assertions of this form are true.

The introduction says that the execution of a declaration consists
of "three phases: _parsing_, _elaboration_, and _evaluation_....
Elaboration, the static phase, determines whether it is well-typed
and well-formed in other ways, and records relevant type or form
information in the basis."

I won't continue to quote the definition, but it seems pretty clear
that programs that violate the type constraints are just as illegal
as programs that violate the syntactic constraints enforced by the
parsing phase.

I am also quite certain that if you were to suggest to Bob Harper
that a Standard ML program shouldn't have to satisfy the typing
rules in order to be legal, he would look at you as if you had
just arrived from another galaxy.

Will