The HOL System Tutorial is a fairly gentle introduction to using the system HOL. It provides screenshots from the interactive sessions, so you can follow what’s happening even if you don’t have the system installed. Better still, download and install HOL, then follow the tutorial to verify the sessions and get a hands-on experience with the system.
The first substantial example is a proof of this theorem: that there are infinitely many primes. The classic proof by Euclid is considered as a proof from “The Book” — in which God keeps the most elegant proof of each mathematical theorem, according to the mathematician Paul Erdös. During a lecture in 1985, Erdös said, “You don’t have to believe in God, but you should believe in The Book.”
However, to rephrase this proof in HOL, many basic concepts needs to be established first: what is a prime? how to define divisibility? All these boil down to logical statements about natural numbers.
The actual proof process in HOL is assisted by the Proof Manager. There are actions to put a goal to the manager, expand the goal by tactics, which are strategies to pick either known facts or lemma from a HOL theory. The expansion of a goal usually gives subgoals, which can be further expanded until everything is known, upon which the initial goal is proved. Of course, picking the correct strategies take some understanding and experience. The Proof Manager allows you to advance a step, backup a step, or redo from the start. All these techniques are demonstrated in this example of the Tutorial.
In the end, Euclid’s proof of the infinity of primes is done in about 10 lines of HOL code, after much polishing. This is finale of a whole chapter with more than 30 pages!
The challenge for any programming language X which claims to be general-purpose is this: can X compile itself? More specifically, can language X be used to write a compiler that compiles itself?
Most functional languages can perform this trick: John McCarthy’s Lisp in Lisp is a classic. Nowadays, there are Scheme in Scheme compilers.
Therefore it is no surprise to find an ML compiler in ML, specifically an SML compiler in SML. This is the mission for MLKit, even from version 1 in 1993. The project was to put the Definition of Standard ML (1990) into an actual implementation in SML. Since then, the 1990 Definition has been revised, and MLKit has evolved into version 4 with better and better compilation and implementation. This is a nice example of the expressive power of ML.
At first, the goal of MLKit was to understand the ML language itself. Both compilation and implementation are coded with clarity, rather than efficiency. However, this understanding provide the basis of other efficient ML implementations, including Moscow ML and Caml.
As a programming language, ML is quite powerful: it features both functional and procedural styles.
ML is born a functional language — indeed the very first implementation of ML is in Lisp, the grand-daddy of functional programming. Like Lisp, ML has a top-level read-evaluate-print loop, making it interactive. However, ML is not an interpretative language: the top-level interactive loop is actually running an incremental compiler. Most ML implementations will compile ML into some form of lambda expressions. Possible ways to deal with these lambda expressions are:
- Interpret the lambda expressions.
- Compile the lambda expressions into byte-codes of some abstract machine, and run the abstract machine.
- Convert the abstract machine byte-codes into native machine codes, to be run directly in real machines.
In pure functional programming, data are only transformed, never modified, hence no side-effects. This simplifies reasoning about program correctness. However, real-world applications need to interact with the world (e.g. response to mouse clicks) — which depends on side-effects. Procedural programming is largely based on data changes, the most explicit being the use of pointers in C/C++ to modify memory locations directly.
Intended for building practical applications (like theorem provers) ML provides procedural features such as assignments and references. As a result ML shares many goodies of mainstream programming languages, e.g. use of modules and separate compilation.
However, even with these many features, ML is not a bloated language. It has a well-thought-out design, just using typed lambda calculus. The evolution of ML is a story about how to implement functional languages efficiently, and how to achieve performance comparable to procedural languages.
I start to play with ML, the MetaLanguage for theorem-provers. It is developed by Robin Milner and others in the early 1970s at the University of Edinburgh. It is now standardized as SML, the Standard ML.
A good ML Tutorial is this:
Tips for Computer Scientists on Standard ML (Revised) by Mads Tofte (2009), which describes all of Standard ML in 20 pages.
To try out ML, I install Moscow ML by Sergei Romanenko. The Windows installer is very convenient. It runs in command-line mode, which is interactive enough for trying out ML.
For a few lines, typing is OK. For many more lines, an editor is much preferred. I’m using TextPad, and I’m able to locate an SML syntax file for TextPad.
Poly/ML by David Matthews is also good for learning ML. It is Windows-based, and the documentation includes a short tutorial on programming Windows in Poly/ML. Sounds exciting.
I can run ML scripts with both Moscow ML and Poly/ML. The Poly/ML window even has copy/paste — so I can copy ML snippet from tutorials and paste to the window for execution.
The language ML is rich with features, so it may take some time to know it well.
Stephen Gilmore wrote a nice set of tutorial: Programming in Standard ML ’97. There is a chapter on Types and type inference. He praises type checking of ML in compile time, making it impossible to have runtime type errors. He cites C as an example of those languages that “neither guarantee to enforce type-correctness when the program is compiled nor when it is running.” It is interesting to note that C programmers have since invented (or recommended) the Hungarian notation to minimize such type errors syntactically.
While type inference can save the programmer the tedious task of declaring types (for variables, function parameters and return values), it can be too smart: a typo that somehow didn’t cause syntax error can lead to a weird type being deduced. This may be easily spotted in top-level interactive mode, but can be hard to find if a large program is being compiled in batch mode.
Robin Milner, who developed ML, worked out an algorithm for type inference in 1978. He just call it Algorithm W.
Martin Elsman directs me to these doco relating to the Pattern Matching algorithm in ML:
- Peter Sestoft: ML Pattern Match Compilation and Partial Evaluation
- Martin Elsman: Polymorphism and Unification of Cyclic Terms
Peter’s paper is quite thorough: starting with codes of a naive ML pattern matcher, he improves it to the instrumented ML pattern matcher. He proceeds to show ML match compilation, also with codes — all within 20 pages!
Martin’ paper confirms my hunch that ML pattern matching is closely related to the unification algorithm of Prolog. Again the algorithm is presented with actual codes, making this enjoyable reading.
Unification is pattern matching on structured data: for example matching a list by its head and tail. The best known algorithm for unification of first-order logic is due to John Robinson in 1965.
It is a pleasure to read the Caml Tutorial. Besides bringing ML’s type-inference into focus, it also introduces pattern matching in functional programming. This is an eye-opener for a Java programmer.
This is different from pattern matching via Regular Expressions in most programming languages. More in the tradition of Prolog patterns, where matching is done via unification, this is another prominent feature of modern functional languages.
Part 3 of the Tutorial is building a toy language ASL entirely in Caml Light. This is where ML shines. Using a language to build a toy language of itself is always a good example of how self-contained the language is.