Safely typing algebraic effects

Last year (2017), I was following the MPRI, a research-oriented master programme in Paris. The project for the Functional programming and type systems course (taught by François Pottier, Didier Rémy, Yann Régis-Gianas and Pierre-Évariste Dagand) was to write a compiler for a tiny functional language. I extended that project with algebraic effects and a static type system checking that effects could not be unhandled. Explaining the type system of my implementation is what this post is about.

next

Parser Construction With Menhir: A Couple Appetizers

This post is a shameless advertisement for Menhir, a parser generator for OCaml. It illustrates Menhir’s new input syntax, which was introduced on November 13, 2018. The code fragments shown below are excerpts of valid .mly files.

next