Fixing various minor issues with the formal syntax

From Successor ML

Contents 1 Introduction 2 Motivation 3 Assumptions 4 Syntax 5 Static Semantics 6 Dynamic Semantics 7 Interactions 8 Compatibility 9 Implementation

Introduction

We propose clarifications to resolve existing ambiguities in the syntax.

Motivation

The syntax specification in the Definition is somewhat sloppy, leaving a number of ambiguities and minor issues. We provide the boring details to resolve the relevant ones. Mostly, these just blesses existing practice in SML implementations. We motivate the individual changes below (for details about the issues, see Defects in the Revised Definition of Standard ML).

Assumptions

None.

Syntax

Defined by the following modifications to the Definition:

• In Section 2.2, the paragraph defining formatting characters, add carriage return and vertical tab to the list of non-printable characters included.

(Needed for portability to major operating systems, where at least CR is mandatory in text files.)

• In Section 2.6, 1st paragraph, extend the sentence starting with "The only required use of op..." by inserting the following before the semicolon:

   [...] in an expression or pattern;

(Clarifies where "op" is really needed: only in expressions and patterns.)

• 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 actually producing a soundness bug - cf. Fixing various minor issues with the formal semantics.)

• In Section 3.4, Figure 6, add the following:

   Restriction: A declaration dec appearing in a structure declaration may not be
   a sequential or local declaration.

(Disambiguates parsing of sequential and local declarations in structures or on top-level: they must be parsed as structure declarations.)

• In Figure 7, add the following:

   Restriction: In a sequential specification, spec_2 may not contain a sharing specification.

(Disambiguates scoping of sharing specification: they must take the largest possible scope.)

• In Figure 8, extend the restriction with the following sentence:

   Furthermore, the strdec may not be a sequential declaration strdec_1<;>strdec_2.

(Disambiguates parsing of sequential structure declarations on top-level: they must be parsed as top-level declarations.)

• In Section 8, Programs, extend the comment on rule 187:

   [...], except for possible fixity directives contained in the topdec.

(Clarifies that the fixity environment has changed even after failed elaboration.)

• In Appendix A, Figure 17, add respective indices 1..m to the ty annotations appearing on both sides of the definition of the function value binding form.

(Changes syntax to what is actually intended and can reasonably be parsed.)

• In Appendix B, extend the first sentence as follows:

   [...], together with the derived form of Figure 18 in Appendix A.

(Corrects incorrect/inconsistent statement.)

• In Appendix B, add the following to the third paragraph:

   The same applies to patterns, where the extra classes AppPat and InfPat are introduced,
   yielding
   
      AtPat < AppPat < InfPat < Pat

(Together with the change to Figure 22, disambiguates precedence for patterns, analogous to expressions.)

• In Appendix B, third bullet, replace the paragraph starting with "Note particularly that..." with:

   Note that the use of precedence does not prevent a phrase, which is an instance of
   a form with higher precedence, having a constitutent which is an instance of a form
   with lower precendence, as long as they can be resolved unambiguously. Thus for example
   
      if ... then while ... do ... else while ... do ...
   
   is quite admissible and parses as
   
      if ... then (while ... do ...) else (while ... do ...)
   
   However, precedence rules out phrases which cannot be disambiguated without
   violating precedence, such as
   
      a andalso if b then c else d orelse e

(Corrects inconsistent and impractical requirements for parsing.)

• In Figure 21, in the production for fvalbind, add indices 1..m to the optional ty annotations. Furthermore, add the following:

   Restriction: The expressions exp_1,...,exp_m-1 in a fvalbind may not terminate in a match.

(Blesses the way parsing of "fun" has been implemented by everybody.)

• In Figure 22, replace the productions for pat with the following:

   apppat ::= atpat               
              <op>longvid atpat       constructed value
   
   infpat ::= apppat              
              infpat1 vid infpat2     constructed value (infix)
   
   pat    ::= infpat
              pat : ty                typed
              <op>vid <: ty> as pat   layered

(Disambiguates precedence in patterns, see above.)

Static Semantics

Unaffected.

Dynamic Semantics

Unaffected.

Interactions

None.

Compatibility

These are merely fixes, they do not change the language beyond resolving ambiguities. The only exception is the restriction on nesting matches in a fvalbind, which is what all SML systems implement anyway.

Implementation

Implementations realise these or similar fixes already.