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.
Recently I was playing around with the core types in the
conduit library (attempting to change leftovers so you could only unget values you had read), when I stumbled across a formulation of those types that lead to some interesting simplifications.