Withtype in signatures
From Successor ML
Contents |
Introduction
We propose adding withtype specifications for datatypes, analogous to the one for datatype declarations. This basically blesses an extension that has long been available in most SML implementations.
Motivation
The absence of this derived form clearly is an oversight in the definition. The derived form is as useful in signatures as it is in declarations.
Assumptions
None.
Syntax
Defined by the following modifications to the Definition:
- In Appendix A, Figure 19, add the following to the Specifications box:
+-----------------------------------+----------------------------------+ | datatype datdesc withtype typbind | datatype datdesc' ; type typbind | +-----------------------------------+----------------------------------+
- and extend the note as follows
(see the note in text concerning datdesc', typdesc, and longtycon_1,...,longtycon'_m)
- In Appendix A, add the following paragraph:
In the form involving withtype, the identifiers bound by datdesc and by typbind must be distinct. The transformed description datdesc' is obtained from datdesc by expanding out all the definitions made by typbind, analogous to datbind above. The phrase "type typbind" can be reinterpreted as a type specification that is subject to further transformation.
Static Semantics
Follows from the definition as a derived form.
Dynamic Semantics
Follows from the definition as a derived form.
Interactions
None.
Compatibility
This is a conservative change, which is already supported by most implementations.
Implementation
Straightforward.
