The Standard ML programming language is defined formally. This definition is presented as a book of rules [MTHM97] expressed in so-called Natural Semantics, a powerful but concise formalism which records the essential essence of the language while simultaneously abstracting away from the uninformative detail which would inevitably be needed in a programming language implementation. As a comparison, the published model implementation of Standard Pascal [WH86] is five times longer than the definition of Standard ML. This is a shocking fact because Standard ML is a much more sophisticated language than Pascal. In these notes we follow the 1997 revision of the language definition.
Standard ML consists of a core language for small-scale programming and a module system for large-scale programming. The Standard ML core language is not a pure applicative programming language, it is a higher-order procedural language with an applicative subset. For most of these notes the focus will be on using the applicative subset of the language so we will spend some time discussing functions, in particular recursive functions, and giving verification techniques for these. In the early sections of these notes the examples are all small integer functions. Later, Standard ML's sophisticated type system is presented. The design of the Standard ML programming language enables the type of any value to be computed, or inferred, by the Standard ML system. Thus, the language has a strong, safe type system but does not force the programmer to state the type of every value before use. This type system facilitates the detection of programming errors before a program is ever executed.
John Hughes in [Hug89] suggests that one of the advantages of functional programming is the ability to glue programs together in many different ways. For this, we require the ability to manipulate functions as data. We will pass them as arguments to other functions and even return them as the results of functions. In order for such a powerful mechanism to be exploited to the fullest, the language must provide a means for functions to be defined in a general, re-usable way which allows values of different types to be passed to the same function. As we shall see, Standard ML provides such a feature without compromising the security of the type system of the language.
The mechanism by which applicative programs are evaluated is then discussed. This leads into the consideration of alternative evaluation strategies one of which is so-called lazy evaluation. This strategy has a profound effect on the style of programming which must be deployed.
The other elements of the Standard ML core language which are discussed are the mechanism used to signal that an exceptional case has been detected during processing and no consistent answer can be returned and the imperative features such as references and interactive input and output.
The core language offers a comfortable and secure environment for the development of small programs. However, a large Standard ML program would contain many definitions (of values, functions or types) and we begin to require a method of packaging together related definitions; for example, a type and a useful collection of functions which process elements of this type. Standard ML has modules called structures. Structures facilitate the division of a large program into a number of smaller, independent units with well-defined, explicit connections. A large programming task may then be broken up so that several members of a programming team may independently produce structures which are assembled to form a single program.
Another reason for tidying collections of definitions into a structure is that we can pass structures as arguments and return them as results. In Standard ML the entity which plays the role of a function mapping structures to structures is called a functor.
Finally, we may wish to take the opportunity when collecting definitions into a structure to hide some of the declarations which played a minor role in helping the implementor to construct the major definitions of the structure. Thus, we require a interface for our structure. The Standard ML term for such an interface is a signature.