A few years ago I was very impressed for learning the Boehm-Berarducci encoding, which is a way for encoding Algebraic Data Types (ADTs) into a kind of lambda calculus that is well typed called System F. The first thing I asked myself was in which la ... read more →

I have on and off again tried to use mypy to type check my python code, but some shortcomings of Python's type annotation system really get in the way. This came now because I needed to write code involving trees that had to change the types of value ... read more →