Signatures and Structures

[ Home ] [ Next ]

Last edit: Wednesday, November 12, 1997 12:19 PM

The Basics

Let us begin with some examples of signatures.  Here is the signature of an ordered type, one that comes equipped with a "less than" and an "equality" relation on it.  We assume that the "less than" relation is transitive and that the "equality" relation is an equivalence relation, though this is not formally expressible in ML.

signature ORDERED = sig
  type t
  val lt : t * t -> bool
  val eq : t * t -> bool
end

This signature describes those structures that provide a type named t and two operations, lt and eq, of type t * t -> bool.   For example, here are two implementations of the ORDERED signature:

structure IntLT : ORDERED = struct
  type t = int
  val lt = (op <)
  val eq = (op =)
end

structure IntDiv : ORDERED = struct
  type t = int
  fun lt (m, n) = (n mod m = 0)
  fun eq (m, n) = (op =)
end

Without going into detail just yet, it should be clear that these structures are in fact implementations of the ORDERED signature.  In general we indicate that a declared structure implements a signature by writing the target signature after the structure name, separatd by a colon.  This is called transparent signature ascription, which will later be contrasted with opaque signature ascription.  The purpose of transparent ascription is to assert --- and have the compiler check --- that a structure implements a specified signature.

Once a structure has been declared we may access its components using paths (or long identifiers or qualified names).  For example, IntLT.lt designates the lt operation of the structure IntLT and IntDiv.lt designates the lt operation of the structure IntDiv.  The type of IntLT.lt is

IntLT.t * IntLT.t -> bool,

and the type of IntDiv.lt is

IntDiv.t * IntDiv.t -> bool.

Notice that the type of these operations has been "externalized" using long identifiers corresponding to those used to access the operations.  Althought IntLT.t and IntDiv.lt are distinct long identifiers, they both are bound to int.  Consequently, we may write IntLt.lt(3,4) and IntDiv.lt(3,4), since the types of IntLT.lt and IntDiv.lt are both int*int->bool, once the type definitions are taken into account.  This is precisely what we mean by the term "transparent ascription" --- the bindings of types in the structure is not hidden by the ascription.  We can think of the compiler as augmenting the signature ORDERED in each case with an equation type t = int that "publicizes" the identity of the type component t.  Had it not done so, the structures IntLT and IntDiv would be useless since there are no values to which we may apply the operations of these modules!  (We will come back to this issue later on when we discuss data abstraction.)

Here are two more signatures, one for a persistent queue, the other for an ephemeral queue.

signature PERS_QUEUE = sig
  type 'a queue
  val empty : 'a queue
  val insert : 'a * 'a queue -> 'a queue
  exception Empty
  val remove : 'a queue -> 'a * 'a queue
end

signature EPH_QUEUE = sig
  type 'a queue
  val new : unit -> 'a queue
  val insert : 'a * 'a queue -> unit
  exception Empty
  val remove : 'a queue -> 'a
end

In both cases the type of queues is parametric in the type of elements of the queue since neither implementation concerns itself with the exact nature of the elements of the queue.

Here are structure declarations that provide implementations of persistent and ephemeral queues.

structure PersQueue : PERS_QUEUE = struct
  type 'a queue = 'a list * 'a list
  val empty = (nil, nil)
  fun insert (x, (bs, fs)) = (x::bs, fs)
  exception Empty
  fun remove (nil, nil) = raise Empty
    | remove (bs, f::fs) = (f, (bs, fs))
    | remove (bs, nil) = remove (nil, rev bs)
end

structure EphQueue : EPH_QUEUE = struct
  type 'a queue = 'a list ref * 'a list ref
  fun new () = (ref nil, ref nil)
  fun insert (x, (bs, fs)) = (bs := x::!bs)
  exception Empty
  fun remove (ref nil, ref nil) = raise Empty
    | remove (ref bs, front as ref (f::fs)) = (front := fs; f)
    | remove (back as ref bs, front as ref nil) =
      (front := rev bs; back := nil; remove (back, front))
end

These modules may be used as follows:

