Fixing various minor issues with the formal semantics
From Successor ML
Contents |
Introduction
For the time being, we propose a number of straightforward fixes to obvious typos and ommissions in the formal bits of the Definition.
Motivation
The Definition contains a number of bugs in inference rules and other parts of the formal semantics. Some of them undermine soundness, some are just plain typos. The changes we propose merely plug these holes and bless existing practice, they should not have any further effect on the defined language. We motivate the individual changes belows (for details about the issues, see Defects in the Revised Definition of Standard ML).
Note: Along with changes in other proposals, the only known (non-pedantic) issue remaining is the lack of a requirement for type sharing to be consistent with respect to the involved constructor environments, which makes exhaustiveness and irredundancy of patterns an ill-defined concept. No straightforward fix seems to exist within the Definition's formal framework, short of introducing a global consistency requirement similar to SML'90.
Assumptions
None.
Syntax
Defined by the following modifications to the Definition:
- In Section 2.9, add the following bullet:
Any tyvar occurring on the right side of a typbind or datbind of the form "tyvarseq tycon = ..." must occur in tyvarseq.
- (Fixes an oversight producing a soundness bug.)
Static Semantics
Defined by the following modifications to the Definition:
- In Section 4.10, Datatype Bindings, add a closing parenthesis to the conclusion of Rule 28.
- (Fixes typo.)
- In Section 4.11, first bullet, in the first sentence change "the program context" to
[...] the program context consisting of the smallest enclosing declaration
- (Disambiguates scoping for resolution of flexible record types. The fix corresponds to most implementations and is such that type inference is independent of order for subexpressions.)
- In Section 5.7, Signature Expressions, add the following side condition to rule 64:
t in TyName^(k)
- (Missing side condition that may render side condition on phi(E) meaningless.)
- In Section 5.7, Specifications, add the following side condition to rule 78:
t_i in TyName^(k), i = 1..n
- (Missing side condition that may render phi(E) ill-defined.)
Dynamic Semantics
Defined by the following modifications to the Definition:
- In Section 7.3, Functor Bindings, in rule 182, replace both occurences of IB with B.
- (Fixes typos.)
- In Seciton 7.3, Top-level Declarations, in the conclusion of rules 184-186, replace B'<'> with
B' <+ B>
- (Fixes propagation of environments, probably typos.)
- In Appendix D, add the following paragraph:
Furthermore, the initial state is defined by
s0 = ({}, {Match, Bind})
- (Fixes minor minor problem with exception semantics (could redefine built-in exceptions).)
- In Chapter E, last paragraph of the introduction, change the last sentence to:
For this purpose, the surrounding text is the smallest enclosing declaration.
- (Disambiguates scope of overloading resolution. Corresponds to most implementations.)
- In Section E.1, before the sentence starting with "Special constants...", insert the following sentence:
The class Real may not contain type names that admit equality.
- (Required to make type inference for overloading with defaults compositional.)
- In Section E.2, Figure 27, change the types of <, >, <=, >= to
numtxt * numtxt -> bool
- (Fixes wrong types, obviously typos.)
Interactions
None. But some further fixes are proposed in other proposals.
Compatibility
These are merely fixes, they do not change the language beyond plugging holes.
Implementation
Implementations realise these or similar fixes already.
