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. [...]
The following article is just a few notes on the nature of the Free monad. [...]
This article assumes familiarity with monads and monad transformers. If you’ve never had an occasion to use lift yet, you may want to come back to it later. The Problem What is the problem that monad-control aims to solve? To answer that, let’s back up a bit. We know that a monad represents some kind of “computational context”. The question [...]