Typing a simple programming language

Samuel Mimram

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.

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

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

2 Definition of the programming language

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

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

typing rules

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

  | Exception -> ...

Check that the program

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

is typable but not

1 + false


if true then 1 else false

4 Reduction of programs

We recall that the rules for reduction of programs are

reduction rules

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.