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

You first need to install OCaml and an editor, for which we advise to
either use *VS Code* or *Emacs* (the former is better
looking, the later is better).

On Ubuntu, you can install ocaml and emacs with

```
sudo apt update
sudo apt install ocaml emacs elpa-tuareg
```

On Windows, we advise you to

install WSL by running in a terminal (right click and then

*Run as administrator*) and typing`wsl --install`

launch Ubuntu from Windows and follow the above steps.

You should

If you want to install VSCode, we recommend that you install the clutter-free version called VSCodium (but the traditional VSCode will do as well). Once done, you should

- first install the
*OCaml Platform*extension (with`ctrl + shift + x`

), - if you are on Windows, also install the
*WSL*extension.

You can evaluate selected code with `shift + enter`

.

*Formatting code.* If you want to be able to automatically
reformat your code, you need to install `ocamlformat`

`apt install ocamlformat`

and you also need to have an empty file named
`.ocamlformat`

in the current directory. You can the reformat
your code with `ctrl + shift + i`

.

You should then read the two following pages:

- the 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?

Add a unit type to the language.

Add functions to the language.