# Typing a simple programming language

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:

## 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).

``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.