Table of Contents
History and Acknowledgements
Poly/ML was originally written by David Matthews at the Computer Laboratory at Cambridge University. It was written in an experimental language, Poly, similar to ML but with a different type system. Among the first users was Larry Paulson who used it to develop the Isabelle theorem prover. It was licensed by Cambridge University's company Cambridge University Technical Services, then called Lynxvale, to Abstract Hardware Limited (AHL) who developed it further and used it to write the Lamba system for hardware verification as well as other tools. Mike Crawley did significant work on the run-time system and Simon Finn was heavily involved in translating Poly/ML from Poly into Standard ML. Nick Chapman (nic AT truthmachine DOT demon DOT co DOT uk) wrote the C-language interface. In 1999 AHL's rights in Poly/ML were acquired by CUTS and they agreed to make Poly/ML freely available.
More recently David Matthews has continued to develop Poly/ML. The Standard Basis Library has been implemented and the compiler converted to the 1997 Definition of Standard ML (Revised). This work was supported in part by LFCS. The most recent work has been rewriting the run-time system which has resulted in the version 5 release. This work was supported by the Verisoft project and the Technical University of Munich.
Since the version 4.0 release Poly/ML now supports the full version of the language as given in the "Definition of Standard ML (Revised)", generally known as ML97.
As well as being extremely fast and efficient implementation of Standard ML Poly/ML provides several additional features. The Thread library allows parallel threads to be created that can make use of multi-core processors. There is a foreign language interface which allows dynamically linked libraries to be loaded and functions within them called from ML. An X-Windows interface using Motif is available and a Windows programming interface. There is also a symbolic debugger for Poly/ML.
Poly/ML is available for the most popular architectures and operating systems. There are native code versions for the i386 (32 and 64 bit). There is a byte-code interpreted version which can be used on unsupported architectures. The configure script will automatically select the architecture when building from source.
You need to build Poly/ML from source and provide the --with-x option to the configure script. Check that you have the appropriate X-Windows and Motif libraries installed first.
The easiest way to build a stand-alone application is with polyc. This is a script that compiles a Standard ML program using the Poly/ML compile and creates an executable program from it. It can also be used to link object files created using the PolyML.export function with the Poly/ML libraries or to produce an object file. When used to compile a Standard ML program it expects the main function to be called "main" e.g.
fun main() = print "Hello World\n";
If the source file is a text file it is assumed to be ML source. If it is a binary file it is assumed to be an object file and will be linked with the Poly/ML library.
Earlier versions of Poly/ML printed values of abstract types and types in opaque signatures just as "?". From version 5.3 Poly/ML now prints the values using the constructors. To suppress this and return to the old behaviour you need to install a pretty-printer for the abstract type. The following code installs a pretty printer that always prints "?" for a type.
let fun pp _ _ (_: MY_TYPE) = PolyML.PrettyString "?" in PolyML.addPrettyPrinter pp end;
Generally the best place to put this code is inside the implementation of the abstract type. This applies whether you are using an abstype or transparent or opaque signature matching to achieve your abstract type. It is also possible to install the pretty printer outside the abstract type and this will work equally well with abstype and transparent matching. With opaque signature matching you can also install the pretty printer outside the structure definition but in some circumstances, particularly if an exception is raised inside the implementation which contains the abstract type as a parameter, the value may be printed with the default printer instead.