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). In order to use it quickly, I have set up an online version at the following url: http://emacs.mimram.fr.

If you are working under Ubuntu (or similar), you can get started by typing

sudo apt install emacs ocaml tuareg-mode

If you are not familiar with Emacs, have a look at the shortcuts.

If you are not familiar with OCaml please read this quickstart which recalls the main OCaml constructions.

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 Reduction of programs

We recall that the rules for reduction of programs are

reduction rules

3.1 Single step reduction

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

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

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.

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

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

4 Typing

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

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

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

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?

5.2 Unit

Add a unit type to the language.