Mainly writing about programming
Posted on April 28, 2026 Tags: Haskell One of my favourite Haskell papers is McIlroy’s wonderful “Power Series, Power Serious” ( 1999 ) . The paper is about power series , which are a type of infinite sums that behave like (infinite) polynomials. For example, cos \cos can be represented by the following power series: cos ( x ) = 1 − x 2 2 ! + x 4 4 ! − x 6 6 ! + x 8 8 ! − x 10 10 ! + ⋯ \cos(x) = 1…
Posted on March 3, 2026 Tags: Haskell This post is about a simple algebraic structure that I have found useful for algorithms that involve searching or sorting based on some ordered weight. I used it a bit in a pair of papers on graph search ( 2021 ; 2025 ) , and more recently I used it to implement a version of the Phases type ( Easterly 2019 ) that supported arbitrary keys, inspired by some work…
Posted on November 18, 2025 Tags: New paper: “Hyperfunctions: Communicating Continuations”, by myself and Nicolas Wu , will be published at POPL 2026 . The preprint is available here . The work contained in the paper started with a post on this blog in 2021 . I had read a paper by Launchbury, Krstić, and Sauerwein ( 2000 ) and I recognised that their hyperfunction construction was quite similar to…
Posted on November 8, 2024 Tags: Agda New paper: “Formalising Graph Algorithms with Coinduction”, by myself and Nicolas Wu , will be published at POPL 2025 . The preprint is available here . The talk is here . The paper is about representing graphs (especially in functional languages). We argue in the paper that graphs are naturally coinductive , rather than inductive, and that many of the…
Posted on November 7, 2023 Tags: Agda New paper: “Algebraic Effects Meet Hoare Logic in Cubical Agda”, by myself, Zhixuan Yang , and Nicolas Wu , will be published at POPL 2024. The preprint is available here .
Posted on October 17, 2022 Tags: Haskell Here’s a cool trick: minimum :: Ord a => [a] -> a minimum = head . sort This is 𝒪 ( n ) \mathcal{O}(n) in Haskell, not 𝒪 ( n log n ) \mathcal{O}(n \log n) as you might expect. And this isn’t because Haskell is using some weird linear-time sorting algorithm; indeed, the following is 𝒪 ( n log n ) \mathcal{O}(n \log n) : maximum :: Ord a => [a] -> a…
Posted on May 3, 2022 Tags: Agda I haven’t written much on this blog recently: since starting a PhD all of my writing output has gone towards paper drafts and similar things. Recently, though, I’ve been thinking about streams, monoids, and comonads and I haven’t managed to wrangle those thoughts into something coherent enough for a paper. This blog post is a collection of those (pretty…
Posted on August 29, 2021 Tags: Haskell I have packaged up the more interesting bits from the Algebras for Weighted Search paper and put it up on hackage. You can see it here . It contains the HeapT monad, the Monus class, and an implementation of Dijkstra’s algorithm, the Viterbi algorithm, and probabilistic parsing. Check it out!
Posted on June 21, 2021 Tags: Haskell , Agda The paper “Algebras for Weighted Search” has just been accepted unconditionally to ICFP. I wrote it with my supervisor, Nicolas Wu , and it covers a lot of the topics I’ve written about on this blog (including hyperfunctions and breadth-first traversals). The preprint is available here .
Posted on March 14, 2021 Tags: Haskell Check out this type: newtype a -&> b = Hyp { invoke :: (b -&> a) -> b } This a hyperfunction ( J. Launchbury, Krstic, and Sauerwein 2013 ; 2000 ; 2000 ) , and I think it’s one of the weirdest and most interesting newtypes you can write in Haskell. The first thing to notice is that the recursion pattern is weird. For a type to refer to itself recursively on…
Posted on January 4, 2021 Tags: Agda The final version of my master’s thesis got approved recently so I thought I’d post it here for people who might be interested. Here’s the university record . Here’s the pdf . And all of the theorems in the thesis have been formalised in Agda. The code is organised to follow the structure of the pdf here . The title of the thesis is “Finiteness in Cubical Type…
Posted on December 27, 2020 Tags: Haskell The Cayley monoid is well-known in Haskell (difference lists, for instance, are a specific instance of the Cayley monoid), because it gives us O ( 1 ) O(1) <> . What’s less well known is that it’s also important in dependently typed programming, because it gives us definitional associativity. In other words, the type x . (y . z) is definitionally equal to…
Posted on December 14, 2020 Tags: Agda , Haskell Consider the following puzzle: Given a list of n n labels, list all the trees with those labels in order. For instance, given the labels [1,2,3,4], the answer (for binary trees) is the following: ┌1 ┌1 ┌1 ┌1 ┌1 ┤ ┤ ┌┤ ┌┤ ┌┤ │┌2 │ ┌2 ││┌2 │└2 │└2 └┤ │┌┤ │└┤ ┤ ┌┤ │┌3 ││└3 │ └3 │┌3 │└3 └┤ └┤ ┤ └┤ ┤ └4 └4 └4 └4 └4 This problem (the “enumeration”…
Posted on November 23, 2020 Part 10 of a 10-part series on Breadth-First Traversals Tags: Haskell We pick up the story again at the question of a breadth-first (Applicative) traversal of a rose tree ( Gibbons 2015 ) . In the last post, I finally came up with an implementation I was happy with: data Tree a = a :& [ Tree a] bft :: Applicative f => (a -> f b) -> Tree a -> f ( Tree b) bft f (x :& xs)…
Posted on November 18, 2020 Tags: Agda Update 2022-11-12 The best approach to this now is probably to use this action, specifically set up for Agda: github.com/wenkokke/setup-agda I’ll leave the rest of this post here, but bear in mind the advice is outdated. Recently travis-ci.org announced that they were closing down, and moving to travis-ci.com. For people who use the service, this basically…
Posted on October 17, 2020 Tags: Combinators There are a bunch of “minimal” computational models out there: Turing machines, lambda calculus, PowerPoint ( Wildenhain 2017 ) , etc. These are radically simple languages which are nonetheless Turing complete, so theoretically “as powerful” as each other. Of those, lambda calculus is my favourite to actually write programs in: it’s the one which is…
Posted on August 22, 2020 Tags: Haskell It’s been a while since I last wrote a post (I’ve been busy with my Master’s thesis, which is nearly done), so I thought I would quickly throw out some fun snippets of Haskell I had reason to write over the past couple of weeks. Zipping With Folds For some reason, until recently I had been under the impression that it was impossible to fuse zips efficiently.…
Posted on May 19, 2020 Tags: Haskell A week or so ago I gave a presentation on purely functional data structures as part of an interview 1 . Here are the slides: https://doisinkidney.com/pdfs/purely-functional-data-structures-slides.pdf The presentation is meant to be about 45 minutes long, and it’s aimed at end of first year computer science students who have done some Haskell and know a little…
Posted on May 2, 2020 Part 2 of a 2-part series on Random Access Lists Tags: Haskell , Agda Imports and Pragmas {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE MultiParamTypeClasses #-}…
Posted on February 20, 2020 Part 9 of a 10-part series on Breadth-First Traversals Tags: Haskell This post will be quite light on details: I’m trying to gather up all of the material in this series to be a chapter in my Master’s thesis, so I’m going to leave the heavy-duty explanations and theory for that. Once finished I will probably do a short write up on this blog. That said, the reason I’m…
Posted on February 15, 2020 Tags: Haskell Just a short one again today! There’s an excellent talk by Kenneth Foner at Compose from 2016 which goes through a paper by Danvy and Goldberg ( 2005 ) called “There and Back Again” (or TABA). You should watch the talk and read the paper if you’re in any way excited by the weird and wonderful algorithms we use in functional languages to do simple things…
Posted on January 29, 2020 Part 8 of a 10-part series on Breadth-First Traversals Tags: Agda , Haskell Imports {-# OPTIONS --cubical --sized-types #-} module Post where open import ../code/terminating-tricky-traversals/Post.Prelude Just a short one today. I’m going to look at a couple of algorithms for breadth-first traversals with complex termination proofs. Breadth-First Graph Traversal In a…
Posted on December 14, 2019 Tags: Haskell , Agda In dependently typed languages, it’s often important to figure out a good “low-level” representation for some concept. Here’s a common low-level representation of the natural numbers: data Nat = Z | S Nat For “real” applications, of course, these numbers are offensively inefficient, in terms of both space and time. But that’s not what I’m after…
Posted on November 15, 2019 Tags: Agda Imports etc. {-# OPTIONS --safe --without-K #-} module Post where open import Data.Fin using ( Fin ; suc ; zero ; _≟_ ) open import Data.Nat using ( ℕ ; suc ; zero ; _+_ ; compare ; equal ; greater ; less ) open import Data.Nat.Properties using ( +-comm ) open import Data.Bool using ( not ; T ) open import Relation.Nullary using ( yes ; no ; does ; ¬_ ) open…
Posted on November 2, 2019 Part 1 of a 2-part series on Random Access Lists Tags: Agda “Heterogeneous Random-Access Lists” by Wouter Swierstra ( 2019 ) describes how to write a simple binary random-access list ( Okasaki 1995 ) to use as a heterogeneous tuple. If you haven’t tried to implement the data structure described in the paper before, you might not realise the just how elegant the…
Posted on October 2, 2019 Tags: Haskell Update 5/10/2019: check the bottom of this post for some links to comments and discussion. Beginners to Haskell are often confused as to what’s so great about the language. Much of the proselytizing online focuses on pretty abstract (and often poorly defined) concepts like “purity”, “strong types”, and (god forbid) “monads”. These things are difficult to…
Posted on July 14, 2019 Tags: Agda I recently finished my undergrad degree in UCC . I’m putting my final-year project up here for reference purposes. Here is the pdf. And here’s a bibtext entry: @thesis { kidney_automatically_2019 , address = {Cork, Ireland}, type = {Bachelor thesis}, title = {Automatically and {Efficiently} {Illustrating} {Polynomial} {Equalities} in {Agda}}, url =…
Posted on June 4, 2019 Tags: Python This post is a write-up of a solution to part of a programming puzzle I did yesterday. It’s a little different than the usual “solution + theory” approach, though: I’m going to talk about the actual steps you’d need to take to get to the solution (i.e. what to google, what intermediate code looks like, etc.). Often write ups like this are presented as finished…
Posted on May 28, 2019 Part 7 of a 10-part series on Breadth-First Traversals Tags: Haskell The Story so Far Currently, we have several different ways to enumerate a tree in breadth-first order. The typical solution (which is the usual recommended approach in imperative programming as well) uses a queue , as described by Okasaki ( 2000 ) . If we take the simplest possible queue (a list), we get a…
Posted on May 14, 2019 Part 6 of a 10-part series on Breadth-First Traversals Tags: Haskell Fusion I was looking again at one of my implementations of breadth-first traversals: bfe :: Tree a -> [a] bfe r = f r b [] where f ( Node x xs) fw bw = x : fw (xs : bw) b [] = [] b qs = foldl ( foldr f) b qs [] And I was wondering if I could fuse away the intermediate list. On the following line: f ( Node x…
Posted on May 11, 2019 Tags: Concatenative , Haskell This post demonstrates a simple encoding of a (typed) concatenative language in Haskell. Point-free style is one of the distinctive markers of functional programming languages. Want to sum a list? That’s as easy as: sum = foldr ( + ) 0 Now I want to sum every number after adding one to it. sumSuccs = foldr ( + ) 0 . map (( + ) 1 ) One more step…
Posted on May 8, 2019 Tags: Haskell This post is a collection of some of the tricks I’ve learned for manipulating lists in Haskell. Each one starts with a puzzle: you should try the puzzle yourself before seeing the solution! The Tortoise and the Hare How can you split a list in half, in one pass, without taking its length? This first one is a relatively well-known trick, but it occasionally comes…
Posted on April 20, 2019 Tags: Agda Just some silly examples of how to get a nice list syntax with mixfix operators in Agda. Intro and Imports {-# OPTIONS --without-K --safe #-} module ListSyntax where open import Data.List as List using ( List ; _∷_ ; [] ) open import Data.Product open import Level using ( _⊔_ ; Level ) open import Data.Nat using ( ℕ ; _+_ ; suc ; zero ) open import Function…
Posted on April 17, 2019 Tags: Agda , Probability Cubical Agda has just come out, and I’ve been playing around with it for a bit. There’s a bunch of info out there on the theory of cubical types, and Homotopy Type Theory more generally (cubical type theory is kind of like an “implementation” of Homotopy type theory), but I wanted to make a post demonstrating cubical Agda in practice, and one of…
Posted on March 24, 2019 Tags: Haskell , Agda A naive—and wrong—way to shuffle a list is to assign each element in the list a random number, and then sort it. It might not be immediately obvious why: Kiselyov ( 2002 ) has a good explanation as to the problem. One way to think about it is like this: choosing n n random numbers each in the range [ 0 , n ) [0,n) has n n n^n possible outcomes, whereas…
Posted on March 21, 2019 Part 1 of a 1-part series on Binary Numbers Tags: Agda , Haskell Number Representations When working with numbers in Agda, we usually use the following definition: data N = Z | S N deriving ( Eq , Ord ) instance Num N where Z + n = n S n + m = S (n + m) Z * m = Z S n * m = m + n * m data ℕ : Set where zero : ℕ suc : ℕ → ℕ _ + _ : ℕ → ℕ → ℕ zero + y = y suc x + y = suc ( x…
Posted on March 14, 2019 Part 2 of a 2-part series on Agda Tips Tags: Agda Literate Agda For including Agda code in LaTeX files, Agda’s built-in literate programming support is a great tool. It typesets code well, and ensures that it typechecks which can help avoid typos. Embedding Agda Code in LaTeX I write the LaTeX document in one file, and the Agda code in another .lagda file. Using the…
Posted on February 25, 2019 Tags: Agda This Post is Available With Clickable Code Here This whole post is written with clickable identifiers and ascii art at the above link. I also provide the normal version below in case there are any problems rendering. As I have talked about previously , a large class of divide-and conquer algorithms rely on “good” partitioning for the divide step. If you then…
Posted on January 25, 2019 Tags: Agda I’m finally at the point where I feel like I can make the project I’ve been working on for the past few months public: A Ring Solver for Agda . The focus of the project is ergonomics and ease-of-use: hopefully the interface to the solver is simpler and more friendly than the one that’s already there. It can do step-by-step solutions (like Wolfram Alpha). It’s…
Posted on January 15, 2019 Part 3 of a 3-part series on Balanced Folds Tags: Haskell When we started the series, we wanted to find a “better” fold: one that was more balanced than either foldl or foldr (in its placement of parentheses). Both of these are about as unbalanced as you can get: >>> foldr ( + ) 0 [ 1 , 2 , 3 ] 1 + ( 2 + ( 3 + 0 )) >>> foldl ( + ) 0 [ 1 , 2 , 3 ] (( 0 + 1 ) + 2 ) + 3 The…
Posted on December 30, 2018 Tags: Haskell For a bunch of algorithms it’s handy to get a quick-and-dirty visualization of a tree. Data.Tree has a tree-drawing function, but its output is too noisy for my taste, and so doesn’t really illustrate the underlying structure in a way I find helpful. This version uses the unicode box-drawing characters to give an output that’s midway between what is…
Posted on December 29, 2018 Tags: Haskell This function is now available on hackage . There’s a family of functions in Control.Applicative which follow the pattern liftA2 , liftA3 , etc. Using some tricks from Richard Eisenberg’s thesis we can write them all at once. {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-}…
Posted on December 21, 2018 Part 2 of a 3-part series on Balanced Folds Tags: Haskell , Agda Previously I tried to figure out a way to fold lists in a more balanced way. Usually, when folding lists, you’ve got two choices for your folds, both of which are extremely unbalanced in one direction or another. Jon Fairbairn wrote a more balanced version, which looked something like this: treeFold :: (a…
Posted on December 18, 2018 Part 5 of a 10-part series on Breadth-First Traversals Tags: Haskell Today, I’m going to look at extending the previous breadth-first traversal algorithms to arbitrary graphs (rather than just trees). Graphs with cycles are notoriously cumbersome in functional languages, so this actually proves to be a little trickier than I thought it would be. First, a quick recap. 3…
Posted on December 14, 2018 Part 2 of a 2-part series on Prime Sieves Tags: Agda Prime numbers in Agda are slow . First, they’re Peano-based, so a huge chunk of optimizations we might make in other languages are out of the window. Second, we really often want to prove that they’re prime, so the generation code has to carry verification logic with it (I won’t do that today, though). And third, as…
Posted on November 20, 2018 Tags: Haskell , Agda One of the favorite pastimes of both Haskell and Agda programmers alike is verifying data structures. Among my favorite examples are Red-Black trees ( Might 2015 ; Weirich 2014 , verified for balance) , perfect binary trees ( Hinze 1999 ) , square matrices ( Okasaki 1999a ) , search trees ( McBride 2014 , verified for balance and order) , and…
Posted on November 10, 2018 Part 1 of a 2-part series on Prime Sieves Tags: Haskell A few days ago, the Computerphile YouTube channel put up a video about infinite lists in Haskell ( Haran 2018 ) . It’s pretty basic, but finishes up with a definition of an infinite list of prime numbers. The definition was something like this: primes = sieve [ 2 .. ] sieve (p : ps) = p : sieve [ x | x <- ps, mod x…
Posted on October 16, 2018 Part 1 of a 1-part series on Total Combinatorics Tags: Agda , Haskell Here’s a quick puzzle: from a finite alphabet, produce an infinite list of infinite strings, each of them unique. It’s not a super hard problem, but here are some examples of what you might get. Given the alphabet of 0 and 1 , for instance, you could produce the following: 0000000... 1000000...…
Posted on September 20, 2018 Part 1 of a 2-part series on Agda Tips Tags: Agda I’m in the middle of quite a large Agda project at the moment, and I’ve picked up a few tips and tricks in the past few weeks. I’d imagine a lot of these are quite obvious once you get to grips with Agda, so I’m writing them down before I forget that they were once confusing stumbling blocks. Hopefully this helps other…
Posted on July 30, 2018 Tags: Haskell , Agda I’ve been writing a lot of Agda recently, and had the occasion to write a Fenwick tree that did some rebalancing. I went with AVL -style rebalancing (rather than red-black or trees of bounded balance ). I’d written pretty full implementations of the other two before, and the Agda standard library ( Danielsson 2018 ) has an implementation already that I…