Back in 2006, Dan Piponi wrote about Löb’s theorem and how it can be implemented elegantly in Haskell and used to build a spreadsheet calculator from a very minimal core. Further notes on the Haskell wiki abstract his loeb function further, and offer a bit more insight into how it operates. A few years later, as I was working [...]

I first encountered the “recursion schemes” idea in Haskell while attending an excellent presentation given by Tim Williams in 2013. His ideas in that talk made a deep impression on me, and I resolved to find a way to prove the potential he promised in my own work. Now, the basic idea of recursion schemes goes back at least as [...]

Lately I’ve been working again on my Category Theory formalization in Coq, and just now proved, in a completely general setting, the following statement: Monads are monoid (objects) in the (monoidal) category of endofunctors (which is monoidal with respect to functor composition). The proof, using no axioms, is here. Now, just how much category theory was needed to establish this [...]

I gave a talk a couple of weeks ago at BayHac 2017 on “Putting lenses to work”, to show in a practical context how we use lenses at my workplace. I specifically avoided any theory about lenses, or the complex types, or the many operators, to show that at its core, lens is a truly invaluable library: The video is [...]

Conal Elliott has been working for several years now on using categories, specifically cartesian closed category, as a way to abstract Haskell functions at compile-time, so you can render the resulting “categorical term” into other categories. Here’s an example Haskell function: