PFA ("Programmation fonctionnelle avancée") - 2011

PFA is a course about advanced aspects of functional programming. It is part of the Master 2 Spécialité Programmation et Logiciels Sûrs of Institut Galilée, Université Paris Nord.

This year I teach classes (CM), while Jean-Yves Moyen manages the lab exercises (TP). With some fine-tuning and changes, the first half of my lessons is based on what Jean-Vincent Loddo and Jean-Yves did in 2009; of course all mistakes in what I do or write remain mine.

Even if I speak French in class, I maintain these pages in English. There are essentially three reasons:

• English is easier for me to use, and I can update the page much faster this way. Don't expect to read a new Shakespeare on the course page, but at least this thing will be up-to-date.
• I'd like these pages to be be useful to other people who don't understand French. English is much more widely spoken.
• The most important reason is that you are expected to work with English-only documentation. As Master-level students you have to speak English: please get at least used to read it.

Jean-Yves Moyen has prepared a really, really nice project based on trivialML. You can find the problem statement and an archive to download on his web page. Of course the elecronic version is always the most up-to-date.

Previous written exams, including solutions

• The 2011-12-13 exam is here.
• The 2011-06-16 rattrapage is here.
• The 2010-12-17 exam is here.
• An old exam (by Jean-Vincent Loddo et Jean-Yves Moyen) is also available, but be careful: the course content was not the same back then.

Mon  2011-09-19  13:45..17:00  PFA CM1  C308
[Tue 2011-09-20  13:45..17:00  PFA TP1  F204]
Tue  2011-09-27  13:45..17:00  PFA CM2  Amphi D
[Tue 2011-10-04  13:45..17:00  PFA TP2  F204]

Tue  2011-10-18  13:45..17:00  PFA CM3  C308 + Amphi A
[Tue 2011-10-25  13:45..17:00  PFA TP4  F204]
Tue  2011-11-15  13:45..17:00  PFA CM4 C308 + C306
[Tue 2011-11-22  13:45..17:00  PFA TP5 F204]
Mon  2011-11-28  13:45..17:00  PFA CM5 C308

[Tue 2011-12-06  13:45..17:00  PFA TP6 F204] [annulé]
[Tue 2011-12-13  14:00..17:00  PFA exam F001]

In September 2011 I made a course mailing list, used for communications and answering questions: if you are a PFA student you are strongly advised to subscribe using this simple web interface. You can send a message to all subscribers (including Jean-Yves Moyen and me, of course) by writing to the address pfa@lipn.univ-paris13.fr . You are free to use a nickname instead of your real name on the list, if you prefer so.

We will use the Objective Caml language, also called OCaml; you are expected to become fluent in it.
You don't really need to buy books about the language unless you prefer the paper format, as the documentation you find on the Net is really good; in several cases the same text is available on paper and in electronic form.

Of course, you should always have available the official OCaml documentation, particularly the default interface library. We also recommend the following texts, all of which are available online:

• Emmanuel Chailloux, Pascal Manoury, Bruno Pagano, Developing Applications With Objective Caml. Available in English and in French.
• Pierre Weis and Xavier Leroy, Le langage Caml, Dunod, 1999. Despite the fact that it doesn't use the current Objective Caml language because of its age, we recommend this book for its excellent programming examples. In French.
• Jean-Vincent recommends this draft of an OCaml book by Jason Hickey.
• A student told me he likes this online course in French by Maxence Guesdon [link updated in 2015].
• I still fondly remember the book from which I learnt functional programming many years ago, Functional programming using Caml Light by Michel Mauny. The language used in the book is the older Caml Light dialect instead of OCaml (there are differences in modules, and some minor syntactic aspects such as infix operators, and Caml Light lacks the object-oriented features), but essentially all the exposition remains valid.

• CM1: introduction to functional programming and OCaml
  • Introduction to functional programming and OCaml.
  • Very informal introduction to static typing, type inference and parametric polymorphism.
  • An introduction to sum types, if there is time.
  Relevant handout: Syntaxe simplifiée (et idéalisée) de OCaml avec sémantique informelle by Jean-Vincent Loddo.
  The OCaml code I wrote while speaking
• CM2: more programming in OCaml: sum types, polymorphism
  • Sum types with extensive examples: lists-as-sums, Peano numbers, binary search trees (set operators).
  No source code this week, unfortunately: there was a problem with the projector of Amphi D, and I had to use the blackboard only.
