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

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.

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.

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`

.

Define an inductive type `prog`

which implements programs.
The constructors should be called `Bool`

, `Int`

,
`Add`

, `Lt`

and `If`

.

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`

).

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.

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`

We recall that the rules for reduction of programs are

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.

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`

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.

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.

Add a unit type to the language.

Add functions to the language.