Don’t forget to submit your answers on moodle at the end of the TD!

1 Getting started

We strongly advise you to use Emacs in order to get used to it (using it will be mandatory afterward for Agda). Everything is already installed in the TD rooms. If you are working on your own computer under Ubuntu (or similar), you can get started by typing

sudo apt install emacs ocaml tuareg-mode

You should then read the two following pages:

• the Emacs shortcuts,
• the OCaml quickstart which recalls all the main OCaml constructions that you should need here.

1.1 Simple operations on unary natural numbers

As a warmup, we are going to implement operations on unary natural numbers. Open a new file named nat.ml.

• Define a type nat of unary natural numbers.
• Define the addition function on natural numbers add of type nat -> nat -> nat. Ensure that the result of adding 3 and 2 is 5.
• Define a function even of type nat -> bool which determines whether a natural number is even or not.

We recall that the type 'a option is defined in the standard library by

type 'a option =
  | None
  | Some of 'a

• Define a function pred of type nat -> nat option which computes the predecessor of a natural number. Note that this is partially defined function (there is no predecessor for 0): here, we return None to indicate that there is no result and Some n to indicate that the result is n.
• Define a function half of type nat -> nat which computes the half of a natural number rounded down (for instance the half of 5 is 2).
• Modify the function half so that it has type nat -> nat option and returns None when the argument is odd.

2 Definition of the programming language

We consider the simple programming language presented in the course where an expression p consists of either

• b: a boolean
• n: an integer
• p + q: a sum of two expression
• p < q: a comparison of two expressions
• if p then q else r: a conditional branching

Start with a new file named typing.ml.

2.1 A type for programs

Define an inductive type prog which implements programs. The constructors should be called Bool, Int, Add, Lt and If.

3 Typing

3.1 Types

A type in our language is either a boolean of an integer. Define an inductive type typ for types (the constructors should be called TBool and TInt).

3.2 Type inference

We recall that the typing rules are

Define a function infer of type prog -> typ which infers the type of a program. You will first define an exception

exception Type_error

and raise it (with raise Type_error) in the case the program cannot be typed.

3.3 Typability

Define a function typable of type prog -> bool which indicates whether a program can be typed or not. We recall that an exception can be catched with the construction

try
  ...
with
  | Exception -> ...

Check that the program

if (1 + 2) < 3 then 4 else 5

is typable but not

1 + false

nor

if true then 1 else false

4 Reduction of programs

We recall that the rules for reduction of programs are

4.1 Single step reduction

Define a function reduce of type prog -> prog option which performs exactly one step of reduction on a program and returns None if no reduction step is possible.

4.2 Normalization

Using reduce, define a function normalize of type prog -> prog which reduces a program as much as possible (we say that it normalizes the program).

Test your function on

if 1+(2+3) < 4 then false else 5

4.3 Optional: parallel reduction

Define a function preduce of type prog -> prog which performs as many reduction steps in parallel as possible. Use it to define a normalization function pnormalize and test it on the above program.

5 Extensions

5.1 Products

Add products to the language, so that we can typecheck

(1 , false)

Additionally, you should add two more operations in the language in order to be able to use pairs, which ones?

Ensure that you can define and type a program which takes a pair (say (3,2)) and swaps its two components.

5.2 Unit

Add a unit type to the language.

5.3 Optional: functions

Add functions to the language.