Posts about programming:

An Example of Defunctionalisation in Rust

06 February 2021

I’m an experienced Haskell programmer, and I’ve been writing a lot of Rust lately. I recently ran into a little trouble when porting a simple function from Haskell to Rust. This article is a short description of my journey.

Docker Cleanup Commands

07 November 2020

I’ve Googled this one too many times, so I’m writing it here for future reference.

Statically Sized Higher-kinded Polymorphism

07 July 2020

Memory-sensitive languages like C++ and Rust use compile-time information to calculate sizes of datatypes. These sizes are used to inform alignment, allocation, and calling conventions in ways that improve runtime performance. Modern languages in this setting support generic types, but so far these languages only allow parameterisation over types, not type constructors. In this article I describe how to enable parameterisation over arbitrary type constructs, while still retaining compile-time calculation of datatype sizes.

Lambdas are Codatatypes

01 July 2019

I was first clued into this a while ago by a comment on Bob Harper’s blog that “exponentials are coinductive”, but it only really clicked for me today. Let’s get into it.

Configuring Agda's standard library on NixOS

17 May 2019

I’ve been using Agda on NixOS for a while (mostly via agda-mode in Emacs), but I remember it was a bit difficult to get going the very first time. Hopefully this becomes a searchable reference to getting it all set up quickly.

On Programming Language Design

21 November 2018

In his propositions as types talk, Philip Wadler contrasts programming languages that have been ‘invented’ with those that have been ‘discovered’. “And you can tell!” he exclaims, receiving giggles from the audience. Regardless of how you feel about mathematical platonism, I think Phil is pointing at a meaningful difference in the way certain ideas arise.

Turning bottom-up into top-down with Reverse State

13 June 2018

I love bound - it makes De Bruijn indices mindlessly easy. I also love Plated for all sorts of whole-program transformations. I think they’re two indispensible tools for working with programming languages. Unfortunately, they’re not compatible.

Comonad Transformers in the Wild

25 February 2018

A certain algorithmic puzzle website has a problem that goes like this…

Continuations From the Ground Up

06 June 2017

It’s difficult to learn functional programming without hearing about continuations. Often they’re mentioned while talking about boosting the performance of pure functional code, sometimes there’s talk of control flow, and occasionally with ‘time-travel’ thrown in there to make it all seem more obscure. It’s all true, but let’s start from the beginning.

Why LINQ (well, C#) is Broken

24 October 2016

LINQ is a system that provides a flexible query interface for .NET languages. It allows a user to write queries over arbitrary data using an in-built SQL-like syntax. This syntactic sugar is mapped to method calls at compile time, so any data structure that implements the correct methods can be used with LINQ.

Search and Replace in Multiple Files

25 July 2015

$ sed -i "s/pattern/replacement/g" FILES

The Programming Thought Process: Fizzbuzz

04 March 2015

With so many programming languages and frameworks at our disposal, it is too easy to believe that knowledge of many tools is the defining characteristic of a good programmer. However, many experienced programmers will assert that it isn’t the languages you know, but your ability to solve problems that defines you as a programmer.

A Practical Introduction to Monad Transformers

01 February 2015

Monad transformers combine the functionality of two monads into one. They are often used as a way to “flatten” nested monads, but are also used to enable interactions between monads that, when used seperately, would be incredibly difficult to implement.