Ch.11 Separate compilation in SML#

§ 11.3. Structure of interface files

An interface file describes the interface of a source file to be compiled separately. Its contents consists of Require declarations and Provide declarations. Require declarations specifies the list of interface files used in this compilation unit as a sequence of declarations of the following form.

_require smiFilePath

smiFilePath is an interface file (smi file) of other compile unit. Frequently used interface files can be grouped together and given a name. SML# maintain a few of them. A useful example is basis.smi which contain all the (mandatory) names (types, functions etc) defined in Standard ML Basis Library. In order to make the basis library available, write the following at the beginning of its interface file.

_require "basis.smi";

Provide declarations describes the resources implemented in this compile unit. Resources corresponds to those definable as SML# declarations, including the following.

  • datatype definitions

  • type definitions

  • exception declarations

  • infix declarations

  • variable definitions

  • module definitions

  • functor definitions

Below is an example interface file queue.smi and its implementation queue.sml.

queue.smi file:

_require "basis.smi"
structure Queue =
struct
  datatype 'a queue = Q of 'a list * 'a list
  exception Dequeue
  val empty : 'a queue
  val isEmpty : 'a queue -> bool
  val enqueue : 'a queue * 'a -> 'a queue
  val dequeue : 'a queue -> 'a queue * 'a
end

queue.sml file:

structure Queue =
struct
  datatype 'a queue = Q of 'a list * 'a list
  exception Dequeue
  val empty = Q ([],[])
  fun isEmpty (Q ([],[])) = true
    | isEmpty _ = false
  fun enqueue (Q(Old,New),x) = Q (Old,x::New)}
  fun dequeue (Q (hd::tl,New)) = (Q (tl,New), hd)
    | dequeue (Q ([],_) = raise Dequeue
    | dequeue (Q(Old,New) = dequeue (Q(rev New,[]))
end
Figure 11.2. Example of interface file

As seen in this example, Provide declarations in interface file resembles Standard ML signatures. A big difference is that in provide declarations in an interface file, datatype and exception are not specifications but they represent unique entities. datatype 'a queue and exception Dequeue declared in queue.smi are treated as the generative type and exception in its implementation. As a result, they corresponds to the same entity even if queue.smi is used in multiple interface files through _require declarations.