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 with
sudo apt update
sudo apt install ocamlOn Windows, we advise you to
install WSL by running in a terminal (right click and then Run as administrator) and typing
wsl --installlaunch Ubuntu by running wsl follow the above
steps:
sudo apt update
sudo apt install ocamlYou 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
ctrl + shift + x),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
sudo apt install ocamlformatand 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:
As a warmup, we are going to implement operations on unary natural
numbers. Open a new file named nat.ml.
nat of unary natural numbers.add of
type nat -> nat -> nat. Ensure that the result of
adding 3 and 2 is 5.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 'apred 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.half of type
nat -> nat which computes the half of a natural number
rounded down (for instance the half of 5 is 2).half_opt, whose type is 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 booleann: an integerp + q: a sum of two expressionp < q: a comparison of two expressionsif p then q else r: a conditional branchingStart 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_errorand 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 5is typable but not
1 + falsenor
if true then 1 else falseWe 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 5Define a function preduce of
type prog -> prog which
performs as many reduction steps in parallel as possible: for instance,
in a program of the form add (p1, p2), it will reduce
p1 and p2. 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.