Fixed scoping for manifest type specifications
From Successor ML
Contents |
Introduction
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.
Motivation
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).
Assumptions
None.
Syntax
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.
Interactions
None.
Compatibility
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.
Implementation
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.
