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 give the flavor of the idea: [...]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 Austin [...]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 difficult [...]This is a tutorial on how to use the

`pcase`

macro in modern flavors of GNU Emacs.
[...]