The MetaLanguage of the Edinburgh LCF theorem proving system has become a programming language in its own right, popular among a reasonably wide segment of the research community. ML has also become a lingua franca among applied type theorists, as they investigate type systems for the 90's as extensions of the remarkably influential Hindley-Milner type system.

Standard ML is an excellent language for many kinds of programming. It is safe, efficient, suitably abstract, and concise. There are many aspects of the language that work well.

However, nothing is perfect: Standard ML has a few shortcomings. In some cases there are obvious solutions, and in other cases further research is required.

Objects with dynamic types allow the integration of operations that essentially require runtime type-checking into statically-typed languages. This paper presents two extensions of the ML language with dynamics, based on our work on the CAML implementation of ML, and discusses their usefulness. The main novelty of this work is the combination of dynamics with polymorphism.

An extension of ML with continuation primitives similar to those found in Scheme is considered. A number of alternative type systems are discussed, and several programming examples are given. A continuation-based operational semantics is defined for a small, purely functional language, and the soundness of the Damas–Milner polymorphic type assignment system with respect to this semantics is proved. The full Damas–Milner type system is shown to be unsound in the presence of first-class continuations. Restrictions on polymorphism similar to those introduced in connection with reference types are shown to suffice for soundness.

This paper provides a formal treatment of isomorphic types for languages equipped with an ML style polymorphic type inference mechanism. The results obtained make less justified the commonplace feeling that (the core of) ML is a subset of second order λ-calculus: we can provide an isomorphism of types that holds in the core ML language, but not in second order λ-calculus. This new isomorphism allows to provide a complete (and decidable) axiomatization of all the types isomorphic in ML style languages, a relevant issue for the type as specifications paradigm in library searches. This work is a very extended version of Di Cosmo (1992): we provide both a thorough theoretical treatment of the topic and describe a practical implementation of a library search system so that the paper can be used as a reference both by those interested in the formal theory of ML style languages, and by those simply concerned with implementation issues. The new isomorphism can also be used to extend the usual ML type-inference algorithm, as suggested by Di Cosmo (1992). Building on that proposal, we introduce a better type-inference algorithm that behaves well in the presence of non-functional primitives like references and exceptions. The algorithm described here has been implemented easily as a variation to the Caml-Light 0.4 system.

We describe the Edinburgh SML Library and draw lessons from its development. These lessons are of two kinds. The first concerns how to use SML to write a library, and shows some of the design choices that have to be considered. Most of the paper concerns this topic. The second kind of lesson concerns ways in which the language hinders the construction of a library. We suggest some changes to the language as a result of this experience, the most important being the addition of higher-order functors. We also suggest that language designers should consider the needs of libraries early on in the design of a language.