[Agda] ANN: "Evolution of a type-checker" & "Dependently-typed programming"

[Pierre-Evariste Dagand]

Dear People of Agda,


As part of a class on "Functional programming and type systems" (MPRI
2.4, for the connoisseurs), I have been given the opportunity to give
a (somewhat opinionated) introduction to dependently-typed functional
programming to 2nd year Masters students.


I've made my teaching material available online. First, there is an
introductory, standalone project entitled "The Evolution of a
Typechecker" (inspired by the folklore "The Evolution of a Haskell
Programmer")

    https://github.com/pedagand/typechecker-evolution

that I use to ring as many of Agda's bells and whistles as possible
while showing the transition from "idiomatic Haskell programmer" to
"idiomatic Agda programmer" (a programmer who, clearly, would live
somewhere around Glasgow).


Second comes the Teacher version (*spoiler alert*) of my lectures
notes, complete with exercises, their solutions and the infrastructure
for producing the teaching version of the Agda files :

   https://github.com/pedagand/MPRI-2.4-DTP
   https://github.com/pedagand/MPRI-2.4-DTP/blob/master/Readme.lagda.rst

It is literate Agda files all the way down : from the Agda files, I
obtain a pdf (the lectures notes) and a program with holes (the
lecture) that is discussed and elaborated in class using a wireless
keyboard with touchpad. We are basically using Agda as an interactive
whiteboard equipped with a type-checker.


If you just want to play with the student version (with the exercises,
without the answers), check out the files listed under Section
"Dependently-typed Functional Programming" on the following page:

    https://gitlab.inria.fr/fpottier/mpri-2.4-public/blob/master/README.md


Beware, I think that there is a problem with the implementation of
Djinn monotonic and I haven't had time to fix it yet. Feel free to
send a PR if you do! More generally, comments, suggestions and rants
are more than welcome, either by mail or by PR.


Many thanks to the Agda team, whose great work has made this sort of
pedagogical experience possible and, actually, extremely pleasant!

-- 
Pierre Dagand