Fixed scoping for manifest type specifications

From Successor ML

Jump to: navigation, search



We propose modifying the definition of the manifest type specification derived form, in order to make its scoping rules consistent witht the rest of the language.


For technical reasons, manifest type specifications are defined as a derived form. However, the definition of this form results in scoping rules that are at odds with the rest of the language. More precisely, when several type specifications are connected with and, as in

   type t = int
   and  u = t

then each specified tycon is visible in the following descriptions, making the above snippet legal. This is different from all other uses of and in the language, which elsewhere introduces either parallel or recursive binding. In particular, the identical type declaration

   type t = int
   and  u = t

is not valid, unless t is already bound in the context. In fact, some implementations used to deviate from the Definition in this respect, making the former example behave analogously (at least Moscow ML and Poly/ML still do).




Defined by the following modification to the Definition:

  • In Appendix A, Figure 19, replace the first two rules with the following one:
   | type tyvarseq_1 tycon_1 = ty_1 | include                                   |
   |  and ...                       |  sig type tyvarseq_1 tycon_1              |
   |  ...                           |       and ...                             |
   |  and tyvarseq_n tycon_n = ty_n |       ...                                 |
   |                                |       and tyvarseq_n tycon_n              |
   |                                |  end where type tyvarseq_1 tycon_1 = ty_1 |
   |                                |      where type ...                       |
   |                                |      ...                                  |
   |                                |      where type tyvarseq_n tycon_n = ty_n |

Static Semantics

Follows from the definition as a derived form. Scoping now behaves consistently with other binding forms.

Dynamic Semantics

Follows from the definition as a derived form.




This change may break programs relying on the current scoping rules. However, since these rules are rather counter-intuitive, and they make using and in type specifications pointless anyway, we expect those programs to be rare. Moreover, it is trivial to adapt them to the change.


Only few SML implementations actually implement manifest type specifications as a derived form. We hence expect the change to be a simplification for the majority of implementations, as it removes an annoying singularity in the language rules.

Personal tools