Exercise 1: Getting Started with ML

Setting Your Path

All the programs you will need to run on the HPC lab computers for this course are located in the one directory:

/home/dcs/jdg659/pub/bin

You'll be needing to run files from this directory quite often, so you should add it to your UNIX path. If you haven't modified the setup of your HPC lab account, then you can do this by adding the following line to your .cshrc file.

setenv PATH ${PATH}:/home/dcs/jdg659/pub/bin

Starting ML (without HOL or Emacs)

ML is a powerful programming language. The HOL theorem prover is essentially ML plus a great many definitions. However, you may wish to use ML on its own. To start ML just type the command `mosml' at the UNIX prompt. This should start the Moscow ML system.

Try starting ML now. If you succeed, you should see the following:

> mosml
Moscow ML version 1.43 (April 1998)
Enter `quit();' to quit.
-

Evaluating Expressions

ML code can be interpreted or compiled. When you see the `-' prompt you can type an expression (terminated by `;'), the interpreter will then evaluate it and print the result. Try evaluating some simple expressions like these:

• 1
• 1+2
• [1,2,3]
• rev [1,2,3]
• true
• false orelse true
• "Hi There"

Notice that the interpreter also prints the type along with the value of the result. Functions in ML are first-class objects; that is, they are also values. Try evaluating the expression rev. What was its type?

Making Definitions

You can bind a value to a name in ML by typing

val name = expression;

- val one = 1;
> val one = 1 : int
- one + one;
> val it = 2 : int

You are free to free to redefine names, for example, you could now say:

- val one = 2;
> val one = 2 : int
- one + one;
> val it = 4 : int

Notice that if you just evaluate an expression without binding it to a name, then ML will automatically bind it to the name it for you. Each evaluation redefines it, so it is always the value of the last expression evaluated. Check this for yourself by evaluating some expression and then evaluating it.

Functions

ML allows you to write function valued expressions (effectively, lambda-abstractions). A function that takes some value x and returns (x + 1) is written as follows:

fn x => x + 1

Another, more usual, way to define functions is as follows:

fun name x = expression;

val name = fn x => expression;

Quitting ML

To exit ML just type `quit();' or C-d at the `-' prompt.