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 [...]