The OCaml compiler, its programming environment and its documentation are available at the Web site http://caml.inria.fr. The documentation includes the reference manual of the language and some tutorials.
The recent book of Chailloux, Manoury and Pagano [12] is a complete presentation of the OCaml language and of its programming environment. The book is written in French, but an English version should be soon available electronically. Other less recent books [15, 74, 26] use the language Caml Light, which approximatively correspond to the core OCaml language, covering neither its module system, nor objects.
For other languages of the ML family, [58] is an excellent introductory document to Standard ML and [51, 50] are the reference documents for this language. For Haskell, the reference manual is [38] and [70, 30] give a very progressive approach to the language.
Typechecking and semantics of core ML are formalized in several articles and book Chapters. A concise and self-contained presentation can also be found in [43, 42, chapter 1]. A more modern formalization of the semantics, using small-step reductions, and type soundness can be found in [77]. Several introductory books to the formal semantics of programming languages [25, 52, 67] consider a subset of ML as an example. Last, [11] is an excellent introductory article to type systems in general.
The object and class layer of OCaml is formalized in [66]. A reference book on object calculi is [1]; this book, a little technical, formalizes the elementary mechanisms underlying object-oriented languages. Another integration of objects in a language of the ML family lead to the prototype language Moby described in [20]; a view mechanism for this language has been proposed in [21].
Several formalization of Standard ML and OCaml modules have been proposed. Some are based on calculi with unique names [51, 48], others use type theoretical concepts [27, 44]; both approaches are compared and related in [45, 69].
ML is actually better characterized by its type system than by its set of features. Indeed, several generalizations of the ML type system have been proposed to increase its expressiveness while retaining its essential properties and, in particular, type inference.
Subtyping polymorphism, which is used both in popular languages such as Java and in some academic higher-order languages, has long been problematic in an ML context. (Indeed, both Java and higher-order languages share in common that types of abstractions are not inferred.) However, there has been proposals to add subtyping to ML while retaining type-inference. They are all based on a form of subtyping constraints [3, 19, 62] or, more generally, on typing constraints [54] and differ from one another mostly by their presentation. However, none of these works have yet been turned into a large scale real implementation. In particular, displaying types to the user is a problem that remains to be dealt with.
Other forms of polymorphism are called ad hoc, or overloading polymorphism by optimists. Overloading allows to bind several unrelated definitions to the same name in the same scope. Of course, then, for each occurrence of an overloaded name, one particular definition must be chosen. This selection process, which is called name resolution, can be done either at compile-time or at run-time, and overloading is called static or dynamic, accordingly. Name resolution for static overloading is done in combination with type-checking and is based on the type context in which the name is used. For example, static overloading is used in Standard ML for arithmetic operations and record accesses. Type information may still be used in the case of dynamic overloading, but to add, whenever necessary, run-time type information that will be used to guide the name resolution, dynamically. For example, type classes in Haskell [38] are a form of dynamic overloading where type information is carried by class dictionaries [55, 36], indirectly. Extensional polymorphism [17] is a more explicit form of dynamic overloading: it allows to pattern-match on the type of expressions at run-time. This resembles to, but also differ from dynamics values [47, 2].
The system F<:ω, which features both higher-order types and subtyping, is quite expressive, hence very attractive as the core of a programming language. However, its type inference problem is not decidable [75]. A suggestion to retain its expressiveness and the convenience of implicit typing simultaneously is to provide only partial type reconstruction [60, 56]. Here, the programmer must write some, but not all, type information. The goal is of course that very little type information will actually be necessary to make type reconstruction decidable. However, the difficulty remains to find a simple specification of where and when annotations are mandatory, without requiring too many obvious or annoying annotations. An opposite direction to close the gap between ML and higher-order type systems is to embed higher-order types into ML types [24]. However, this raises difficulties that are similar to partial type reconstruction.
Actually, most extensions of ML explored so far seem to fit into two categories. Either, they reduce to insignificant technical changes to core ML, sometimes after clever reformulation though, or they seem to increase the complexity in disproportion with the gain in expressiveness. Thus, the ML type system might be a stable point of equilibrium —a best compromise between expressiveness and simplicity. This certainly contributed to its (relative) success. This also raised the standards for its its successor.