val q = PersQueue.empty
val q' = PersQueue.insert (1, q)
val q'' = PersQueue.insert (2, q)
val (x'', _) = PersQueue.remove q''        (* 2 *)
val (x', _) = PersQueue.remove q'          (* 1 *)

val q = EphQueue.new ()
val q' = EphQueue.new ()
EphQueue.insert (1, q);
EphQueue.insert (9, q');
EphQueue.remove q;                          (* 1 *)
EphQueue.remove q';                         (* 9 *)

We may avoid the excessive use of qualified names by either introducing a shorter, less obtrusive name, or by using the open declaration.  Here's an example of both styles.  Using short names we would write:

structure PQ = PersQueue and EQ = EphQueue
val q = PQ.empty
val q' = EQ.new ()

Using open we would write:

open PersQueue
val q = empty
val q' = insert (1, q)

It is generally advisable to avoid using open since it is not immediately apparent which identifiers are introduced by the declaration -- every component of the open'd structure is included, shadowing any other declarations that may otherwise be in effect.  This can lead to quite subtle bugs that are difficult to find by reading the text of the program.  In the preceding example, not only are the variables q and q' introduced by the declaration, but so are bindings for empty, insert, Empty, and remove!

To limit the effect of a use of open on the surrounding context, we often use open in conjunction with local.  For example, we would write

local
  open PersQueue
in
  val q = empty
  val q' = insert (1, q)
end

This allows us to define q and q' conveniently without explicitly referring to the structure PersQueue, and at the same time avoids introducing bindings other than for q and q' into the environment.

Views

Using transparent ascription we may express the requirement that a module implement a given signature.  For example, by writing structure PersQueue : PERS_QUEUE = ... we are requiring that the implementation of persistent queues implement the signature PERS_QUEUE in an intuitively obvious sense.  If the implementation should fail to provide any of the components of the ascribed signature, or provide them with different types, then the signature ascription fails, and the compiler will warn us of the mismatch.

In the examples above the structures matched the given signature exactly, by providing precisely the components specified with precisely the required types.  In fact signature matching is a bit more liberal -- to satisfy the ascription the structure must provide at least the components required with at least as general types as are required.  Any "extra" components are dropped from the structure during signature matching, and any "extra" generality in the type of a component is constrained to the type of the signature.  To take a simple example, the following is a correct ascription of signature to a module:

structure S : sig type t val f:t->t end = struct
  type t=int
  fun f(x)=x
  fun g(x)=x
end

(Recall that fun f(x)=x abbreviates val f=fn x=>x.)   Afterwards, the component g is unavailable, and the type of f is S.t->S.t = int->int, and not 'a->'a.   This means that S.g is an unbound identifier, and that S.f may not be applied to values other than integers, even though the underlying code is sufficiently polymorphic to do so.

By dropping components and specializing types we obtain a limited view of a structure.  We may, if we like, have many different views of the same structure.   For example,

structure S = struct type t=int fun f(x)=x fun g(x)=x end
structure S1 : sig type t val f:t->t end = S
structure S2 : sig type t val g:t->t end = S

Here we define S without ascribing any signature at all to the binding.   Everything about the implementation of S is fully visible within the scope of the binding.  We then constrain this information by providing two distinct views of the same structure, one that exports f and the other that exports g.

Of what practical use are views?  The most common use is to extract components of a larger structure for use in some specialized context.  For example, suppose that we wish to define a structure that implements a dictionary whose keys are drawn from a structure implementing the keys.  For the purposes of the dictionary module all we care about keys is that they provide operations for comparing keys; everything else is irrelevant to the dictionary module.  Here's a sketch of the scenario we are considering:

signature STRING = sig
  type t
  val eq : t * t -> bool
  val lt : t * t -> bool
  val ^ : t * t -> t
  ...
end
structure String : STRING = ... implementation of string operations ...

structure Key : ORDERED = String

signature DICT = sig
  type dict
  val insert : Key.t * dict -> dict
  ...
end
structure Dict : DICT = ... Key.lt ... Key.eq ... Dict.insert ("abc", d)...

Notice that we choose to view the String structure (which is in fact built into ML) as having signature ORDERED.  This means, in particular, that the ensuing implementation of dictionaries may refer only to Key.lt and Key.eq, since only these components are defined for Key.  However, the fact that Key.t = string is visible to the client of the dictionary, so that it makes sense to write Dict.insert "abc".   The alert reader will have noticed, however, that the same type equation is true within the implementation of Dict, so we are not assured that Dict uses only the operations Key.lt and Key.eq on keys.   The dictionary package really should be generic with respect to the key structure: it should not depend on the specific choice of keys and hence should be usable with many different choices.  We will return to this point shortly.  For now, our main concern is to illustrate the use of transparent ascription to view the String structure as having the signature ORDERED.

Two further remarks about views:

1. Unfortunately it often happens that a pre-defined structure (such as String in the above example) does not quite provide the components of interest.  For example, in the pre-defined String structure of ML the type is called string, not t, the equality operation is written =, not eq, and the less than operation is written <, not lt.  To rectify this kind of "impedance mismatch" between components, we may use a functor that selects the appropriate components from a structure and gives them the appropriate names.
2. A convenient use of views is to eliminate auxiliary functions from a structure.   Rather than use local to confine the definition of an auxiliary function to a specific declaration, we can simply define the auxiliary as a full-fledged component of the structure that is then eliminated by signature matching.  This is an extremely common, and convenient, idiomatic use of signature matching in ML.

Abstraction

Let us return now to the example of persisent queues defined above.   The definition given there is problematic because the implementation type of the abstraction is completely visible to the client.  That is, the type 'a PersQueue.queue is equal to the type 'a list * 'a list.  This means that we may call, for example, remove with any pair of lists whatsoever, not just a pair of lists arising from uses of the operations PersQueue.insert and PersQueue.remove.  In this case there is no serious difficulty since any pair of lists may be thought of as the representation of some queue; there is no significant representation invariant on the implementation type that might be violated by providing an arbitrary pair of lists.  Nevertheless it is bad programming style to publicize this information; after all, the queue might be implemented by some entirely different means and we would like to shield clients of the abstraction from such details.   Not only does this make the client robust across changes to the implementation of queues, but it also allows us to isolate queueing bugs to the operations that implement them.  This is achieved by hiding the implementation type from the client using opaque signature ascription.  This is achieved as follows:

structure PersQueue :> PERS_QUEUE = ... as above ...

Note well the use of ":>", rather than ":", to ascribe a signature to the module!  This minor difference in syntax makes all the difference in semantics, for after the binding all we know about the structure PersQueue is exactly what is written in the signature.  In particular, the type PersQueue.queue is abstract, meaning that it is known to be some type, but precisely which type is hidden from the client.  This means that the application PersQueue.insert (1, ([],[])) is now a type error since the type of ([],[]) is 'a list * 'a list, which is no longer equivalent to 'a PersQueue.queue.   Furthermore, if we have a value of type PersQueue.queue, it must have arisen from some combination of the operations PersQueue.empty, PersQueue.insert, and PersQueue.remove; there is no other way for such a value to arise.

Why might we wish to know that a value of a type must have arisen in a certain way?   The most important reason is to enforce representation invariants.   For example, suppose that we are implementing a dictionary package using a binary search tree.  The implementation might be defined in terms of a library of operations for manipulating generic binary trees called BinTree.  The implementation of the dictionary might look like this:

structure Dict :> DICT =
  struct
    (* Rep Invariant: binary search tree *)
    type t = string BinTree.tree
    fun insert (k, t) = ...
    fun lookup k = ...
  end

Had we used transparent, rather than opaque, ascription of the DICT signature to the Dict structure, the type Dict.t would be known to clients to be string BinTree.tree.  But then one could call Dict.lookup with any value of type string BinTree.tree, not just one that satisfies the representation invariant governing binary search trees (namely, that the strings at the nodes descending from the left child of a node are smaller than those at the node, and those at nodes descending from the right child are larger than those at the node).   By using opaque ascription we are isolating the implementation type to the Dict package, which means that the only possible violations of the representation invariant are those that arise from errors in the Dict package itself; the invariant cannot be disrupted by any other means.  The operations themselves may assume that the representation invariant holds whenever the function is called, and are obliged to ensure that the representation invariant holds whenever a value of the representation type is returned.  Therefore any combination of calls to these operations yielding a value of type Dict.t must satisfy the invariant.

You might be wondering whether we could equally well use run-time checks to enforce representation invariants.  The idea would be to have a "debug flag" that, when set, causes the operations of the dictionary structure to check that the representation invariant holds of their arguments and results.  In this case this is surely possible, but at a great cost.  The time required to check the binary search tree invariant is proportional to the size of the binary search tree itself, a cost that is clearly prohibitive.  But wouldn't we turn off the debug flag before shipping the production copy of the code?  Yes, indeed, but then the benefits of checking are lost for the code we care about most!  (To paraphrase Tony Hoare, it's as if we used our life jackets while learning to sail on a pond, then tossed them away when we set out to sea.)  By using the type system to enforce abstraction, we can confine the possible violations of the representation invariant to the dictionary package itself, and, moreover, we need not turn off the check for production code.

This discussion glosses over a subtle point, however.  Efficiency considerations aside, you might think that we can always replace static localization of representation errors by dynamic checks for them.  But this is false!  One reason is that the representation invariant might not be computable!  As an example, we define an abstract type of total functions on the integers, those that are guaranteed to terminate when called, without performing any I/O or having any other computational effect.  It is a theorem of recursion theory that no run-time check can be defined that ensures that a given integer-valued function is total.  Yet we can define an abstract type of total functions that, while not admitting ever possible total function on the integers as values, provides a useful set of such functions as elements of a structure.  Here's a sketch of such a package:

signature TIF = sig
  type tif
  val apply : tif -> (int -> int)
  val id : tif
  val compose : tif * tif -> tif
  val double : tif
  ...
end

structure Tif :> TIF = struct
  type tif = int->int
  fun apply t n = t n
  fun id x = x
  fun compose (f, g) = f o g
  fun double x = 2 * x
  ...
end

Should the application of such some value of type Tif.tif fail to terminate, we know where to look for the error.  No run-time check can assure us that an arbitrary integer function is in fact total.

Here is yet an even more subtle point about representation invariants governing a data structure.  One cannot, in general, tell from the representation type whether a given value is "really" a value of the abstract type.  Here's an example.  Under many operating systems processes are "named" by integer-value process identifiers.  Using the process id we may send messages to the process, cause it to terminate, or perform any number of other operations on it.  The thing to notice here is that any integer at all is a possible process identifier; we cannot tell by looking at the integer whether it is indeed a process id.  That is, no run-time check on the value will reveal whether a given integer is a "real" or   "bogus" process id.  The only way to know is to consider the "history" of how that integer came into being, and what operations were performed on it.  Using the abstraction mechanisms just described, we can enforce the requirement that a value of type pid, whose underlying representation is int, is indeed a process identifier.  You are invited to imagine how this might be achieved in ML.

Abstraction and views are, in a sense, fundamentally opposite notions.  For a view to make sense, it is essential that the underlying types not be obscured by the imposition of a view.  Let us consider again the example above in which we viewed the String structure as an implementation of the ORDERED signature.  Suppose we had used opaque ascription, rather than transparent ascription, writing

structure Key :> ORDERED = String

The structure Key is now essentially useless because we can never create a value of type Key.t!  Using opaque ascription we limit ourselves to precisely the information specified in the signature (in this case, ORDERED).   This means that the only operations available to us are the comparisons, which can never be applied to any value.  Transparent ascription ensures that the type Key.t remains visible as String.t so that all string operations are available on it.  The same effect may be achieved using opaque ascription, provided that we publicize the underlying type in the signature.  This is achieved by writing

signature STRING_ORDERED = sig
  type t = String.t
  val lt : t*t->bool
  val eq : t*t->bool
end

structure Key :> STRING_ORDERED = String

Notice the use of a type definition in the signature STRING_ORDERED to achieve essentially the same effect as the transparent ascription.  However, to do so we had to define a specialized version of the ORDERED signature in which the type t is defined to be String.t.  We can avoid rewriting the signature using the where type operation on signatures.  Thus we may write instead

signature STRING_ORDERED = ORDERED where type t=String.t
structure Key :> STRING_ORDERED = String

or just

structure Key :> ORDERED where type t=String.t = String

Transparent ascription may thus be viewed as a stylized use of opaque ascription, in which the compiler implicitly propagates type information into the signature (using where type) to ensure that the identities of the type components are not obscured by the ascription.

Signature Matching

We finish this chapter with a more precise description of signature matching.   When may be correctly ascribe a signature to a module?  First, we compute the principal signature for the module.  This is the most precise (most informative) signature that can be given to that module.  Then, we determine whether the ascribed signature is a sub-signature of the principal signature, meaning that the ascribed signature is more precise than the ascribed signature.  Third, if the ascription is transparent, we carry on using the view of the principal signature determined by the ascription; otherwise, if the ascription is opaque, we carry on using the ascribed signature itself.

The principal signature for a structure is determined as follows:

1. Every type definition in the structure determines the identical type specification in the signature.
2. Every datatype declaration in the structure determines the identical datatype specification in the signature.
3. Every value declaration in the structure determines a value specfication in the signature that specifies the principal type of the binding as the type of that component in the signature.
4. Every exception declaration in the structure determines an identical exception specification in the signature.

Here are the rules in tabular form:

Structure Component	Inferred Principal Signature
type t = ty	type t = ty
datatype t = ... C of ty ...	datatype t = ... C of ty ...
exception x of ty	exception x of ty
val x = exp	val x : ty

In the last case the type ty is the principal type scheme of exp (relative to the preceding declarations).  The complete rules for inferring the principal signature of a structure are a bit more complex.  For example, type and datatype constructors are handled similarly to the simple type declarations mentioned here, and we must be careful about the treatment of "hidden" type identifiers (arising, for example, from a re-declaration of a datatype in a module).  These are rough-and-ready rules for inferring the principal signature of a structure; the complete rules are consistent with these, but are a bit more complex to state.

The second step of determining whether a structure satisfies an ascribed signature is to extract the "view" of the principal signature determined by the ascribed signature.  This consists of dropping all components not named in the ascribed signature, and specializing the types of the value components in the principal signature to those in the ascribed signature.  For example, if the principal signature specifies val f : 'a -> 'a, and the ascribed signature specifies val f : int -> int, the view contains the latter declaration.  Formation of the view fails if a specified component in the ascribed signature is missing in the principal signature, or if the specified type is not an instance of the principal type.  As a convenience a datatype specification in the principal signature may be viewed as an opaque type specification in the ascribed signature, in which case the constructors may be viewed as values of the opaque type.  For example, the following is a correct ascription of a signature to a module that declares a datatype:

structure S : sig type t val Z : t val S : t->t end =
  struct datatype t = Z | S of t end

Here we are regarding the datatype as an abstract type with operations determined by the constructors of the datatype.

There is one important subtlety that deserves further mention.  Suppose that the principal signature of a module contains the following specifications:

datatype t = ...
type u = t * t

and the ascribed signature contains only the specification

type u

In order for the view to make sense we must ensure that the datatype t remains present in the view, despite not being mentioned explicitly (it is implicitly mentioned by virtue of inclusion of a type declaration whose binding involves t).   This is achieved by renaming t to ?.t, thereby marking it as "hidden", and augmenting the view with an opaque type.  In the preceding example the view becomes

type ?.t
type u = ?.t * ?.t

and it is arranged that the binding of ?.t be held abstract in the resulting view.  (The complete story of how this is achieved is given in The Definition of Standard ML.)

We then determine whether the view of the principal signature is at least as general as in the ascribed signature.  This reduces to checking that the type definitions in the ascribed signature are true of the view of the principal signature induced by the ascription.  If so, then the ascription succeeds, and otherwise the ascription fails.

Finally, if the ascription is transparent, the view of the principal signature induced by the ascription is used as the signature of the structure identifier; if it is opaque, the ascribed signature is used.

To check your understanding, make sure you see why the following is a correct ascription:

signature SIG = sig
  type elt
  val lt : elt * elt -> bool
  type dict
  val empty : dict
  val insert : elt * dict -> dict
  val lookup : elt * dict -> bool
end

structure S :> SIG = struct
  type elt = int
  val lt : elt * elt -> bool
  datatype dict = Empty | Node of dict * elt * dict
  val empty = Empty
  fun insert (e, d) = ...
  fun lookup e = ...
end

[ Home ] [ Next ]

Copyright © 1997 Robert Harper.  All rights reserved.