One of my own old blog posts. Incrementally refactors normal Enumerator and Observer interfaces (in the object-oriented sense) using algebraic reasoning, gradually bringing them closer and closer to realistic networking protocols, and quite quickly arriving at a place where the networking concepts of “acknowledgement of messages” and “flow control to avoid overwhelming a receiver” fall out for free.

A short tutorial on algebraic data types, useful tools for reasoning about and refactoring data structures:

In what sense are data types algebraic? […] Isn’t this all just a bunch of general abstract nonsense? We’ll investigate these questions, and perhaps demystify this important concept of functional languages.

An example of how these ideas can help can be seen in my old blog post on The Origins of Flow Control and Acknowledgements.

(Aside: this post’s link seems to be to a rescued copy of the text, which was originally at http://blog.lab49.com/archives/3011.)

A recent ML-family language design:

1SubML is an experimental ML-like programming language with a unified module and value language, structural subtyping, global type inference, higher rank polymorphic types, existential types, higher kinded types (no partial application), recursive types, worst-case polynomial time type checking and much more.

The importance of (and tricks for) doing proofs about code you’re writing as you write it:

This is a brief write-up of a trick I learned that helps me write code faster and more accurately. I say “trick”, but it’s really something I started to do without noticing as I moved further into my career.

When you’re working on something difficult, sketch a proof in your head as you go that your code will actually do what you want it to do. A simple idea, but easier said than done: doing this “online” without interrupting your flow takes a lot of practice. But once you get really good at it, you’ll find that a surprising amount of the time your code will work on the first or second try. It feels a little magical.

(via John Regehr)

An elegant example of FP for the FP portion of my PL course:

A simple, useful, plain-text variant of Donald Knuth’s paragraph-filling algorithm can be expressed as a fold. This algorithm runs in time linear to the length of its input and usually produces better results than the classic greedy text-flow algorithm.

Makes explicit the connection between the Visitor design pattern and sum types (a.k.a. tagged unions / algebraic data types).

Development of incremental improvements to a pure-functional quicksort implementation, eliminating multiple passes over the input and unnecessary append operations by introducing accumulators.