This repository is inspired by The Evolution of a Haskell Programmer, which was itself inspired by the folklore joke The Evolution of a Programmer.
Our patient zero is a Haskell98-compliant implementation of a typechecker for the simply-typed λ-calculus. We then improve (and branch upon) variants of this base program.
Caution: bugs have voluntarily been inserted in the various
implementations, unless typing prevents it. In principle, only the
HEAD of master is bug-free, because the type system leaves us no
choice.
This repository has been tested with Agda 2.5.4.1 and the Agda standard library 0.17.
Contributions are more than welcome. In particular, we welcome exploratory branches (even if unfruitful) and further bike-shedding of existing branches.
Since the value of this repository lies more in its genotype than the final product, we are keen on keeping a clean history, even if it means rewriting history and push-forcing changes to this repository.
This project has been initiated by Pierre-Évariste Dagand as part of MPRI-2.4 course material. It contains a significant amount of McBride-ism (namely: the mantras of bidirectional typing, canonical & elimination forms, strongly typed term representation, dissection, etc.) and a pinch of the Agda prelude.
