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

definitionaltype 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:We call such a specification atypetyvarseq tycon=tydefinitional spec(also sometimes referred to astype 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

structuresharing 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 replication specs serve the same purpose for datatype specs as definitional type specs do for simple type specs, and we use the termdatatypetycon=datatypelongtycondefinitional specificationsto 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`A.t`

(and hence`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`t`

to be the same as`A.t`

, and in addition it implicitly specifies the data constructors`C`

and`D`

associated with`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`X.t`

and`A.t`

are the same type and`A.D`

and`X.D`

are 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

`where type`

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

`S1`

is 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`t`

is`int list`

).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`S1`

is a large signature. SML '97 provides another solution to this problem in the form of the`definition. It modifies an existing signature by adding a definition of one of it's types. In our example, we would use it as follows:`

where typesignature S2 = sig structure A : S1 where type t = int list endHere the`where type`

definition modifies or augments the signature`S1`

, and`S1 where type A.t = int`

is a new form of signature expression. With`where type`

we 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 type`

clauses 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 type`

clause is a symbolic path`A.t`

(alongtyconin the Definition's terminology), and the effect is to augment the specification of`t`

in`S1`

.

Datatypes defined by where clauses.The type defined by a`where type`

clause 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 type`

is equivalent to an embedded datatype replication spec, so signature`U`

could 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`t`

and 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 type`

definition cannot mention types that are specified in the signature it modifies. So the following example is illegal (assuming no type`t`

is 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.t`

on the right hand side of the`where type`

clause refers to the type specified inside the signature`S`

, then we will have created a kind of undesirable circular dependency, where type`s`

depends on the substructure`A`

because of the where definition, while`A`

depends on`s`

because`s`

is mentioned in`A`

's signature.We would like to be able to replace any signature definition using the

`where type`

construct by an equivalent definition that replaces the where definitions with type abbreviation specs and datatype replication specs. It is clear that the signature`U`

in the last example could not be expressed without the`where type`

clause 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 type`

construct 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 type`

definitions. 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 type`

in terms of it.However, for technical reasons the Definition does things backward, treating

`where type`

as a primary notion and defining type abbreviation specs (but not datatype replication specs) in terms of`where type`

and`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 (`s`

,`u`

, and`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 type`

definition 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 = intwhichisacceptible 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

[1] signature S = [2] sig [3] type s [4] structure A : sig [5] type t [6] type u [7] sharing type t = u [8] sharing type t = s [9] end [10] endthe sharing constraint in line [7] applies to the preceding specs in lines [5] and [6], and is legal because the type names`t`

and`u`

mentioned in the sharing constraint are bound in those specs. The sharing constraint at line [8], on the other hand, is not legal, because its "scope" consists of lines [5-7], while it mentions the type`s`

bound lin line [3]. 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

`where`

definitions. The declaration of`S`

above can be rewritten as the following legal SML '97 declaration.[1] signature S = [2] sig [3] type s [4] structure A : sig [5] type t = s [6] type u = t [7] end [8] endIt can also be legally rewritten (according to the Definition) as[1] signature S = [2] sig [3] type s [4] structure A : sig [5] type t = s [6] type u [7] sharing type t = u [8] end [9] endbut this version raises a delicate and controversial point. Notice that the type`t`

is defined in its specification at line [5], and it is further constrained by the sharing constraint at line [7].## 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 calldefinitional sharing. Here is a typical example of coherence sharing:signature S = sig type t type s sharing type t = s endIn this case, neither`t`

nor`s`

is 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`t`

is effectively defined to be equal to`int`

by 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`t`

and`v`

are defined directly in terms of the formal types`s`

and`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

nodefinition 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 illegal

signature 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.## 1.3.5.1 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 example

signature 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.## 1.3.5.2 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 example

signature S = sig type s type t = s type u sharing type t = u endBy our definition above,`t`

is defined, and therefore not sharable, and this signature declaration is rejected. Technically, however, the semantic representation of`t`

in the signature is the type function`\().(()`

(a nullary type function, wherens)`is the semantic type "name" for`

ns`s`

), and this type function is eta-equivalent to`, a simple flexible type name. Therefore, if this eta-reduction is assumed,`

ns`t`

meets 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`t`

is 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`int`

is 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 type`

clauses. For instance, the following three declarations of signature`S`

are 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 type`

clauses, 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`S`

so 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.The

`where type`

construct 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 todefinea 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 type`

clause 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

`A`

and`B`

have the signature`ORD`

defined belowsignature ORD = sig type t val comp : t * t -> t endthe sharing specificationsharing A = Bguarantees not only that the types`A.t`

and`B.t`

are the same but that the comparison operations`A.comp`

and`B.comp`

were the same, i.e. that`A`

and`B`

implement 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 instance

sharing 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`B`

has no type components, the sharing equations`A = B`

and`B = C`

are 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.## 1.3.8.

`include`

sigexpThe syntax of the

`include`

spec 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`include`

and`where type as a derived form. Thus`

`type t =`

ty`is supposed to be an abbreviation for`

include sig type t end where type t =This 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 definingty`where type`

via a syntactic translation into definitional specs, and that is the issue of free variable capture. For instance, in the following signature definition the type`u`

appearing in the`where type`

clause is different from the type`u`

specified in the body of`S`

.signature S = sig type u type t end where type t = u * uIf we were to eliminate the`where type`

clause in the following definition by textually moving the definition inward to the point where`t`

is specified, we would have signature S = sig type u type t = u * u end which is clearly incorrect, because the free occurences of`u`

in the definition of`t`

have been captured by the local binding of`u`

. So though this approach to eliminating`where type`

can 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 form

abstraction 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`

,`Opaque.t`

is still equivalent to`int`

, because of the definition in the signature, but`Opaque.s`

is a new abstract type that is different from`int`

.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.

openandlocalspecification forms deletedThe Definition of SML '90 had two special forms of specification that could be used in signatures:

`local...in..end`

and`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 A`

specification allows`A.t`

to be abbreviated to`t`

, while the`local`

form prevents the components of`A`

from being added to`S`

as specifications. So this definition of signature`S`

is 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 simply

signature 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)

```
```

Dave MacQueen
Last modified: Thu Jun 28 17:23:44 EDT 2001