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:
\x -> f x (g x) And here’s its categorical rendering, just to [...]
A while back, Edward Kmett wrote a library called reflection, based on a 2004 paper by Oleg Kiselyov and Chung-chieh Shan that describes a neat trick for reifying data into types (here the word “reify” can be understood as turning a value into something that can be referenced at the type level). There was also an article written by [...]
One of the most common structures used in programming are key/value maps, also called hash maps, dictionaries, association lists, or simply functions. These maps generally provide a way to add new values, lookup keys, iterate over the collection, etc. Yet in Coq, even though this facility exists in the standard library under the module FMap, it can be quite [...]