Free Structures Aren't Just

Free structures are a popular idea in Haskell when speaking about constructions like the “free monad” or notions like “lists are free monoids”. This terminology can be misleading, however. Free structures aren’t just “free”, they have to be “free” with respect to something.

Stupid right/left folding tricks

There's a folk-wisdom trick for converting a right fold on lists into a left fold. This may not appear to be terrifically useful at first but if you look a bit beneath the surface then it reveals a practical tool in any functional programmer's toolbelt.

There is no royal road to mathematics

There is no royal road to mathematics, but instead an enormous shining underground city. Here, I hope to give a little tour to its districts and customs for the new traveler.

Papers We Love BOS No. 2, "Foundations of Logic and Functional Programming via Martin-Löf"

I gave a talk for Papers We Love, Boston on the 18th where I discussed Martin-Löf type theory from a historical and programming context. The goal was to motivate and inspire reading the (notably long) 1983 Martin-Löf lectures On the Meanings of the Logical Constants and the Justifications of the Logical Laws. The video was just posted and the slides are available here.

Why the Cross Product Is What It Is

When studying sets in mathematics you learn a number of seemingly arbitrary constructions like, for instance, the so-called Cartesian Product. It's natural to ask why these constructions are so privileged... and while the answer is not exactly straightforward, it is very revealing! (An answer to a question posed on Quora.)

JSON is not Object Notation

This is a silly nit to pick, but here goes. JSON doesn't denote objects, it denotes finite, initial state which is exactly why it's useful. So, JSON isn't an "object notation", only JavaScript itself is.

Typing Transducers (as Kleisli arrows)

There's been a little flurry of activity around analyzing Clojure's upcoming transducers using Haskell types. This post outlines an isomorphism between one such representation and list "binding functions" a -> [b]. This suggests that flatMap is central to the idea of transduction.

Some Points About Type Safety

The technical concept "type safety", and even the underlying technical concept "type", is often misunderstood due to being conflated with marketing terms or given undue technical weight. This post enumerates some useful intuition pumps for better understanding, talking about, and consuming material related to type safety.

Codata Diagonalization

Modern programming has something that was often talked about but never formalized throughout much of modern mathematics, codata. This post sketches a constructive proof of diagonalization using codata in Haskell notation.

Immutable Enumeration in Swift

Enumeration of container types is a very important programming technique. In immutable languages, one mechanism for this is to have a generic "left view" interface. This interface corresponds exactly to Stream codata and Swift is powerful enough to (almost) implement all of the above directly.