Lectures given at the *Bertinoro International Spring School for graduate students in computer science*, 2005.

Based on F. Pottier and X. Leroy's course on "Typage et programmation", DEA Programmation.

- Slides on the syntax and the semantics of mini-ML, monomorphic types, polymorphic types, type inference, safety.
- Slides on extensions of mini-ML: tuples, sums, recursive types, algebraic datatypes, references, exceptions.
- Slides on more extensions of mini-ML: extensible records, a simple object calculus, subtyping, dynamic types.
- Slides on the Objective CAML module system.
- A minimal bibliography.

The solution is due on 30 May 2005, 6pm. Send me by email or by snail-mail your solution to the exercises; send me by email a tarred and compressed copy of the directorytcc/*, containing the solutions to the programming exercises.I'd like to keep a list of the students interested in this exam, so that, if any problem arises, I can quickly get in touch with all of you. So, please, let me know by email if you plan to solve the exam.

Email:Francesco.Zappa_Nardelli (at) inria.frAddress:Francesco Zappa Nardelli, Projet Moscova, INRIA Rocquencourt, Domaine de Voluceau, B.P. 105, 78153 Le Chesnay Cedex, France

This exam is supposed to be a complement to the lectures. Whenever you do not understand one question, or you do not see how to proceed, feel free to explain me the problem you have: I will be happy to provide guidance and hints. I will also keep an updated FAQ below.I am grateful to Gilles Peskine and to Luc Maranget for their comments, and to James Leifer for double-checking my hopeless English prose.

- The solution of the exam.
- A solution of the programming exercises.
- The email sent to the students, with some comments on their exams (in italian).
- The list of the students who validated this exam.

## FAQ

(A question turns into a FAQ if it is asked by at least two persons.)

Q: How can we import a file into OCaml top-level?A:

#use "filename.ml". If you want to import all the code in the directorytcc/into the top-level, then follow the instructions below.$ cd tcc $ make $ ocaml Objective Caml version 3.08.3 # #use "ast.ml";; [...] # #load "lexer.cmo";; # #load "parser.cmo";; # #use "util.ml";; [...]Now you can use all the relevant functions. For instance:# let example s = let (a,tau) = parse_expression s in print_endline(print_expression a); print_endline(print_type tau);; val example : string -> unit =# example "3 : int";; 3 int - : unit = () Q: Exercise 2, translation of types: you show how to translate record types, but the source language does not have records!A: Replace the translation of record types with the translation for product types defined as:

[[ tau_1 * tau_2 ]] = [[ tau_1 ]] * [[ tau_2 ]]. The exam has been updated accordingly on 19 April.Q: In the fileast.ml, the abstract syntax of the target language forces constants to be integers!A: When I solved the exercise I had only integer constants; then I added booleans but I did not test my solution (OCaml typechecker would have complained here...). In

ast.ml, the codetype tl_expression = ... | TL_Const of int | ...should be replaced bytype tl_expression = ... | TL_Const of constant | .... The archive above has been updated on 21 April.Q: In Exercise 2, when you talk of records, do you mean extensible records?A: No! By records I mean records, as defined in slides 65-66.

Q: Did you forget a typing rule in Exercise 1?A: With the type rules for intersection types given in the Exercise 1, it is impossible to associate the type

(int -> int) /\ (bool -> bool)to the identity functionfun x -> x. Indeed, a type rule calledintersection introductionis missing. The exam has been updated accordingly on 13 April 2005.

Important:the only question affected by the missing rule is Question 4, point (2). If you solved this question before the exam was updated, I will accept it as correct.Q: Exercise 1. Can an intersection type be the intersection of 0 types?A: The grammar of types allows only binary intersections. You can prove that associativity holds for intersection types, and build intersections of

ntypes, forn >= 1; but the intersection of 0 types is not a type. So, the answer is no.Q: Can I solve the exam in Italian?A: Of course: choose your favourite among Italian, English, and French.

Q: This exam is amazingly long!A: It is not that long: the typesetted correction is two pages long, and the source code you have to write keeps in 200 lines.

Last updated: 26-4-2005