Implementation of the reversible programming language Π in Haskell, 2024 SDU bachelor project of Frederik List.

It is easiest to run the program in an interactive Haskell interpreter like ghci. This implementation was developed and tested on GHC 9.0.2 (with packages base-4.15.1.0, mtl-2.2.2, and containers-0.6.4.1).

There are various parts of the implementation split into multiple files:

• Examples.hs contains all of the examples in the article and more. It imports most of the other relevant modules, so just loading this module should be sufficient.
• Pi.hs defines the syntax of Π as ordinary algebraic datatypes. This includes combinators, types, and values as well as several helper methods to handle them.
• Infer.hs contains the code for type inference of Π programs as well as an evaluator monad for catching type errors.
• Eval.hs implements the interpreter for Π values.
• Norm.hs contains the code for synthesis, reification, and normalization of Π programs.
• Pretty.hs is a small, partial library for pretty-printing (mostly Π terms).
• Symantics.hs contains the typed tagless-final implementation of Π. Note that normalization is not implemented in the tagless-final style as I suspect quite a few unfavorable GHC extensions are required to simulate dependent types.

All of the examples are prefixed with ex_. You should load Examples.hs in an interactive Haskell interpreter (ghci Examples.hs), type ex_, and hit Tab to see available examples. When you run an example, the results are pretty-printed to your screen.

The tagless-final examples are best understood by reading the source code.