SML '97 Modules

Type definitions in signatures

SML '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 in

  signature S =
  sig
    type t sharing type t = int
  end

but 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 = ty

for instance

  type t = int list

Allowing 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 S above is no longer legal. Instead, we must employ a type definition spec and write

  signature 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 S is called a definitional sharing constraint, since it identifies a formal, unknown type t with 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 with where type

Sometimes 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 S1 is a large signature with a simple specification of type t:

  signature S1 =
  sig
    type t
    ... (* twenty other specifications *)
  end

Later we want to use S1, but we want to specify in addition that t is int (or 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
  end

But this sharing is no loner legal, because int is 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 S1 is a large signature. SML '97 provides another solution to this problem in the form of the where type 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:

  signature S2 =
  sig
    structure A : S1 where type A.t = int
  end

Here 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, like

  signature S2 =
  sig
    structure A : S1 where type A.t = int list
  end

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] end

the 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] end

It 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] end

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

Restriction of sharing to "formal" types

Replacement of "definitional" sharing by definitional specs

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
  end

This last example might suggest that one could always replace type sharing specs with type definition specs or where type clauses, 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
  end

There is no way to rearrange the definition of the signature S so that the sharing spec can be replaced by a definition.

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

This 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
  end

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

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)

include sigexp

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)