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 directory tcc/*, 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.fr
- Address: 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 directory tcc/ 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 file ast.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 code type tl_expression = ... | TL_Const of int | ... should be replaced by type 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 function fun x -> x. Indeed, a type rule called intersection introduction is 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 n types, for n >= 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.