Typing a simple programming language

Samuel Mimram

If you are not familiar with OCaml, please read this quickstart first (it recalls the basics of OCaml as well as editing). You can use whichever editor you’d like, but Emacs or Atom is strongly recommended since it will be used afterward.

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

1 Basic setup

Before starting, launch a terminal and run the following magic command, which should setup everything we need for you:

wget -O - http://inf551.mimram.fr/install.sh | /bin/sh

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 a recursive 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
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 a recursive 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
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)

In addition to pairs, you should add two more constructions in order to be able to use pairs, which ones?

5.2 Unit

Add a unit type to the language.