Significant changes were made in the SML module system in SML '97. The motivations for this change were to simplify the semantics of the module system, mainly by weakening the notion of structure sharing, and to improve the expressiveness of signatures by adding definitional type specifications. The addition of definitional type specifications is accompanied with new restrictions on type sharing specs. In many cases where type sharing specs would have been used in SML '90, in SML '97 it is necessary, or perhaps just better style, to use definitional type specifications. In SML '97, structures do not have unique, checkable static identities, and structure sharing is viewed as an abbreviation for implied type sharing. The lack of a structure level equivalent of definitional type specs was soon found to be awkward, and SML/NJ has implemented this useful feature ( Section 1.6.2).
1.3.1. Type abbreviations in signatures
SML '97 Definition, Section G.1.
It has long been realized that the original signature language of SML '90 was not expressive enough for some purposes. In particular, it was not possible in general to indicate both the existence and the definition of a type component in a specification. In special cases, one could use a definitional type sharing specification, as insignature S = sig type t sharing type t = int endbut this would not work if
t's definition was a type expression like
int list. So in SML '97 the definition of type specification is extended to allow specifications of the form:type tyvarseq tycon = tyWe call such a specification a definitional spec (also sometimes referred to as type abbreviation spec). Using this sort of specification, we can rewrite the above signature more neatly as follows:signature S = sig type t = int list endAllowing type definition specs in signatures makes it possible to write a signature that more fully captures or constrains the type information in a structure. It also makes it more practical to use the opaque form of signature matching described below (Section 1.3.9), because one has more control over which exported types are abstract (opaque) and which are concrete (transparent).
Type definition specs were introduced in SML/NJ starting with version 0.93, and they have also been supported in Caml Special Light and Ocaml(?). The main improvement made in SML '97 is to reduce confusing interactions between type definition specs and type sharing specs by placing new restrictions on type sharing specs. We restrict the types that can appear in a sharing spec to those specified within the current signature (Section 1.3.4), and we ban definitional sharing specs (Section 1.3.5). We also increase the usefulness of definitional specs by using the "
where type" syntax to attach definitions to previously defined signatures (Section 1.3.3). The resulting design gives us more expressive power than SML '90.
The motivations for introducing type definition specs also apply to structure specs. In SML '90 programs we often use definitional structure sharing specs, bug this form of sharing spec is not allowed is SML '97. Clearly a structure analogue of type definition specs would be a convenient replacement, but unfortunately SML '97 does not provide them. So SML/NJ fills this gap, as described below in the section on structure definition specs (Section 1.6.2).
1.3.2. Datatype replication specs
Datatype replication declarations were described in Section 1.1.5. An analogous datatype replication specification form has been provided for signatures, and it has the same syntax as the declarations:datatype tycon = datatype longtyconDatatype replication specs serve the same purpose for datatype specs as definitional type specs do for simple type specs, and we use the term definitional specifications to cover these two forms. Here is an examplestructure A = struct datatype 'a t = C | D of 'a * 'a t end signature S = sig datatype t = datatype A.t endNote that even though
t) is a unary type constructor, we do not include formal type variable parameters in the datatype replication spec. The effect of this spec is to define type component
tto be the same as
A.t, and in addition it implicitly specifies the data constructors
A.t. Thus in a functor declaration such asfunctor F(X: S) : sig val f : 'a X.t -> 'a A.t end = struct fun f(X.C) = X.C | f(X.D(x,y)) = A.D(x,X.D(x,y)) endit is guaranteed that
A.tare the same type and
X.Dare the same data constructor.
As explained below in Section 1.3.6, one of the main uses of datatype replication specs is to substitute for definitional sharing constraints, which are no longer allowed.
1.3.3. Modifying signatures with
Sometimes it's "too late" to use a definitional type spec when we need one. By this I am refering to cases where the type we would like to define is specified in a signature that has already been declared, perhaps in a library. For example, suppose
S1is a large signature with a simple specification of type
t:signature S1 = sig type t ... (* twenty other specifications *) endLater we want to use
S1, but we want to specify in addition that
One could insert
S1's defining signature expression in place of
S1, modified with the appropriate definition of
t, but this is obviously undesirable when
S1is a large signature. SML '97 provides another solution to this problem in the form of the
where typedefinition. It modifies an existing signature by adding a definition of one of it's types. In our example, we would use it as follows:signature S2 = sig structure A : S1 where type t = int list endHere the
where typedefinition modifies or augments the signature
S1 where type A.t = intis a new form of signature expression. With
where typewe are able to express things that we couldn't express before with definitional sharing constraints, likesignature S2 = sig structure A : S1 where type t = int list endWe can even use
where typeclauses in cases where the type to be defined is buried inside a substructure, as in the following examplesignature U = sig structure A : S1 ... end signature S2 = sig structure B : U where type A.t = int list endNote that here the left hand side of the
where typeclause is a symbolic path
A.t(a longtycon in the Definition's terminology), and the effect is to augment the specification of
Datatypes defined by where clauses. The type defined by a
where typeclause can be one that was specified as a datatype.structure A = struct datatype 'a t = C | D of 'a * 'a t end signature S = sig datatype 'a t = C | D of 'a * 'a t end signature U = S where type 'a t = 'a A.tIn this example, the
where typeis equivalent to an embedded datatype replication spec, so signature
Ucould equivalently have been defined assignature U = sig datatype t = datatype A.t endTechnically, the Definition is rather lenient about consistency between the affected primary specification and its definition in a where clause. For instance, the following signature declaration is legal,signature S = sig datatype t = T end where type t = intthough such a signature cannot be realized because the base specification of
tand its definition in the where clause are not consistent. A compiler might check for such obvious inconsistencies (but SML/NJ does not).
Context of right hand side of where definition. The type expression on the right hand side of a
where typedefinition cannot mention types that are specified in the signature it modifies. So the following example is illegal (assuming no type
tis defined in the context of this declaration).signature S = sig type s type t end where type s = tThe reason for this restriction is that we want to avoid examples like the followingsignature S = sig type s structure A : sig type t val x : s * t end end signature U = S where type s = A.t * A.tIf the
A.ton the right hand side of the
where typeclause refers to the type specified inside the signature
S, then we will have created a kind of undesirable circular dependency, where type
sdepends on the substructure
Abecause of the where definition, while
sis mentioned in
We would like to be able to replace any signature definition using the
where typeconstruct by an equivalent definition that replaces the where definitions with type abbreviation specs and datatype replication specs. It is clear that the signature
Uin the last example could not be expressed without the
where typeclause under this interpretation of the context of the clause's right hand side. This is why we exclude the body of the modified signature from the context of the right hand side and thereby make this example illegal.
SML/NJ Discrepancy: The natural way of thinking of the
where typeconstruct is that is is a way of introducing type abbreviation specs (or datatype replication specs) into a previously defined signature, thereby producing an augmented version of that signature. It should in principle be possible to equivalently define that augmented signature with the definitions placed directly at the points of specification of the affected types. This is in fact how SML/NJ implements
where typedefinitions. Thussignature S = sig type t end where type t = intis tranformed by the compiler into the declarationsignature S = sig type t = int endThus treating type abbreviation specs as the primary construct and defining
where typein terms of it.
However, for technical reasons the Definition does things backward, treating
where typeas a primary notion and defining type abbreviation specs (but not datatype replication specs) in terms of
include. Thus in the Definition,signature S = sig type t = int endis translated intosignature S = sig include sig type t end where type t = int endFor the most part, this difference in approaches does not matter. The Definition's version admits more signatures as legal, but we argue that they are not signatures that good programmers would want to write. Here is an example of a legal signature that is not accepted by SML/NJ (due to Marin Elsman, see SML/NJ bug 1330):signature S = sig type s structure U : sig type 'a t type u = (int * real) t end where type 'a t = s end where type U.u = intWe leave it as an exercise for diligent language lawyers to verify that this is acceptible under the definition, but it is pretty clearly not the sort of thing we want to encourage programmers to write. Determining whether this signature makes sense is an exercise in setting up a system of equations in higher-order variables (
t) and then seeking a solution of that system. We would prefer that the sensibility of a signature definition should be more obvious.
One particular reason why this signature declaration is not accepted by SML/NJ is that SML/NJ does not allow a
where typedefinition to apply to a type constructor that already has a definitional specification. A simpler example of a signature that is rejected for this reason is:signature S = sig type s type t = s end where type t = intA more sensible way to write this would besignature S = sig type s type t = s end where type s = intwhich is acceptible to SML/NJ.
1.3.4. Restriction of sharing to local paths
In SML '90, a sharing specification is an independent specification in a signature, but in SML '97, sharing specifications modify the specifications (a sequencial spec) that they follow textually in the signature. The components mentioned in the sharing constraint must all come from the specifications modified by the sharing constraint. Thus, in signature S =  sig  type s  structure A : sig  type t  type u  sharing type t = u  sharing type t = s  end  endthe sharing constraint in line  applies to the preceding specs in lines  and , and is legal because the type names
umentioned in the sharing constraint are bound in those specs. The sharing constraint at line , on the other hand, is not legal, because its "scope" consists of lines [5-7], while it mentions the type
sbound lin line . The same rule applies to structure sharing constraints.
This scope restriction on sharing constraints is the main reason why sharing constraints may need to be converted into definitional specs or
wheredefinitions. The declaration of
Sabove can be rewritten as the following legal SML '97 declaration. signature S =  sig  type s  structure A : sig  type t = s  type u = t  end  endIt can also be legally rewritten (according to the Definition) as signature S =  sig  type s  structure A : sig  type t = s  type u  sharing type t = u  end  endbut this version raises a delicate and controversial point. Notice that the type
tis defined in its specification at line , and it is further constrained by the sharing constraint at line .
1.3.5. Noninterference of sharing and definitional specs
In SML '90, there were two flavors of type sharing, one where both types involved are "formal" or unknown, which we call coherence sharing, and the other sort, where one type is unknown and the other is known, which we call definitional sharing. Here is a typical example of coherence sharing:signature S = sig type t type s sharing type t = s endIn this case, neither
sis determined, but the sharing spec requires that when they are instantiated, they are both instantiated to the same type.
A simple example of definitional sharing is:signature S = sig type t sharing type t = int endwhere type
tis effectively defined to be equal to
intby the sharing constraint.
In SML '97, it is possible to define a type directly, in its original specification, or after the fact, using the "where type" syntax, so definitional sharing seems redundant. Furthermore, the interaction between definitional sharing and direct definition could create puzzles, such as the following:signature S = sig type s type t = s list type 'a u type v = int u sharing type t = v endHere, types
vare defined directly in terms of the formal types
u, and then they are equated by the sharing specification. If we wanted to determine whether this signature is satisfiable, we would have to see whether types s and u exist that satisfy the equations list = int uSolving such second-order equations is a messy problem in general, perhaps unsolvable. To solve this problem, the SML '97 design excludes such examples by outlawing definitional sharing. In other words, the types involved in a sharing specification are required to be formal or "flexible".
Technically, the Definition requires that a type constructor involved in a sharing constraint be (1) not defined as a type function, and (2) not defined in terms of some "rigid" type constructor (i.e. a type constructor previously defined in the context).
We choose to define "sharable" as meaning simply that there is no definition applying to a type constructor. We'll use the term "defined" for the opposite of sharable. A more subtle definition is possible; see note "Sharable Types" below.
Thus the following signature is illegalsignature S = sig type s = int (* s is defined *) type t (* t is sharable *) sharing type t = s (* s is not sharable *) endand has to be reexpressed as (for instance):signature S = sig type s = int type t = s endWith "where type" definitions, things are a little more complicated. An inner type sharing constraint can be affected by an outer definitional constraint, as in the following example:signature S1 = sig type s type t sharing type t = s (* ok, because s and t are sharable here *) end where type t = int; (* this converts both s and t to rigid types *)This is legal, but the following declaration is not:signature S2 = sig structure A : S1 type v sharing type v = A.s (* A.s not flexible *) end;However, S2 can easily be converted to the legal S3 below by replacing the outer sharing constraint by a definition.signature S3 = sig structure A : S1 type v = A.s end;In general, we recommend avoiding sharing constraints that can easily be expressed by definitional specs. So one should always prefertype t = stotype t sharing type t = s.The same applies to structure sharing and structure definition specs (which are an SML/NJ language extension). Violations of this newly enforced constraint can often be eliminated by replacing structure sharing by structure definition specs, e.g. replacingstructure A : SIGA sharing A = B.Cwithstructure A : SIGA = B.C.
184.108.40.206 SML/NJ Exception for Structure Sharing with Same Signature
SML/NJ provides one important exception to the rule about sharing rigid types. This is the case where the type sharing is implied by structure sharing between two structures with the same signature.
Here is an examplesignature S = sig type t = int end signature S1 = sig structure A : S structure B : S sharing A = B endThis is allowed in SML/NJ because A and B have the same signature, even though the sharing constraint is equivalent tosharing type A.t = B.tand A.t and B.t have the rigid spectype t = int.
220.127.116.11 What Types Are Sharable [Mostly for language lawyers]
There is some controversy about what type constructors should be allowed in sharing constraints. We can illustrate this by the following examplesignature S = sig type s type t = s type u sharing type t = u endBy our definition above,
tis defined, and therefore not sharable, and this signature declaration is rejected. Technically, however, the semantic representation of
tin the signature is the type function
\().(()ns)(a nullary type function, where
nsis the semantic type "name" for
s), and this type function is eta-equivalent to
ns, a simple flexible type name. Therefore, if this eta-reduction is assumed,
tmeets the requirements of the definition and can appear in the sharing constraint. On the other hand, considersignature S = sig type s type t = s list type u sharing type t = u endHere the representation of
tis the type function
\().(()ns) list, which does not reduce to a simple type name, so the sharing constraint is clearly illegal. The reasons that we adopt the simpler and more restrictive meaning of sharable are that it is easier to explain and it admits all sensible usages. We claim that it promotes a cleaner and simpler style in signature writing. It is also much simpler more efficient to implement (at least for SML/NJ). Here are some example signatures that are admitted under the more complicated version of the definition (thanks to Martin Elsman of DIKU):signature S1 = sig type t type s = t end where type s = int signature S2 = sig type t type s = t sharing type t = s end signature S3 = sig type s structure U : sig type 'a t type u = (int * real) t end where type 'a t = s end where type U.u = intIt is not clear that examples like these have any importance to anyone other than language lawyers. The last is particularly perverse: reading a signature should not be an exercise in puzzle solving!
1.3.6. Replacement of "definitional" sharing by definitional specs
We used to be able to use a definitional sharing specification, as illustrated by:signature S2 = sig structure A : S1 sharing type A.t = int endBut this sharing is no loner legal, because
intis not a path local to the body of
S2. There are situations where you have a choice of using sharing specifications or type definition specs or
where typeclauses. For instance, the following three declarations of signature
Sare equivalent:signature T = sig type s end signature S = sig type t structure A : T sharing type t = A.s end signature S = sig type t structure A : sig type s = t end (* expanding T *) end signature S = sig type t structure A : T where type s = t endThis last example might suggest that one could always replace type sharing specs with type definition specs or
where typeclauses, but this is not quite the case, as shown by the following example:signature S = sig type s structure A : sig datatype d = D of s datatype t = K end sharing type s = A.t endThere is no way to rearrange the definition of the signature
Sso that the sharing spec can be replaced by a definition. However, this example is rather contrived, and it is not clear that there would be any serious practical impact if we gave up the ability to write such signatures and uniformly used definitional specs in place of sharing.
where typeconstruct can also be used to define types specified as datatypes in the base signature, and this makes it related to the datatype replication specs described below. Here is an example.structure A = struct datatype t = T end signature S = sig datatype t = T end signature S1 = S where type t = A.tThis capability to define a datatype spec is needed in order to replace definitional sharing constraints like in the following example:signature S = sig datatype t = T sharing type t = A.t endThe definition in this case does not require a check that the datatype "signature" of the spec and its definition in the
where typeclause have to agree, but a compiler could perform some level of checking. It might at least check that the type on the right hand side of the definition is also a datatype, and beyond that it might check that the number and names of data constructors agree.
1.3.7. Structure sharing as derived form for type sharing
In SML '97, structure sharing has been weakened from a first-class feature to a derived syntax feature, i.e. a feature that is explained in terms of translation to type sharing syntax. This is a real weakening of the expressiveness of the module system. In SML '90, where each structure had a unique static identity and structure sharing could be checked statically, one could use structure sharing to guarantee not only that types in two structures agreed, but that the values making up the associated interface to those types were also shared. For instance, if two structures
Bhave the signature
ORDdefined belowsignature ORD = sig type t val comp : t * t -> t endthe sharing specificationsharing A = Bguarantees not only that the types
B.tare the same but that the comparison operations
B.compwere the same, i.e. that
Bimplement the same ordering over the same type.
In SML '97, we can still write such sharing specification, but they are viewed as abbreviations for all possible implied type sharing specs. In this case, the above structure sharing spec translates to the following type sharing spec:sharing type A.t = B.tThis does not imply that the comparison operators A.comp and B.comp agree, so it is strictly weaker than the structure sharing spec in SML '90.
One can recover something like the old structure sharing functionality when the structures in question contain a (generative) type that is used to uniquely identify the structure. In effect, the type is used as a unique tag to guarantee identity of the structure as a whole. This works if there is no "cheating", i.e. if no other independently defined structure incorporates this same tagging type.
Another thing to note about the weak version of structure sharing is that it is not transitive. For instancesharing A = B and B = Cdoes not necessarily imply thatsharing A = Cis satisfied. Here is an examplesignature S0 = sig type t end signature S = sig structure A : S0 structure B : sig end structure C : S0 sharing A = B and B = C endSince structure
Bhas no type components, the sharing equations
A = Band
B = Care vacuous, and translate into no type sharing at all. In particular, they do not guarantee that
A.t = C.t, and therefore do not imply the sharing constraint
A = C.
The paths appearing is structure sharing specs must also satisfy the locality restriction described in Section 1.3.4. That is, the structures that are specified to share must all be components (or subcomponents) of the same signature that contains the sharing spec. This will guarantee that the type sharing specs that the structure sharing translates into will satisfy the locality constraint for type sharing.
This locality rule will generally preclude "definitional structure sharing specs", which are used fairly frequently in SML '90. How should we rewrite such definitional structure sharing specs? One approach is to expand the structure sharing into the corresponding set of type sharing specs, and then replace the definitional type sharing specs with the appropriate "where type" definitions. For example, given a structure A defined as follows:structure A = struct datatype t = T endthe SML '90 signaturesignature S = sig structure B : sig type t end sharing B = A endcan be rewritten assignature S = sig structure B : sig type t end where type t = A.t endOf course, if there were a dozen types involved in A rather than just one, this can lead to an unpleasant expansion of the code. For this reason, it would have been desirable to have a structure analogue of definitional specs, so that we could write something like:signature S = sig structure B : sig type t end = A endSuch definitional structure specs are in fact supported in SML/NJ; see Section 1.6.2.
The syntax of the
includespec has been generalized to allow arbitrary signature expressions as well as signature names. The purpose of this extension is to allow definitional type specs to be defined in terms of
where type as a derived form. Thustype t = tyis supposed to be an abbreviation forinclude sig type t end where type t = tyThis seems somewhat convoluted, since the simple type definition spec seems to be a more elementary concept in its own right, but this approach was chosen because of technical convenience in the Definition. There is a technical problem with treating simple definitional specs as the primitive construct and defining
where typevia a syntactic translation into definitional specs, and that is the issue of free variable capture. For instance, in the following signature definition the type
uappearing in the
where typeclause is different from the type
uspecified in the body of
S.signature S = sig type u type t end where type t = u * uIf we were to eliminate the
where typeclause in the following definition by textually moving the definition inward to the point where
tis specified, we would have signature S = sig type u type t = u * u end which is clearly incorrect, because the free occurences of
uin the definition of
thave been captured by the local binding of
u. So though this approach to eliminating
where typecan work at the level of semantic structures, it doesn't work as a textual transformation (i.e. as a derived form).
1.3.9. opaque signature matching
Previous versions of SML/NJ supported a special structure declaration formabstraction S : SIG = struct ... endwhose purpose was to create an "abstract" instance of the signature
SIG. This feature was left out of SML '90 for various reasons, but the need for it was real.
In SML '97, a similar feature has been provided in the form of "opaque" signature matching using the special signature constraint syntax
S :> SIG. For example, the following declaration has the same effect as the old "abstraction" declaration given above.structure S :> SIG = struct ... endThe effect of opaque signature matching is that the formal or flexible types in the signature SIG get fresh, abstract instantiations that are distinct from the corresponding types in the structure expression being constrained. Here is a more detailed example:signature SIG = sig type s type t = int val zero : s val succ : s -> s val f : s -> t end strucutre Transp : SIG = struct type s = int type t = int val zero = 0 fun succ x = x+1 fun f x = x end strucutre Opaque :> SIG = struct type s = int type t = int val zero = 0 fun succ x = x+1 fun f x = x endBecause of the normal transparent signature matching, Transp.s is equivalent to
int, as is Transp.t. But in the case of
Opaque.tis still equivalent to
int, because of the definition in the signature, but
Opaque.sis a new abstract type that is different from
There are two places where it may make sense to use opaque signature matching. First in a normal structure declaration as in the above examples, and second in specifying the result signature of a functor.functor F(X: PSIG) :> SIG = struct ... endWhen a functor is defined with an opaque result signature like this, each time the functor is applied a new abstract instantiation of the result signature is created.
It does not make sense to use the opaque signature matching form for the formal parameter of a functor (i.e. on the input side as opposed to the output side).
1.3.10. equality type specs, inferred equality properties
1.3.11. open and local specification forms deleted
The Definition of SML '90 had two special forms of specification that could be used in signatures:
open. These forms, particularly local specs, were introduced for technical reasons within the definition. These specification forms have both been dropped in SML '97. These features were controversial in SML '90, because when used in full generality their behavior had no clear intuitive justification, despite their having a precise technical meaning and a technical role in the Definition's semantics. The utility of these features was also dubious, except for one special restricted case, where open and local were combinded to allow the abbreviation of type paths in specifications. For example:structure A = struct type t = int end; signature S = sig local open A in val x : t end end;Here the
open Aspecification allows
A.tto be abbreviated to
t, while the
localform prevents the components of
Afrom being added to
Sas specifications. So this definition of signature
Sis equivalent to writingsignature S = sig val x : A.t end;
In SML/NJ, local and open were never fully implemented according to the SML '90 Definition, but they were partially implemented to support just the above path abbreviation idiom. In fact, the open form was implemented so that it could be used for abbreviational effect even without the surrounding local spec. Thus in SML/NJ 0.93 it was possible to write simplysignature S = sig open A val x : t end;with the same effect.
Since these forms have been dropped in SML '97, when converting SML '90 (or SML/NJ 0.93) code it is necessary to find and eliminate uses of local and open in signatures and write out the full type paths for those types which were thereby abbreviated.
Any (non SML/NJ) code that uses local specs in their full generality to achieve some strange effect will have to be rewritten to achieve the desired effect some other way [dbm: I would be interested in seeing examples of this].
1.3.12. no repeated specifications of an identifier
1.3.13. behavior of include (Defn vs SML/NJ)