• CM3: modules and functors
  • Separation between interface and implementation, abstract data types; visibility of private definitions.
  • Modules and signatures, with examples.
  • Implemented a "set" abstract data type using lists, with modules and signatures signature. Shown how to use the OCaml library documentation; and the OCaml sources, if we don't have access to all the documentation (I had forgotten do download some files, which has been an opportuity for finding the information elsewhere).
  • Modifed our set data structure so that a comparison function (equality only) needs to be supplied as parameter to all the exported functions.
  • Functors. Turned the previous version of our "set" implementation into a functor: now the comparison function is only provided once at functor application time, and the resulting module is friendly to use.
  • Played with predefined functors: Map.
  • Hint at ad-hoc polymophism: the = operator is the easiest example.
  • Started speaking about interpreters: introduced a language similar to Jean-Yves' expression language, with a let form. Abstract syntax only; I explained what a parser is (many people seemed not to have understood it) and said that we will generate one automatically the next time.
  Relevant handout: Modules et foncteurs en OCaml by Jean-Vincent Loddo.
  The source code I have written on my computer while talking is available here.
• CM4: denotational semantics and interpreters
  • From mathematical semantics to executable semantics: formal syntax and semantics of TrivialML. Explained very carefully.
  • Using OCaml as a meta-language: implemented TrivialML by closely following mathematical syntax and semantics.
    • Implemented environments in OCaml, as functions. Some panicky expressions among the students prompted me to also provide a list-based implementation.
    • Written the expression evaluator in OCaml; explained very carefully.
    • Not implemented the toplevel form and program evaluators yet
  • Written a printer for values, and tested the expression interpreter by directly using the sum type for expressions, with no parser.
  • Very quick introduction to lexer and parser generators. Started adapting on the fly a frontend which I had prepared, but students were tired and it was late.
  Relevant handout: The trivialML language: formal syntax, semantics and typing, by me, sections 1 and 2. [I've distributed version 2.1 on paper; in version 2.2 I've just reformulated the grammar production for programs by removing the Kleene star operator "*" and replacing it with two productions featuring explicit recursion, as I also did in class; the language is exactly the same with either version; in version 2.3 I've corrected an obvious mistake in the si..alors..sinon case of the evaluation function definition, and added two references about type inference].
  The source code I have written on my computer while talking is available here.
• CM5: static typing
  • Distributed paper copies of the project problem statement prepared by Jean-Yves;
  • OCamlLex and OCamlYacc: re-explained at the beginning of the session, when students were more receptive;
  • implemented the frontend for trivialML, and showed that now the interpreter works and can be used with programs in concrete syntax. Computed the factorial of 10 in trivialML;
  • with static typing we can catch many errors before ever starting execution;
  • understanding sequent calculus rules and proofs;
  • typing rules for trivialML expressions. Typing some language forms not in trivialML (while, for and for-each loops);
  • imperative langugage semantics: hinted at how we can extend TrivialML's semantics to allow for side effects;
  • type checking in a different style: Abstract Interpretation;
  • Abstract Interpretation: from mathematics to OCaml (on the computer). We have written the complete type checker for expressions, but we have not called it from the main program yet.
  Relevant handout: The trivialML language: formal syntax, semantics and typing, by me, section 3.
  The source code I have written on my computer while talking is available here. I've also quickly written some instructions about how to use the trivialML interpreter.
• CM6: runtime
  • Finished what we started in CM5: integrated the type checker into the trivialML interpreter.
  • Object life time: stack allocation vs. heap allocation
  • Tagging and boxing: low-level data representation
    • Why we can avoid some tagging when we use static typing
  • Introduction to automatic memory management
    • Reference counting
    • Tracing garbage collection
    • Mark-and-sweep
    • Semispace (handwaving a little)
  • Exercise: extending trivialML with pairs and unary operators. Updated the mathematical definition (syntax, semantics, type rules, abstract-interpretation typing) and the OCaml code. I won't publish that part of the code, since the project contains something similar.
  The source code I have written on my computer while talking, integrating static type checking into trivialML, is available here. I have intentionally left a bug in the type checking of recursive procedures: explain it and fix it.
  I used a Beamer presentation: runtime-presentation.pdf.

Here you can find electronic copies of what I distribute on paper in class, and copies of my projector presentations.

You can find here copies of the ML files I write in class on my computer. Some of them weren't originally supposed to be published as they are not particularly well-written: I use them as exercises or examples writing them while I speak; anyway some students requested a copy, so here they are.

You can find TPs on Jean-Yves Moyen's page.

In CM5 we finished implementing a very simple but usable interpreter for the trivialML language (static type checking is implemented but not called from the main program yet, as of the end of CM5). The complete interpreter sources are available here.

The trivialML interpreter simply reads its program from the standard input, then it evaluates it and prints the result on the standard output. It performs no output until it has read its input program.

Example:

# Clean old compiled stuff if any, and recompile:
./CLEAN && ./GO

# If everything has worked now the file a.out exists: this is the trivialML interpreter:
ls a.out

# Run trivialML a program:
./a.out
# Write a trivialML program, then push Ctrl+D to close the standard input channel.
# The interpreter will compute and print the result.

Back to my home page...