Functor, applicative, and monad
August 31, 2019
Functor, applicative, and monad are useful abstractions. They're also not so hard to understand!
Five wonderful angels: A love letter to K-On
July 24, 2019
K-On is an unassuming masterpiece by Kyoto Animation
Learning Agda by implementing matrix multiplication
April 14, 2019
In which I implement type-safe matrix multiplication in Agda
Why I love type theory
February 8, 2019
Discover the connection between type theory and algebra, logic, and category theory.