257 lines
11 KiB
Markdown
257 lines
11 KiB
Markdown
# Functional programming and type systems (2017-2018)
|
|
|
|
This page supplements
|
|
[the official page of MPRI 2-4](https://wikimpri.dptinfo.ens-cachan.fr/doku.php?id=cours:c-2-4-2).
|
|
|
|
## Location and duration
|
|
|
|
The lectures take place at University Paris 7 - Denis Diderot,
|
|
Bâtiment Sophie Germain, in room 2035.
|
|
|
|
They are scheduled on Fridays from 12:45 to 15:30.
|
|
There is a 15-minute break in the middle of each lecture.
|
|
|
|
## Teachers
|
|
|
|
* Functional Programming: Under the Hood (12h30, [François Pottier](http://gallium.inria.fr/~fpottier))
|
|
* Metatheory of Typed Programming Languages (12h30, [Didier Rémy](http://gallium.inria.fr/~remy/), *head*)
|
|
* Advanced Aspects of Type Systems (12h30, [Yann Régis Gianas](http://www.pps.jussieu.fr/~yrg/))
|
|
* Dependently-typed Functional Programming (12h30, [Pierre-Evariste Dagand](https://pages.lip6.fr/Pierre-Evariste.Dagand/))
|
|
|
|
## Aims
|
|
|
|
This course presents the principles and formalisms that underlie many of
|
|
today's typed functional programming languages.
|
|
(Here are some [introductory slides](slides/fpottier-00.pdf).)
|
|
|
|
The course is made up of four parts and can be split after the first two
|
|
parts.
|
|
|
|
In the first part, we discuss the *operational semantics* of functional
|
|
programming languages, and we present several classic *program
|
|
transformations*, including closure conversion, defunctionalization, and the
|
|
transformation into continuation-passing style (CPS). These program
|
|
transformations are interesting from two points of view. First, they are
|
|
*useful programming techniques*, which can help write or understand
|
|
programs. Second, they are used in the *compilation* of functional
|
|
programming languages, so they help understand what happens when the machine
|
|
executes a program. We use operational semantics to *prove* that the meaning
|
|
of programs is preserved by these transformations. Finally, we suggest how
|
|
these definitions and theorems can be expressed in a form that a machine can
|
|
check. That is, although Coq is not a prerequisite of the course, we will at
|
|
least try to *read and understand Coq definitions and statements*.
|
|
|
|
In the second part, we focus on the meta-theoretical properties of type
|
|
systems. We study parametric polymorphism (as in System F and ML), data
|
|
types and type abstraction. We show syntactic type soundness (via progress
|
|
and subject reduction) by reasoning by induction on typing derivations. We
|
|
also show how to obtain semantic properties via logical relations by
|
|
reasoning by induction on the structure of types. Finally, we introduce
|
|
subtyping, row polymorphism, and illustrate the problems induced by
|
|
side effects (references) and the need for the value restriction.
|
|
|
|
The third part of the course introduces "rich" type systems designed
|
|
to guarantee extra properties in addition to safety: principality,
|
|
information hiding, modularity, extensionality, purity, control of
|
|
effects, algorithmic invariants, complexity, resource usage, or full
|
|
functional correctness. The expressivity of these systems sometimes
|
|
endangers the tractability, or even the feasibility, of type checking
|
|
and type inference: a common thread between these lectures discusses
|
|
the tradeoffs made on the design of these systems to balance
|
|
expressivity and tractability.
|
|
|
|
The last part focuses on the use of dependent types for programming:
|
|
effectful programming with monads and algebraic effects; tagless
|
|
interpreters; programming with total functions; generic programming.
|
|
We also show the limits of dependently-typed functional programming.
|
|
|
|
## Project
|
|
|
|
The [programming project](project/) is now available!
|
|
The deadline is **Friday, February 16, 2018**.
|
|
|
|
## Approximate syllabus
|
|
|
|
### Functional Programming: Under the Hood
|
|
|
|
* (22/09/2017)
|
|
Introduction ([slides 00](slides/fpottier-00.pdf)).
|
|
Syntax and operational semantics, on paper and on a machine
|
|
([slides 01a](slides/fpottier-01a.pdf))
|
|
([slides 01b](slides/fpottier-01b.pdf)).
|
|
* Newton-Raphson in OCaml ([solution](ocaml/NewtonRaphson.ml)).
|
|
* 1 is not even in Coq ([Even.v](coq/Even.v)).
|
|
* (29/09/2017)
|
|
From a small-step semantics down to an efficient verified interpreter,
|
|
in several stages
|
|
([Coq demo](coq/DemoSyntaxReduction.v))
|
|
([slides 02](slides/fpottier-02.pdf))
|
|
([OCaml code](ocaml/Lambda.ml))
|
|
([Coq repo](coq/)).
|
|
* (06/10/2017) Compiling away first-class functions:
|
|
closure conversion, defunctionalization
|
|
([slides 03](slides/fpottier-03.pdf))
|
|
([Coq repo](coq/)).
|
|
* (13/10/2017) Making the stack explicit: the CPS transformation
|
|
([slides 04](slides/fpottier-04.pdf))
|
|
([Coq repo](coq/)).
|
|
* Transforming a call-by-value interpreter
|
|
([exercise](ocaml/EvalCBVExercise.ml), [solution](ocaml/EvalCBVCPS.ml)).
|
|
* Transforming a call-by-name interpreter
|
|
([solution](ocaml/EvalCBNCPS.ml)).
|
|
* Transforming a graph traversal
|
|
([solution](ocaml/Graph.ml)).
|
|
* (20/10/2017) Equational reasoning and program optimizations
|
|
([slides 05](slides/fpottier-05.pdf))
|
|
([Coq mini-demo](coq/DemoEqReasoning.v)).
|
|
|
|
### Metatheory of Typed Programming Languages
|
|
|
|
* (15/09/2017)
|
|
[Metatheory of System F](http://gallium.inria.fr/~remy/mpri/slides1.pdf)
|
|
[(handout)](http://gallium.inria.fr/~remy/mpri/handout1.pdf)
|
|
(see also [intro](http://gallium.inria.fr/~remy/mpri/slides8.pdf),
|
|
and chap [1,2,3](http://gallium.inria.fr/~remy/mpri/cours1.pdf)
|
|
and [4](http://gallium.inria.fr/~remy/mpri/cours2.pdf)
|
|
of [course notes](http://gallium.inria.fr/~remy/mpri/cours.pdf))
|
|
* (27/10/2017)
|
|
[ADTs, existential types, GADTs](http://gallium.inria.fr/~remy/mpri/slides2.pdf)
|
|
([handout](http://gallium.inria.fr/~remy/mpri/handout2.pdf)
|
|
[without](http://gallium.inria.fr/~remy/mpri/handout2a.pdf) or
|
|
[only](http://gallium.inria.fr/~remy/mpri/handout2b.pdf)
|
|
the extra material)
|
|
(se also [chap 6](http://gallium.inria.fr/~remy/mpri/cours4.pdf)
|
|
of [course notes](http://gallium.inria.fr/~remy/mpri/cours.pdf))
|
|
* (03/11/2017)
|
|
[Logical relations](http://gallium.inria.fr/~remy/mpri/slides3.pdf)
|
|
[(handout)](http://gallium.inria.fr/~remy/mpri/handout3.pdf)
|
|
([chap 8](http://gallium.inria.fr/~remy/mpri/cours6.pdf)
|
|
of [course notes](http://gallium.inria.fr/~remy/mpri/cours.pdf))
|
|
* (10/11/2017) ~~Subtyping. Rows.~~
|
|
[Overloading](http://gallium.inria.fr/~remy/mpri/slides4.pdf)
|
|
[(handout)](http://gallium.inria.fr/~remy/mpri/handout4.pdf)
|
|
(see also [chap 7](http://gallium.inria.fr/~remy/mpri/cours5.pdf)
|
|
of [course notes](http://gallium.inria.fr/~remy/mpri/cours.pdf))
|
|
* (17/11/2017)
|
|
[References, Value restriction, Side effects](http://gallium.inria.fr/~remy/mpri/slides5.pdf)
|
|
([handout](http://gallium.inria.fr/~remy/mpri/handout5.pdf))
|
|
(see also sections [3.6, 3.7](http://gallium.inria.fr/~remy/mpri/cours1.pdf)
|
|
and [4.5](http://gallium.inria.fr/~remy/mpri/cours2.pdf)
|
|
of [course notes](http://gallium.inria.fr/~remy/mpri/cours.pdf))
|
|
* See exercises in [course notes](http://gallium.inria.fr/~remy/mpri/cours.pdf)
|
|
|
|
|
|
### Rich types, tractable typing
|
|
|
|
* (08/12/2017)
|
|
[Introduction](slides/yrg-00-introduction.pdf),
|
|
[ML and Type inference](slides/yrg-01-type-inference.pdf)
|
|
* Subtyping
|
|
* Effects and resources
|
|
* Modules
|
|
* Dependent types
|
|
* Functional correctness
|
|
|
|
### Dependently-typed Functional Programming
|
|
|
|
* Effectful functional programming.
|
|
* Dependent functional programming.
|
|
* Total functional programming.
|
|
* Generic functional programming.
|
|
* Open problems in dependent functional programming.
|
|
|
|
## Evaluation of the course
|
|
|
|
Two written exams (a partial exam on Friday Dec 1 and a final exam) and one
|
|
programming project or several programming exercises are used to evaluate
|
|
the students that follow the full course. Only the partial exam will count
|
|
to grade students who split the course.
|
|
|
|
Only course notes and hand written notes are allowed for the exams.
|
|
|
|
Although the course has changed, you may still have a look at previous exams
|
|
available with solutions:
|
|
|
|
- mid-term exam 2016-2017:
|
|
[Record concatenation](http://gallium.inria.fr/~remy/mpri/exams/partiel-2016-2017.pdf)
|
|
- mid-term exam 2015-2016:
|
|
[Type containment](http://gallium.inria.fr/~remy/mpri/exams/partiel-2015-2016.pdf)
|
|
- final exam 2014-2015: [Copatterns](http://gallium.inria.fr/~remy/mpri/exams/final-2014-2015.pdf)
|
|
- mid-term exam 2014-2015:
|
|
[Information flow](http://gallium.inria.fr/~remy/mpri/exams/partiel-2014-2015.pdf)
|
|
- final exam 2013-2014:
|
|
[Operation on records](http://gallium.inria.fr/~remy/mpri/exams/final-2013-2014.pdf)
|
|
- mid-term exam 2013-2014:
|
|
[Typechecking Effects](http://gallium.inria.fr/~remy/mpri/exams/partiel-2013-2014.pdf)
|
|
- final exam 2012-2013:
|
|
[Refinement types](http://gallium.inria.fr/~remy/mpri/exams/final-2012-2013.pdf)
|
|
- mid-term exam 2012-2013:
|
|
[Variations on ML](http://gallium.inria.fr/~remy/mpri/exams/partiel-2012-2013.pdf)
|
|
- final exam 2011-2012:
|
|
[Intersection types](http://gallium.inria.fr/~remy/mpri/exams/final-2011-2012.pdf)
|
|
- mid-term exam 2011-2012:
|
|
[Parametricity](http://gallium.inria.fr/~remy/mpri/exams/partiel-2011-2012.pdf)
|
|
- final exam 2010-2011:
|
|
[Compiling a language with subtyping](http://gallium.inria.fr/~xleroy/mpri/2-4/exam-2010-2011.pdf)
|
|
- mid-term exam 2010-2011:
|
|
[Compilation
|
|
of polymorphic records](http://gallium.inria.fr/~remy/mpri/exams/partiel-2010-2011.pdf)
|
|
|
|
## Recommended software
|
|
|
|
Please install [opam](https://opam.ocaml.org/doc/Install.html) first.
|
|
|
|
Then, install OCaml 4.0x and Coq **8.5** via the following commands:
|
|
```bash
|
|
opam init --comp=4.05 # for instance
|
|
opam repo add coq-released https://coq.inria.fr/opam/released
|
|
opam update
|
|
opam install -j4 -v coq.8.5.3
|
|
```
|
|
(Do *not* install Coq 8.6. The version of AutoSubst that I am using is
|
|
not compatible with it. If for some reason you need Coq 8.6, or have
|
|
already installed Coq 8.6, note that `opam switch` can be used to let
|
|
multiple versions of Coq coexist.)
|
|
|
|
Please also install François Pottier's
|
|
[variant](https://github.com/fpottier/autosubst)
|
|
of the
|
|
[AutoSubst](https://www.ps.uni-saarland.de/autosubst/) library:
|
|
```bash
|
|
git clone git@github.com:fpottier/autosubst.git
|
|
make -C autosubst install
|
|
```
|
|
|
|
In order to use Coq inside `emacs`,
|
|
[ProofGeneral](https://proofgeneral.github.io/)
|
|
is highly recommended.
|
|
Here is a suggested installation script:
|
|
```bash
|
|
rm -rf /tmp/PG
|
|
cd /tmp
|
|
git clone git@github.com:ProofGeneral/PG.git
|
|
cd PG
|
|
EMACS=/Applications/Aquamacs.app/Contents/MacOS/Aquamacs
|
|
if [ ! -x $EMACS ]; then
|
|
EMACS=emacs
|
|
fi
|
|
make EMACS=$EMACS compile
|
|
TARGET=/usr/local/share/emacs/site-lisp/ProofGeneral
|
|
sudo rm -rf $TARGET
|
|
sudo mv /tmp/PG $TARGET
|
|
```
|
|
|
|
Enable ProofGeneral by adding the following line to your `.emacs` file:
|
|
```elisp
|
|
(load-file "/usr/local/share/emacs/site-lisp/ProofGeneral/generic/proof-site.el")
|
|
```
|
|
If desired, ProofGeneral can be further
|
|
[customized](https://proofgeneral.github.io/doc/userman/ProofGeneral_9/).
|
|
|
|
## Bibliography
|
|
|
|
[Types and Programming Languages](https://mitpress.mit.edu/books/types-and-programming-languages),
|
|
Benjamin C. Pierce, MIT Press, 2002.
|
|
|
|
[Advanced Topics in Types and Programming Languages](https://www.cis.upenn.edu/~bcpierce/attapl/),
|
|
Edited by Benjamin C. Pierce, MIT Press, 2005.
|