Simplifying val rec syntax

From Successor ML

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

Introduction

We propose a simplification of the val rec syntax that rules out non-sensical phrases, and removes an inconsistency between static and dynamic semantics.

Motivation and Example

The current syntax for recursive value declarations allows many phrases that are either useless or confusing. For example,

 val rec rec rec f = fn x => x
 val f = fn x => x and rec g = fn x => f x

Note that in the latter declaration, the right-hand side of g does not refer to the f of the same declaration.

The syntax can be simplified by only allowing rec directly after the val keyword.

Furthermore, the Definition currently allows recursive value declarations to overwrite identifier status. This is inconsistent with the rules of the dynamic semantics, and hence arguably a bug. It also is counter-intuitive and a nuisance to implement (no implementation does it "correctly"). Our proposal removes this possibility.

Assumptions

None.

Syntax

Defined by the following modifications to the Definition:

• In Section 2.8, Figure 4, and in Appendix B, Figure 21, replace the production for value declarations with:

   dec ::= val <rec> tyvarseq valbind    value declaration

and remove the second production for valbind.

• In Section 2.9, 4th bullet, replace the start of the sentence with:

For each value binding pat = exp in a value declaration with rec,

• In Appendix A, third paragraph, replace "val tyvarseq rec valbind" with "val rec tyvarseq valbind".

• In Appendix A, Figure 17, replace the transformed form of function declarations with:

   val rec tyvarseq fvalbind

Note that this change reverses the order of the rec keyword and an eventual type variable sequence in a value declaration, making it more natural.

Static Semantics

• In Section 4.10, Declarations, change rule 15 to:

   U = tyvars(tyvarseq)    <tynames VE \subseteq T of C>
   <forall vid in Dom VE, vid notin Dom C or is of C(vid) = v>
   C + U <+ VE> |- valbind => VE    VE' = Clos_C,valbind VE    U \cap tyvars VE' = 0
   ---------------------------------------------------------------------------------   (15)
                   C |- val <rec> tyvarseq valbind => VE' in Env

• In Section 4.10, Value Bindings, remove rule 26. Add the respective comment to the comment on rule 15, but replace the last two sentences with the following:

   The side condition on the value identifiers in C ensures that C + VE does not
   overwrite identifier status in the recursive case. For example, the program
   "datatype t = f; val rec f = fn x => x;" is not legal.

Dynamic Semantics

• In Section 6.6, second paragraph, replace "recursive value bindings of the form rec valbind" with "recursive value declarations of the form val rec valbind".

• In Section 6.7, Declarations, change rule 114 to:

                 E |- valbind => VE
 -------------------------------------------------    (114)
 E |- val <rec> tyvarseq valbind => <Rec>VE in Env

• In Section 6.7, Value Bindings, remove rule 126.

Interactions

None.

Compatibility

The change intentionally rules out some previously legal programs and reverses the order in which the rec keyword and the optional type variable sequence may appear in a value declaration. However, at least one major SML implementation - namely SML/NJ - always implemented the revised syntax, so the change is unlikely to affect existing programs.

No current implementation follows the Definition with respect to overwriting of identifier status (although they deviate in different ways). Consequently, this part of the change is even less likely to affect existing programs.

Implementation

Minor simplification of the parser.