Type definitions in signaturesSML '97 Definition, Section G.1. Also known as "type abbreviations in signatures".
It has long been known 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 special cases, one could use a 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 formtype tyvarseq tycon = tyfor instancetype t = int listAllowing type definition specs of this sort 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, because one has more control over which exported types are abstract (opaque) and which are concrete (transparent).
Type definition specs are also necessary now because of new restrictions on sharing specifications discussed below. The type paths in a type sharing specification must be local to the previous specifications in the signature, which means that the declaration of signature
Sabove is no longer legal. Instead, we must employ a type definition spec and writesignature S = sig type t = int end(or the equivalent version using
where type(see next topic). This form is clearer and more concise in any case.
A type sharing spec as in the first declaration of
Sis called a definitional sharing constraint, since it identifies a formal, unknown type
twith the known type
int, thereby effectively defining t. The SML '97 design eliminates definitional sharing constraints, with the intension that they should be replaced by more direct type definition specs.
Type definition specs were introduced in SML/NJ starting with version 0.93, and they have also been supported in Caml Special Light. The main improvement made in the SML '97 design is to reduce confusing interactions between type definition specs and type sharing specs.
The reasons why type definition specs are needed also apply when dealing with structures. In SML '90, we have used definitional structure sharing, and these forms of sharing specs are no longer allowed. Clearly a structure analogue of type definition specs is the answer, but unfortunately the SML '97 definition does not provide them. So SML/NJ fills the gap, as described below in the section on structure definition specs.
Datatype replication specs
Modifying signatures withSometimes it's too "late" to use a type definition spec. I am refering to cases where the type in question is specified in a previously definied signature. 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
int list). 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. 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 A.t = int 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 A.t = int list end
Restriction of sharing to local pathsIn 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 .
Restriction of sharing to "formal" types
Replacement of "definitional" sharing by definitional specsThere 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 now 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.
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.
Structure sharing as derived form for type sharing
- "weak" structure sharing
- structures no longer have a unique static identity
- sharing not "transitive" (or transitively inherited)
opaque signature matching
- where can it be used
- replaces "abstraction" declaration of SML/NJ
equality type specs, inferred equality properties
open and local specification forms deleted
no repeated specifications of an identifier
behavior of include (Defn vs SML/NJ)