Listing buffers by tab using consult and bufferlo

I've gotten into the habit of using tabs, via tab-bar, to organise my buffers when I have multiple projects open at once. Each project has its own tab. There's nothing fancy here (yet), I simply open a new tab manually before opening a new project.

A while ago I added bufferlo to my config to help with getting consult-buffer to organise buffers (somewhat) by tab. I copied the configuration from the bufferlo README and started using it. It took me a little while to notice that the behaviour wasn't quite what I wanted. It seemed like one buffer "leaked" from another tab.

In the image above all files in ~/.emacs.d should be listed under Other Buffers, but one has been brought over into the tab for the Sider project.

After a bit of experimenting I realised that

1. the buffer that leaks is the one I'm in when creating the new tab, and
2. my function for creating a new tab doesn't work the way I thought.

My function for creating a new tab looked like this

(lambda ()
  (interactive)
  (tab-new)
  (dashboard-open))

and it turns out that tab-new shows the current buffer in the new tab which in turn caused bufferlo to associate it to the wrong tab. From what I can see there's no way to tell tab-new to open a specific buffer in the newly created tab. I tried the following

(lambda ()
  (interactive)
  (with-current-buffer dashboard-buffer-name
    (tab-new)))

hoping that the dashboard would open in the new tab. It didn't, it was still the active buffer that popped up in the new tab.

In the end I resorted to use bufferlo-remove to simply remove the current buffer from the new tab.

(lambda ()
  (interactive)
  (tab-new)
  (bufferlo-remove (current-buffer))
  (dashboard-open))

No more leakage and consult-buffer works like I wanted it to.

Tags: emacs

September 16, 2025 06:29 AM

Topological Sort: Managing Mutable Structures in Haskell

Welcome back to our Rust vs. Haskell comparison series, featuring some of the most common LeetCode questions. We’ve done a couple graph problems the last two weeks, involving DFS and BFS.

Today we’ll do a graph problem involving a slightly more complicated algorithm. We’ll also use a couple data structures we haven’t seen in this series yet, and we’ll see how tricky it can get to have multiple mutable structures in a Haskell algorithm.

To learn all the details of managing your data structures in Haskell, check out Solve.hs, our problem solving course. You’ll learn all the key APIs, important algorithms, and you’ll get a lot of practice with LeetCode style questions!

The Problem

Today’s problem is called Course Schedule. We are given a number of courses, and a list of prerequisites among those courses. For a prerequisite pair (A,B), we cannot take Course A until we have taken Course B. Our job is to determine, in a sense, if the prerequisite list is well-defined. We want to see whether or not the list would actually allow us to take all the courses.

As an example, suppose we had these inputs:

Number Courses: 4
Prerequisites: [(2, 0), (1,0), (3,1), (3,2)]

This is a well defined set of courses. In order to take courses 1 and 2, we must take course 0. Then in order to take course 3, we have to take courses 1 and 2. So if we have the ordering 0->1->2->3, we can take all the courses. So we would return True.

However, if we were to add (1,3) there, we would not be able to take all the courses. We could take courses 0 and 2, but then we would be stuck because 1 and 3 have a mutual dependency. So we would return False with this list.

We are guaranteed that the course indices in the prerequisites list are in the range [0, numCourses - 1]. We are also guaranteed that all prerequisites are unique.

The Algorithm

For our algorithm, we will image these courses as living in a directed graph. If course A is a prerequisite of Course B, there should be a directed edge from A to B. This problem essentially boils down to determining if this graph has a cycle or not.

There are many ways to approach this, including relying on DFS or BFS as we discussed in the past two weeks! However, to introduce a new idea, we’ll solve this problem using the idea of topological sorting.

We can think of nodes as having “in degrees”. The “in degree” of a node is the number of directed edges coming into it. We are particularly concerned with nodes that have an in degree of 0. These are courses with no prerequisites, which we can take immediately.

Each time we “take” a course, we can increment a count of the courses we’ve taken, and then we can “remove” that node from the graph by decrementing the in degrees of all nodes that it is pointing to. If any of these nodes have their in degrees drop to 0 as a result of this, we can then add them to a queue of “0 degree nodes”.

If, once the queue is exhausted, we’ve taken every course, then we have proven that we can satisfy all the requirements! If not, then there must be a cycle preventing some nodes from ever having in-degree 0.

Rust Solution

We’ll start with a Rust solution. We need to manage a few different structures in this problem. The first two will be vectors giving us information about each course. We want to know the current “in degree” as well as having a list of the courses “unlocked” by each course.

Each “prerequisite” pair gives the unlocked course first, and then the prerequisite course. We’ll call these “post” and “pre”, respectively. We increase the in-degree of “post” and add “post” to the list of courses unlocked by “pre”:

pub fn can_finish(num_courses: i32, prerequisites: Vec<Vec<i32>>) -> bool {
    // More convenient to use usize
    let n = num_courses as usize;

    let mut inDegrees = Vec::with_capacity(n);
    inDegrees.resize(n, 0);

    // Maps from “pre” course to “post” course
    let mut unlocks: Vec<Vec<usize>> = Vec::with_capacity(n);
    unlocks.resize(n, Vec::new());

    for req in prerequisites {
        let post = req[0] as usize;
        let pre = req[1] as usize;
        inDegrees[post] += 1;
        unlocks[pre].push(post);
    }
    ...
}

Now we need to make a queue of 0-degree nodes. This uses VecDeque from last time. We’ll go through the initial in-degrees list and add all the nodes that are already 0. Then we’ll set up our loop to pop the front element until empty:

pub fn can_finish(num_courses: i32, prerequisites: Vec<Vec<i32>>) -> bool {
    let n = num_courses as usize;

    ...

    // Make a queue of 0 degree
    let mut queue: VecDeque<usize> = VecDeque::new();
    for i in 0..(num_courses as usize) {
        if inDegrees[i] == 0 {
            queue.push_back(i);
        }
    }

    let mut numSatisfied = 0;
    while let Some(course) = queue.pop_front() {
        ...
    }
    return numSatisfied == num_courses;
}

All we have to do now is process the course at the top of the queue each time now. We always increment the number of courses satisfied, since de-queuing a course indicates we are taking it. Then we loop through unlocks and decrement each of their in degrees. If reducing an in-degree takes it to 0, then we add this unlocked course to the back of the queue:

pub fn can_finish(num_courses: i32, prerequisites: Vec<Vec<i32>>) -> bool {
    let n = num_courses as usize;

    ...

    let mut numSatisfied = 0;
    while let Some(course) = queue.pop_front() {
        numSatisfied += 1;
        for post in &unlocks[course] {
            inDegrees[*post] -= 1;
            if (inDegrees[*post] == 0) {
                queue.push_back(*post);
            }
        }
    }
    return numSatisfied == num_courses;
}

This completes our solution! Here is the full Rust implementation:

pub fn can_finish(num_courses: i32, prerequisites: Vec<Vec<i32>>) -> bool {
    let n = num_courses as usize;
    // Make a vector with inDegree Count
    let mut inDegrees = Vec::with_capacity(n);
    inDegrees.resize(n, 0);

    // Make a vector of "unlocks"
    let mut unlocks: Vec<Vec<usize>> = Vec::with_capacity(n);
    unlocks.resize(n, Vec::new());

    for req in prerequisites {
        let post = req[0] as usize;
        let pre = req[1] as usize;
        inDegrees[post] += 1;
        unlocks[pre].push(post);
    }

    // Make a queue of 0 degree
    let mut queue: VecDeque<usize> = VecDeque::new();
    for i in 0..(num_courses as usize) {
        if inDegrees[i] == 0 {
            queue.push_back(i);
        }
    }

    let mut numSatisfied = 0;
    while let Some(course) = queue.pop_front() {
        numSatisfied += 1;
        for post in &unlocks[course] {
            inDegrees[*post] -= 1;
            if (inDegrees[*post] == 0) {
                queue.push_back(*post);
            }
        }
    }
    return numSatisfied == num_courses;
}

Haskell Solution

In Haskell, we can follow this same approach. However, this is a somewhat challenging algorithm for Haskell beginners, because there are a lot of data structure “modifications” occurring, and expressions in Haskell are immutable! So we’ll organize our solution into three different parts:

1. Initializing our structures
2. Writing loop modifiers
3. Writing the loop

This solution will introduce 2 data structures we haven’t used in this series so far. The IntMap and the Sequence (Seq), which we’ll use qualified like so:

import qualified Data.IntMap.Lazy as IM
import qualified Data.Sequence as Seq

The IntMap type works more or less exactly like a normal Map, with the same API. However, it assumes we have Int as our key type, which makes certain operations more efficient than a generic ordered map.

Then Seq is the best thing to use for a FIFO queue. We would have used this last week if we implemented BFS from scratch.

We’ll also make a few type alias, since we’ll be combining these structures and frequently using them in type signatures:

type DegCount = IM.IntMap Int
type CourseMaps = (DegCount, IM.IntMap [Int])
type CourseState = (Int, Seq.Seq Int, DegCount)

The setup to our problem is fairly simple. Our function takes the number of courses as an integer, and the prerequisites as a list of tuples. We’ll write a number of helper functions beneath this top level definition, but for additional clarity, we’ll show them independently as we write them.

canFinishCourses :: Int -> [(Int, Int)] -> Bool
canFinishCourses numCourses prereqs = ...

Initializing Our Structures

Recall that the first part of our Rust solution focused on populating 3 structures:

1. The list of in-degrees (per node)
2. The list of “unlocks” (per node)
3. The initial queue of 0-degree nodes

We use IntMaps for the first two (and use the alias DegCount for the first). These are easier to modify than vectors in Haskell. The other noteworthy fact is that we want to create these together (this is why we have the CourseMaps alias combining them). We process each prerequisite pair, updating both of these maps. This means we want to write a folding function like so:

processPrereq :: (Int, Int) -> CourseMaps -> CourseMaps

For this function, we want to define two more helpers. One that will make it easier to increment the key of a degree value, and one that will make it easy to append a new unlock for the other mapping.

incKey :: Int -> DegCount -> DegCount

appendUnlock :: Int -> Int -> IM.IntMap [Int] -> IM.IntMap [Int]

These two helpers are straightforward to implement. In each case, we check for the key existing. If it doesn’t exist, we insert the default value (either 1 or a singleton list). If it exists, we either increment the value for the degree, or we append the new unlocked course to the existing list.

incKey :: Int -> DegCount -> DegCount
incKey k mp = case IM.lookup k mp of
  Nothing -> IM.insert k 1 mp
  Just x -> IM.insert k (x + 1) mp

appendUnlock :: Int -> Int -> IM.IntMap [Int] -> IM.IntMap [Int]
appendUnlock pre post mp = case IM.lookup pre mp of
  Nothing -> IM.insert pre [post] mp
  Just prev -> IM.insert pre (post : prev) mp

Now it’s very tidy to implement our folding function, and apply it to get these initial values:

processPrereq :: (Int, Int) -> CourseMaps -> CourseMaps
processPrereq (post, pre) (inDegrees', unlocks') =
  (incKey post inDegrees', appendUnlock pre post unlocks')

Here’s where our function currently is then:

canFinishCourses :: Int -> [(Int, Int)] -> Bool
canFinishCourses numCourses prereqs =
  where
    (inDegrees, unlocks) = foldr processPrereq (IM.empty, IM.empty) prereqs

Now we want to build our initial queue as well. For this, we just want to loop through the possible course numbers, and add any that are not in the map for inDegrees (we never insert something with a value of 0).

canFinishCourses :: Int -> [(Int, Int)] -> Bool
canFinishCourses numCourses prereqs =
  where
    (inDegrees, unlocks) = foldr processPrereq (IM.empty, IM.empty) prereqs
    queue = Seq.fromList
      (filter (`IM.notMember` inDegrees) [0..numCourses-1])

Writing Loop Modifiers

Now we have to consider what structures are going to be part of our “loop” and how we’re going to modify them. The type alias CourseState already expresses our loop state. We want to track the number of courses satisfied so far, the queue of 0-degree nodes, and the remaining in-degree values.

The key modification is that we can reduce the in-degrees of remaining courses. When we do this, we want to know immediately if we reduced the in-degree to 0. So let’s write a function that decrements the value, except that it deletes the key entirely if it drops to 0. We’ll return a boolean indicating if the key no longer exists in the map after this process:

decKey :: Int -> DegCount -> (DegCount, Bool)
decKey key mp = case IM.lookup key mp of
  Nothing -> (mp, True)
  Just x -> if x <= 1
    then (IM.delete key mp, True)
    else (IM.insert key (x - 1) mp, False)

Now what’s the core function of the loop? When we “take” a course, we loop through its unlocks, reduce all their degrees, and track which ones are now 0. Since this is a loop that updates state (the remaining inDegrees), we want to write a folding function for it:

decDegree :: Int -> (DegCount, [Int]) -> (DegCount, [Int])

First we perform the decrement. Then if decKey returns True, we’ll add the course to our new0s list.

decDegree :: Int -> (DegCount, [Int]) -> (DegCount, [Int])
decDegree post (inDegrees', new0s) =
  let (inDegrees'', removed) = decKey post inDegrees'
  in  (inDegrees'', if removed then (post : new0s) else new0s)

Writing the Loop

With all these helpers at our disposal, we can finally write our core loop. Recall the 3 parts of our loop state: the number of courses taken so far, the queue of 0-degree courses, and the in-degree values. This loop should just return the number of courses completed:

canFinishCourses :: Int -> [(Int, Int)] -> Bool
canFinishCourses numCourses prereqs = ...
  where
    (inDegrees, unlocks) = foldr processPrereq (IM.empty, IM.empty) prereqs
    queue = Seq.fromList
      (filter (`IM.notMember` inDegrees) [0..numCourses-1])

    loop :: CourseState -> Int
    loop (numSatisfied, queue’, inDegrees’) = ...

If the queue is empty, we just return our accumulated number. While we’re at it, the final action is to simply compare this loop result to total number of courses to get our final result:

canFinishCourses :: Int -> [(Int, Int)] -> Bool
canFinishCourses numCourses prereqs = loop (0, queue, inDegrees) == numCourses
  where
    (inDegrees, unlocks) = foldr processPrereq (IM.empty, IM.empty) prereqs
    queue = Seq.fromList
      (filter (`IM.notMember` inDegrees) [0..numCourses-1])

    loop :: CourseState -> Int
    loop (numSatisfied, queue’, inDegrees’) = case Seq.viewl queue' of
      Seq.EmptyL -> numSatisfied
      (course Seq.:< rest) -> ...

We we “pop” the first course off of the queue, we first get the list of “post” courses that could now be unlocked by this course. Then we can apply our decDegree helper to get the final inDegrees’’ map and the “new 0’s”.

canFinishCourses :: Int -> [(Int, Int)] -> Bool
canFinishCourses numCourses prereqs = loop (0, queue, inDegrees) == numCourses
  where
    (inDegrees, unlocks) = foldr processPrereq (IM.empty, IM.empty) prereqs
    queue = Seq.fromList
      (filter (`IM.notMember` inDegrees) [0..numCourses-1])

    loop :: CourseState -> Int
    loop (numSatisfied, queue’, inDegrees’) = case Seq.viewl queue' of
      Seq.EmptyL -> numSatisfied
      (course Seq.:< rest) ->
        let posts = fromMaybe [] (IM.lookup course unlocks)
            (inDegrees'', new0s) = foldr decDegree (inDegrees', []) posts
        ...

Finally, we append the new 0’s to the end of the queue, and we make our recursive call, completing the loop and the function!

canFinishCourses :: Int -> [(Int, Int)] -> Bool
canFinishCourses numCourses prereqs = loop (0, queue, inDegrees) == numCourses
  where
    (inDegrees, unlocks) = foldr processPrereq (IM.empty, IM.empty) prereqs
    queue = Seq.fromList
      (filter (`IM.notMember` inDegrees) [0..numCourses-1])

    loop :: CourseState -> Int
    loop (numSatisfied, queue’, inDegrees’) = case Seq.viewl queue' of
      Seq.EmptyL -> numSatisfied
      (course Seq.:< rest) ->
        let posts = fromMaybe [] (IM.lookup course unlocks)
            (inDegrees'', new0s) = foldr decDegree (inDegrees', []) posts
            queue'' = foldl (Seq.|>) rest new0s
        in  loop (numSatisfied + 1, queue'', inDegrees'')

Here’s the full solution, from start to finish:

type DegCount = IM.IntMap Int
type CourseMaps = (DegCount, IM.IntMap [Int])
type CourseState = (Int, Seq.Seq Int, DegCount)

canFinishCourses :: Int -> [(Int, Int)] -> Bool
canFinishCourses numCourses prereqs = loop (0, queue, inDegrees) == numCourses
  where
    incKey :: Int -> DegCount -> DegCount
    incKey k mp = case IM.lookup k mp of
      Nothing -> IM.insert k 1 mp
      Just x -> IM.insert k (x + 1) mp

    appendUnlock :: Int -> Int -> IM.IntMap [Int] -> IM.IntMap [Int]
    appendUnlock pre post mp = case IM.lookup pre mp of
      Nothing -> IM.insert pre [post] mp
      Just prev -> IM.insert pre (post : prev) mp

    processPrereq :: (Int, Int) -> CourseMaps -> CourseMaps
    processPrereq (post, pre) (inDegrees', unlocks') =
      (incKey post inDegrees', appendUnlock pre post unlocks')
    
    (inDegrees, unlocks) = foldr processPrereq (IM.empty, IM.empty) prereqs

    queue = Seq.fromList
      (filter (`IM.notMember` inDegrees) [0..numCourses-1])

    decKey :: Int -> DegCount -> (DegCount, Bool)
    decKey key mp = case IM.lookup key mp of
      Nothing -> (mp, True)
      Just x -> if x <= 1
        then (IM.delete key mp, True)
        else (IM.insert key (x - 1) mp, False)
    
    decDegree :: Int -> (DegCount, [Int]) -> (DegCount, [Int])
    decDegree post (inDegrees', new0s) =
      let (inDegrees'', removed) = decKey post inDegrees'
      in  (inDegrees'', if removed then (post : new0s) else new0s)
    
    loop :: CourseState -> Int
    loop (numSatisfied, queue', inDegrees') = case Seq.viewl queue' of
      Seq.EmptyL -> numSatisfied
      (course Seq.:< rest) ->
        let posts = fromMaybe [] (IM.lookup course unlocks)
            (inDegrees'', new0s) = foldr decDegree (inDegrees', []) posts
            queue'' = foldl (Seq.|>) rest new0s
        in  loop (numSatisfied + 1, queue'', inDegrees'')

Conclusion

This problem showed the challenge of working with multiple mutable types in Haskell loops. You have to be very diligent about tracking what pieces are mutable, and you often need to write a lot of helper functions to keep your code clean. In our course, Solve.hs, you’ll learn about writing compound data structures to help you solve problems more cleanly. A Graph is one example, and you’ll also learn about occurrence maps, which we could have used in this problem.

That’s all for graphs right now. In the next couple weeks, we’ll cover the Trie, a compound data structure that can help with some very specific problems.

by James Bowen at September 15, 2025 08:30 AM

70: Phil Wadler

We sat down with Phil Wadler, one of the most influential folks in the Haskell community, functional programming, and programming languages, responsible for type classes, monads, and much more. We take a stroll down memory lane, starting from Haskell's inception. We talked about the difference between research and Phil's work on impactful industrial projects and standards - specifically XML and the design of generics in Java, as well as Phll's teaching at the University of Edinburgh using Agda.. Phil is a fountain of great ideas and stories, and this conversation could have gone on for hours. As it is, we hope you enjoy the hour that we had as much as we did. 

by Haskell Podcast at September 14, 2025 07:00 AM

Moonbit developers are lying to you

The Moonbit team recently published a blog post claiming their language runs "30% faster than Rust" for FFT workloads. This is a lie by omission. They benchmarked against a deliberately crippled Rust implementation that no competent programmer would write.

• The Moonbit FFT benchmark used a crippled Rust baseline and used to claim their language was faster than Rust.
• My corrected Rust implementation is 3.2–3.4× faster than Moonbit on the same benchmark.
• In 5 minutes of prompting GPT-5, I produced a Rust version already 2.33× faster than Moonbit.
• Zero PRs merged or replied to by the team at time of writing. There are PRs fixing the Rust benchmark older than their tweet announcing Moonbit was faster than Rust.
• Moonbit devs are programming language developers that have marketed their language aggressively on the basis of performance for awhile now, they know better than this.
• Moonbit should retract or clearly amend their blog post with corrected Rust baseline results. Including the qualification that their benchmark is a naive Cooley-Tukey FFT benchmark and nothing else.

by Unknown at September 14, 2025 12:00 AM

Haskell equations, thirty-eight years later

One night, while drifting off to sleep (or failing to), I solved a conundrum that has puzzled me since 1987.

Before Haskell there was Orwell. In Orwell equations were checked to ensure order is unimportant (similar to Agda today). When an equation was to match only if no previous equation applied, it was to be preceded by ELSE. Thus, equality on lists would be defined as follows:

    (==) :: Eq a => [a] -> [a] -> Bool
    [] == []          =  True
    (x:xs) == (y:ys)  =  x == y && xs == ys
    ELSE
    _ == _            =  False

We pondered whether to include this restriction in Haskell. Further, we wondered whether Haskell should insist that order is unimportant in a sequence of conditionals, unless ELSE was included. Thus, equality on an abstract type Shape would be defined as follows:

    (==) :: Shape -> Shape -> Bool
    x == y | circle x && circle y  =  radius x == radius y
           | square x && square y  =  side x == side y
    ELSE
           | otherwise             =  False

In Orwell and early Haskell, guards were written at the end of an equation and preceded by the keyword if or the end of an equation could be labelled otherwise. (Miranda was similar, but lacked the keywords.) Here I use the guard notation, introduced later by Paul Hudak, where otherwise is a variable bound to True.

Sometime two equations or two guards not separated by ELSE might both be satisfied. In that case, we thought the semantics should ensure that both corresponding right-hand sides returned the same value, indicating an error otherwise. Thus, the following:

    plus :: Thing -> Thing -> Thing
    plus x y | zero x     =  y
             | zero y     =  x
    ELSE
             | otherwise  =  ...

would be equivalent to:

    plus :: Thing -> Thing -> Thing
    plus x y | zero x && zero y && x == y    =  x
             | zero x && zero y && x /= y    =  error "undefined"
             | zero x && not (zero y)        =  y
             | not (zero x) && zero y        =  x
             | not (zero x) && not (zero y)  =  ...

Here the code checks that if x and y are both zero then they are the same. (I will consider a refinement to the check for sameness later.) Of course, the compiler would issue code that performs the tests zero x, zero y, and x == y at most once.

We didn’t pursue this design in Haskell for two reasons. First, because we thought it might be too unfamiliar. Second, because the ELSE on a line by itself was syntactically awkward. It would be especially annoying if one ever wanted the usual cascading behaviour:

    f :: Thing -> Thing
    f x | p x  =  ...
    ELSE
        | q x  =  ...
    ELSE
        | r x  =  ...

Here each guard is tested in turn, and we take the first that succeeds.

Today, the first problem is perhaps no longer quite so strong an issue. Many applications using Haskell would welcome the extra assurance from flagging any cases where order of the equations is significant. But the syntactic awkwardness of ELSE remains considerable. It was syntax about which I had an insight while tossing in bed.

Above otherwise is a variable bound to True in the standard prelude. But say we were to treat otherwise as a keyword, and to give it the meaning that the equation applies only if no previous equation applies, and to allow it to optionally be followed by a further guard. Then our first example becomes:

    (==) :: Eq a => [a] -> [a] -> Bool
    [] == []            =  True
    (x:xs) == (y:ys)    =  x == y && xs == ys
    _ == _ | otherwise  =  False

And our second example becomes:

    (==) :: Shape -> Shape -> Bool
    x == y | circle x && circle y  =  radius x == radius y
           | square x && square y  =  side x == side
           | otherwise             =  False

And our third example becomes:

    plus :: Thing -> Thing -> Thing
    plus x y | zero x     =  y
             | zero y     =  x
             | otherwise  =  ...

If one doesn’t want to invoke the equality test in the case that both zero x and zero y hold then one would instead write:

    plus :: Thing -> Thing -> Thing
    plus x y | zero x            =  y
             | otherwise zero y  =  x
             | otherwise         =  ...

Similarly, the cascading example becomes:

    f :: Thing -> Thing
    f x | p x            =  ...
        | otherwise q x  =  ...
        | otherwise r x  =  ...

That’s it! The syntactic awkwardness is greatly reduced.

The proposed notation depends upon Paul’s clever insight to move the guard from the end of the equation to the middle, so evaluation works strictly left to right. But we’ve had guards in that position for quite a while now. Goodness knows why none of us hit upon this proposal thirty-odd years ago.

Of course, the change is not backward compatible. Changes to guards could be made backward compatible (with added ugliness) by using a different symbol than ‘|’ to mark guards with the new semantics. But now the old definition of (==) should not be accepted without an otherwise, and I cannot think of how to introduce that new semantics with a backward compatible syntax.

The solution, as with so much of Haskell nowadays, is to activate the new semantics with a pragma. Manual porting of legacy code would not be hard in most cases, and it would also be easy to write a tool that adds otherwisewhenever the equations are not easily shown to be independent of order.

John Hughes suggests a further refinement to the above. Using equality to check that the value of two equations is the same may not be appropriate if the values are computed lazily. Instead, he suggests that the plus example should translates as follows:

    plus :: Thing -> Thing -> Thing
    plus x y | zero x && zero y              =  x `meet` y
             | zero x && not (zero y)        =  y
             | not (zero x) && zero y        =  x
             | not (zero x) && not (zero y)  =  ...

Here we presume a type class

    class Meet a where
      meet : a -> a -> a

which confirms that the two arguments are the same and returns a value that is the same as both the arguments. For strict data types, two arguments are the same if they are equal.

    instance Meet Integer where
      x `meet` y | x == y     =  x
                 | otherwise  =  error "undefined"

For lazy data types, we check that they are the meet lazily.

    instance Meet a => Meet [a] where
      [] `meet` []           =  []
      (x:xs) `meet` (y:ys)   =  (x `meet` y) :: (xs `meet` ys)
      meet _ _  | otherwise  =  error "undefined"

If the compiler could not verify that equations are disjoint, it would require that their right-hand sides have a type belonging to the class Meet.

In most cases, one would hope the compiler could verify that equations are disjoint, and hence would not have to resort to meet or additional checks. One might wish to allow a pragma to declare disjointness, permitting the compiler to assume, for instance, that x < y and x >= y are disjoint. An SMT solver could do much of the work of checking for disjointness.

In general, equations not separated with otherwise would be checked to ensure they are disjoint or all give equivalent results. For example,

    g :: Thing -> Thing
    g x | p x             =  a x
        | q x             =  b x
        | otherwise r x   =  c x
        | s x             =  d x
        | otherwise t x   =  e x

would be equivalent to

    g :: Thing -> Thing
    g x | p x && q x              =  a x `meet` b x
        | p x && not (q x)        =  a x
        | q x && not (p x)        =  b x
        | otherwise r x && s x    =  c x `meet` d x
        | r x && not (s x)        =  c x
        | s x && not (r x)        =  d x
        | otherwise t x           =  e x

On the other hand, if we declared that p x and q x are disjoint, and the same for s x and r x, then the first code would instead compile to something equivalent to Haskell’s current behaviour,

    g :: Thing -> Thing
    g x | p x             =  a x
        | otherwise q x   =  b x
        | otherwise r x   =  c x
        | otherwise s x   =  d x
        | otherwise t x   =  e x

One drawback of this proposal is that the source code doesn’t directly indicate when extra tests and the use of meet are required. An IDE might provide feedback to make explicit which tests are performed, or one might also add pragmas or additional syntax to reflect that information in the source.

I hope some reader might be keen to take this forward. What do you think?

by Philip Wadler (noreply@blogger.com) at September 13, 2025 10:37 PM

GHC 9.14.1-alpha2 is now available

GHC 9.14.1-alpha2 is now available

bgamari - 2025-09-12

The GHC developers are very pleased to announce the availability of the second alpha prerelease of GHC 9.14.1. Binary distributions, source distributions, and documentation are available at downloads.haskell.org.

GHC 9.14 will bring a number of new features and improvements, including:

• Significant improvements in specialisation:

  • The SPECIALISE pragma now allows use of type application syntax

  • The SPECIALISE pragma can be used to specialise for expression arguments as well as type arguments.

  • Specialisation is now considerably more reliable in the presence of newtypes

• Significant improvements in the GHCi debugger

• Record fields can be defined to be non-linear when LinearTypes is enabled.

• RequiredTypeArgments can now be used in more contexts

• SSE/AVX2 support in the x86 native code generator backend

• A major update of the Windows toolchain

• … and many more

A full accounting of changes can be found in the release notes. Given the many specialisation improvements and their potential for regression, we would very much appreciate testing and performance characterisation on downstream workloads.

Observant readers of these prerelease announcements will note that polymorphic specialisation has been dropped from alpha 2. This measure was taken out of an abundance of caution after finding a miscompilation during testing of alpha 1. While this bug will be fixed in the next alpha, we expect to keep polymorphic specialisation disabled by default in the final release. Users needing more aggressive specialisation can explicitly enable this feature with the -fpolymorphic-specialisation flag. Depending upon our experience with 9.14.1, we may enable this feature by default in a later minor release.

This is the second of three expected alpha prereleases. We expect the next (third) alpha will come 23 Sept. 2025, with the release candidate coming 7 Oct. 2025.

We would like to thank the Zw3rk stake pool, Well-Typed, Mercury, Channable, Tweag I/O, Serokell, SimSpace, the Haskell Foundation, and other anonymous contributors whose on-going financial and in-kind support has facilitated GHC maintenance and release management over the years. Finally, this release would not have been possible without the hundreds of open-source contributors whose work have made the Haskell ecosystem what it is today.

As always, do give this release a try and open a ticket if you see anything amiss.

by ghc-devs at September 12, 2025 12:00 AM

GHC 9.14.1-alpha2 is now available

GHC 9.14.1-alpha2 is now available

bgamari - 2025-09-12

The GHC developers are very pleased to announce the availability of the second alpha prerelease of GHC 9.14.1. Binary distributions, source distributions, and documentation are available at downloads.haskell.org.

GHC 9.14 will bring a number of new features and improvements, including:

• Significant improvements in specialisation:

  • The SPECIALISE pragma now allows use of type application syntax

  • The SPECIALISE pragma can be used to specialise for expression arguments as well as type arguments.

  • Specialisation is now considerably more reliable in the presence of newtypes

• Significant improvements in the GHCi debugger

• Record fields can be defined to be non-linear when LinearTypes is enabled.

• RequiredTypeArgments can now be used in more contexts

• SSE/AVX2 support in the x86 native code generator backend

• A major update of the Windows toolchain

• … and many more

A full accounting of changes can be found in the release notes. Given the many specialisation improvements and their potential for regression, we would very much appreciate testing and performance characterisation on downstream workloads.

Observant readers of these prerelease announcements will note that polymorphic specialisation has been dropped from alpha 2. This measure was taken out of an abundance of caution after finding a miscompilation during testing of alpha 1. While this bug will be fixed in the next alpha, we expect to keep polymorphic specialisation disabled by default in the final release. Users needing more aggressive specialisation can explicitly enable this feature with the -fpolymorphic-specialisation flag. Depending upon our experience with 9.14.1, we may enable this feature by default in a later minor release.

This is the second of three expected alpha prereleases. We expect the next (third) alpha will come 23 Sept. 2025, with the release candidate coming 7 Oct. 2025.

We would like to thank the Zw3rk stake pool, Well-Typed, Mercury, Channable, Tweag I/O, Serokell, SimSpace, the Haskell Foundation, and other anonymous contributors whose on-going financial and in-kind support has facilitated GHC maintenance and release management over the years. Finally, this release would not have been possible without the hundreds of open-source contributors whose work have made the Haskell ecosystem what it is today.

As always, do give this release a try and open a ticket if you see anything amiss.

by ghc-devs at September 12, 2025 12:00 AM

Qualified Imports and Alias Resolution in Liquid Haskell

Liquid Haskell (LH) is a formal verification tool for Haskell programs, with the potential to prove correctness with considerably less friction than approaches that aim to make code correct by construction using dependent types—often at the cost of heavy refactoring (as argued in a previous post). It has come a long way towards becoming a usable tool by adding quality-of-life features to foster its adoption. Think optimization of spec verification and improved user experience.

During my GSoC 2025 Haskell.org project with Tweag, I worked on a seemingly small but impactful feature: allowing LH’s type and predicate aliases to be written in qualified form. That is, being able to write Foo.Nat instead of only just Nat, like we can for regular Haskell type aliases.

In this post, I introduce these annotations and their uses, walk through some of the design decisions, and share how I approached the implementation.

Aliasing refinement types

Type and predicate aliases in LH help users abstract over refinement type annotations, making them easier to reuse and more concise. A type alias refines an existing type. For instance, LH comes with built-in aliases like Nat and Odd, which refine Int to represent natural and odd numbers, respectively.

{-@ type Nat = {v: Int | v >= 0 } @-}

{-@ type Odd = {v: Int | (v mod 2) = 1 } @-}

Predicate aliases, by contrast, capture only the predicate part of a refinement type. For example, we might define aliases for positive and negative numerical values.

-- Value parameters in aliases are specified in uppercase,
-- while lowercase is reserved for type parameters.

{-@ predicate Neg N = N < 0 @-}

{-@ predicate Pos N = N > 0 @-}

Enter the subtle art of giving descriptive names so that our specifications read more clearly. Consider declaring aliases for open intervals with freely oriented boundaries.

{-@ predicate InOpenInterval A B X =
      (A != B) &&
      ((X > A && X < B) || (X > B && X < A)) @-}

{-@ type OpenInterval A B = { x:Float | InOpenInterval A B x } @-}

These aliases can then be used to prove, for instance, that an implementation of an affine transformation, fromUnitInterval below, from the open unit interval to an arbitrary interval is a bijection. The proof proceeds by supplying an inverse function (toUnitInterval) and specifying¹ that their composition is the identity. The example shows one half on the proof; the other half is straightforward and left to the reader.

type Bound = Float

{-@ inline fromUnitInterval @-}
{-@ fromUnitInterval :: a : Bound
                     -> { b : Bound | a != b }
                     -> x : OpenInterval 0 1
                     -> v : OpenInterval a b @-}
fromUnitInterval :: Bound -> Bound -> Float -> Float
fromUnitInterval a b x = a + x * (b - a)

{-@ inline toUnitInterval @-}
{-@ toUnitInterval :: a : Bound
                   -> { b : Bound | a != b }
                   -> x : OpenInterval a b
                   -> v : OpenInterval 0 1 @-}
toUnitInterval :: Bound -> Bound -> Float -> Float
toUnitInterval a b x = (x - a) / (b - a)

{-@ intervalId :: a : Bound
                   -> { b : Bound | a != b }
                   -> x : OpenInterval a b
                   -> {v : OpenInterval a b | x = v} @-}
intervalId :: Bound -> Bound -> Float -> Float
intervalId a b x = fromUnitInterval a b . toUnitInterval a b

Another case: refining a Map type to a fixed length allows us to enforce that a function can only grant access privileges to a bounded number of users at any call site.

type Password = String
type Name = String

{-@ type FixedMap a b N = { m : Map a b | len m = N } @-}

{-@ giveAccess :: Name
               -> Password
               -> FixedMap Name Password 3
               -> Bool @-}
giveAccess :: Name -> Password -> Map Name Password -> Bool
giveAccess name psswd users =
  Map.lookup name users == Just psswd

None of these specifications strictly require aliases, but they illustrate the practical convenience they bring.

A crowded name space

When we try to be simple and reasonable about such aliases, it becomes quite likely for other people to converge on the same names to describe similar types. Even a seemingly standard type such as Nat is not safe: someone with a historically informed opinion might want to define it as strictly positive numbers², or may just prefer to refine Word8 instead of Int.

Naturally, this is the familiar problem of name scope, for which established solutions exist, such as modules and local scopes. Yet for LH and its Nat, it was the case that one would have to either invent a non-conflicting name, exclude assumptions for the base package, or avoid importing the Prelude altogether. It might be argued that having to invent alternative names is a minor nuisance, but also that it can quickly lead to unwieldy and convoluted naming conventions once multiple dependencies expose their own specifications.

Simply stated, the problem was that LH imported all aliases from transitive dependencies into a flat namespace. After my contribution, LH still accumulates aliases transitively, but users gain two key capabilities: (i) to disambiguate occurrences by qualifying an identifier, and (ii) to overwrite an imported alias without conflict. In practice, this prevents spurious verification failures and gives the user explicit means to resolve clashes when they matter.

Consider the following scenario. Module A defines alias Foo. Two other modules, B and B', both define an alias Bar and import A.

module A where
{-@ type Foo = { ... } @-}

module B where
import A
{-@ type Bar = { ... } @-}

module B' where
import A
{-@ type Bar = { ... } @-}

A module C that imports B and B' will now see Foo in scope unambiguously, while any occurrence of Bar must be qualified in the usual Haskell manner.

module C where

import B
import B'

{-@ baz :: Foo -> B.Bar @-}
baz _ = undefined

Previously, this would have caused C to fail verification with a conflicting definitions error, even if Bar was never used.

examples/B.hs:3:10: error:
    Multiple definitions of Type Alias `Bar`
    Conflicting definitions at
    .
    * examples/B.hs:3:10-39
    .
    * examples/B'.hs:3:10-39
  |
3 | {-@ type Bar = { ... } @-}
  |          ^^^^^^^^^^^^^^

This error is now only triggered when the alias is defined multiple times within the same module. And instead, when an ambiguous type alias is found, the user is prompted to choose among the matching names in scope and directed to the offending symbol.

examples/C.hs:6:19: error:
    Ambiguous specification symbol `Bar` for type alias
    Could refer to any of the names
    .
    * Bar imported from module B defined at examples/B.hs:3:10-39
    .
    * Bar imported from module B' defined at examples/B'.hs:3:10-39
  |
6 | {-@ baz :: Foo -> Bar @-}
  |                   ^^^

The precise behavior is summarized in a set of explicit rules that I proposed, which specify how aliases are imported and exported under this scheme.

The initial name resolution flow

The project goals were initially put forward on a GitHub issue as a spin-off from a recent refactoring of the codebase that changed the internal representation of names to a structured LHName type that distinguishes between resolved and unresolved names and stores information about where the name originates, so that names are resolved only once for each compiled module.

Name resolution has many moving parts, but in broad terms its implementation is divided into two phases: The first handles names corresponding to entities GHC knows of—data and type constructors, functions, and annotation binders of aliases, measures, and data constructors—and uses its global reader environment to look them up. The resolution of logical entities (i.e. those found in logical expressions) is left for the second phase, where the names resolved during the first phase are used to build custom lookup environments.

Occurrences of type and predicate aliases were resolved by looking them up in an environment indexed by their unqualified name. When two or more dependencies (possibly transitive) defined the same alias, resolution defaulted to whichever definition happened to be encountered first during collection. This accidental choice was effectively irrelevant, however, since a later duplicate-name check would short-circuit with the aforementioned error. Locally defined aliases were recorded in the module’s interface file after verification, and LH assembled the resolution environment by accumulating the aliases from the interface files of all transitive dependencies.

The reason a module import brings all aliases from transitive dependencies into scope is that no mechanism exists to declare which aliases a module exports or imports. Implementing such a mechanism exceeded the project’s allocated time, so a trade-off was called for. On the importing side, Haskell’s qualifying directives could be applied, but an explicit defaulting mechanism was needed to determine what aliases a module exposes. This left us with at least three possibilities:

1. Export no aliases, so that they would be local to each module alone. This no-op solution would allow the user to use any names she wants, but quickly becomes inconvenient as an alias would have to be redefined in each module she intends to use it.
2. Export only those locally defined, so that only aliases from direct dependencies would be in scope for any given module. This could leave out aliases used to specify re-exported functions, so we would end up in a similar situation as before.
3. Export all aliases from transitive dependencies, avoiding the need to ever duplicate an alias definition.

The chosen option (3) reflects the former behavior and, complemented by the ability qualify and overwrite aliases, it was deemed the most effective solution.

Qualifying type aliases

Type aliases are resolved during the first phase, essentially because they are parsed as type constructors, which are resolved uniformly across the input specification. Two changes had to be made to qualify them: include module import information in the resolution environment to discern which module aliases can be used to qualify an imported type alias, and make sure transitively imported aliases are stored in the interface file along with the locally defined type aliases.

Careful examination of the code revealed that we could reuse environments built for other features of LH that could be qualified already! And as a bonus, their lookup function returns close-match alternatives in case of failure. Factoring this out almost did the trick. In addition, I had to add some provisions to give precedence to locally defined aliases during lookups.

Qualifying predicate aliases

Two aspects of the code made predicate aliases somewhat hard to reason about. First, predicate aliases are conflated in environments with Haskell entities lifted by inline and define annotations. The rationale is to use a single mechanism to expand these definitions in logical expressions.

Second, the conflated environments were redundantly gathered twice with different purposes: to resolve Haskell function names in logical expressions, and afterwards again to resolve occurrences of predicate aliases.

Both were not straightforward to deduce from the code. These facts, together with some code comments from the past about predicate aliases being the last names that remained “unhandled”, pointed the way.

The surgical change, then, was to sieve out predicate aliases from the lifted Haskell functions as they were stored together in interface files, and include these predicate aliases in the environment used to resolve qualified names for other features.

Alias expansion

Although the problem I set out to solve was primarily about name resolution, the implementation also required revisiting another process: alias expansion. For a specification to be ready for constraint generation, all aliases must be fully expanded (or unfolded), since liquid-fixpoint³ has no notion of aliases.

Uncovering this detail was crucial to advance with the implementation. It clarified why Haskell functions lifted with inline or define are eventually converted into predicate aliases: doing so allows for every aliasing annotation to be expanded consistently in a single pass wherever they appear in a specification. With qualified aliases, the expansion mechanism needed some adjustments, as the alias names were now more structured (LHName).

An additional complication was that the logic to expand type aliases was shared with predicate aliases, and since I did qualification of type aliases first, I needed to have different behavior for type and predicate aliases. In the end, I opted for duplicating the expansion logic for each case during the transition, and unified it again after implementing qualification of predicate aliases.

Closing remarks

My determination to understand implementation details was rewarded by insights that allowed me to refactor my way to a solution. For perspective, my contribution consisted of a 210 LOC addition for the feature implementation alone, after familiarizing myself with 2,150 LOC out of the 25,000 LOC making up the LH plugin. The bulk of this work is contained in two merged PRs (#2550 and #2566), which include detailed source documentation and tests.

The qualified aliases support and the explicit rules that govern it are a modest addition, but hopefully one of a positive impact on user experience. LH tries to be as close as possible to Haskell, but refinement type aliases still mark the boundary between both worlds. Perhaps the need for an ad hoc mechanism for importing and exporting logic entities will be revised in a horizon where LH gets integrated into GHC (which sounds good to me!).

This project taught me about many language features and introduced me to the GHC API; knowledge I will apply in future projects and to further contribute to the Haskell ecosystem. I am grateful to Facundo Domínguez for his generous and insightful mentoring, which kept on a creative flow throughout the project. Working on Liquid Haskell was lots of fun!

---

1. Note that, in this example, the inline annotation is used to translate the Haskell definitions into the logic so Liquid Haskell can unfold calls to these functions when verifying specifications.↩
2. It took humanity quite a while to think clearly about a null quantity, and further still for it to play a fundamental role as a placeholder for positional number notation.↩
3. liquid-fixpoint is the component of Liquid Haskell that transforms a module’s specification into a set of constraints for an external SMT solver.↩

September 11, 2025 12:00 AM

GHC 9.10.3 is now available

GHC 9.10.3 is now available

Zubin Duggal - 2025-09-10

The GHC developers are very pleased to announce the availability of the final release for GHC 9.10.3. Binary distributions, source distributions, and documentation are available at downloads.haskell.org and via GHCup.

GHC 9.10.3 is a bug-fix release fixing many issues of a variety of severities and scopes, including:

• Fix a number of crashes in the compiler frontend (#25960, #25004, #25056)
• Fix incorrect results in the NCG (#25601, #26061)
• Support for far jumps in the AArch64 NCG (#24648)
• A fix for a segfault in the RTS when running certain code involving STM (#26205)
• And many more!

A full accounting of these fixes can be found in the release notes. As always, GHC’s release status, including planned future releases, can be found on the GHC Wiki status.

We would like to thank Well-Typed, Tweag I/O, Juspay, QBayLogic, Channable, Serokell, SimSpace, the Haskell Foundation, and other anonymous contributors whose on-going financial and in-kind support has facilitated GHC maintenance and release management over the years. Finally, this release would not have been possible without the hundreds of open-source contributors whose work comprise this release.

As always, do give this release a try and open a ticket if you see anything amiss.

by ghc-devs at September 10, 2025 12:00 AM

Translation Table

I remember seeing a version of the above in High School. My favourite entries, which I quote to this day, are

"... accidentally strained during mounting" --> "... dropped on the floor"

"... handled with extreme care throughout the experiments" --> "... not dropped on the floor"

and

"correct within an order of magnitude" --> "wrong"

From Futility Closet. Spotted via Boing Boing.

by Philip Wadler (noreply@blogger.com) at September 09, 2025 11:34 AM

Why are we funding this?

 

In the face of swinging funding cuts in the US, David Samuel Shiffman defends the value of scientific curiosity in American Scientist. Spotted via Boing Boing.

by Philip Wadler (noreply@blogger.com) at September 09, 2025 11:18 AM

Graph Algorithms in Board Games!

For last week’s problem we started learning about graph algorithms, focusing on depth-first-search. Today we’ll do a problem from an old board game that will require us to use breadth-first-search. We’ll also learn about a special library in Haskell that lets us solve these types of problems without needing to implement all the details of these algorithms.

To learn more about this library and graph algorithms in Haskell, you should check out our problem solving course, Solve.hs! Module 3 of the course focuses on algorithms, with a special emphasis on graph algorithms!

The Problem

Today’s problem comes from a kids board game called Snakes and Ladders, which will take a little bit to explain. First, we imagine we have a square board in an N x N grid, where each cell is numbered 1 to N^2. The bottom left corner is always “1”, and numbers increase in a snake-like fashion. First the increase from left to right along the bottom row. Then they go from right to left in the next row, before reversing again. Here’s what the numbers look like for a 6x6 board:

36 35 34 33 32 31
25 26 27 28 29 30
24 23 22 21 20 19
13 14 15 16 17 18
12 11 10  9  8  7
 1  2  3  4  5  6

The “goal” is to reach the highest numbered tile, which is either in the top left (for even grid sizes) or the top right (for odd grid sizes). One moves by rolling a 6-sided die. Given the number on the die, you are entitled to move that many spaces. The ordinary path of movement is following the increasing numbers.

As is, the game is a little boring. You just always want to roll the highest number you can. However, various cells on the grid are equipped with “snakes” or “ladders”, which can move you around the grid if your die roll would cause your turn to end where these items start. Ladders typically move you closer to the goal, snakes typically move you away from the goal. Here’s an illustrative picture of a board:

We can represent such a board by putting an integer on each cell. The integer -1 represents an ordinary cell, where you would simply proceed to the next cell in order. However, we can represent the start of each snake and ladder with a number corresponding to the cell number where you end up if your die role lands you there. Here’s an example:

-1 -1 -1 -1 -1 -1
-1 -1 -1 -1 -1 -1
-1 -1 -1 -1 -1 -1
-1 35 -1 -1 13 -1
-1 -1 -1 -1 -1 -1
-1 15 -1 -1 -1 -1

This grid has two ladders. The first can take you from position 2 to position 15 (see the bottom left corner). The second can take you from position 14 to position 35. There is also a snake, that will take you back from position 17 to position 13. Note that no matter the layout, you can only follow one snake or ladder on a turn. If you end your turn at the beginning of a ladder, which takes you to the beginning of another ladder, you do not take the second ladder on that turn.

Our objective is to find the smallest number of dice rolls possible to reach the goal cell (which will always have -1). In this case, the answer is 4. Various combinations of 3 rolls can land us on 14, which will take us to 35. Then rolling 1 would take us to the goal.

It is possible to contrive a board where it is impossible to reach the goal! We need to handle these cases. In these situations we must return -1. Here is such a grid, with many snakes, all leading back to the start!

1  1 -1
 1  1  1
-1  1  1

The Algorithm

This is a graph search problem where each step we take carries the same weight (one turn), and we are trying to find the shortest path. This makes it a canonical example of a Breadth First Search problem (BFS).

We solve BFS by maintaining a queue of search states. In our case, the search state might consist simply of our location, though we may also want to track the number of steps we needed to reach that location as part of the state.

We’ll have a single primary loop, where we remove the first element in our queue. We’ll find all its “neighbors” (the states reachable from that node), and place these on the end of the queue. Then we’ll continue processing.

BFS works out so that states with a lower “cost” (i.e. number of turns) will all be processed before any states with higher cost. This means that the first time we dequeue a goal state from our queue, we can be sure we have found the shortest path to that goal state.

As with last week’s problem, we’ll spend a fair amount of effort on our “neighbors” function, which is often the core of a graph solution. Once we have that in place, the mechanics of the graph search generally become quite easy.

Rust Solution

Once again we’ll start with Rust, because we’ll use a special trick in Haskell. As stated, we want to start with our neighbors function. We’ll represent a single location just using the integer representing it on the board, not its grid coordinates. So at root, we’re taking one usize and returning a vector of usize values. But we’ll also take the board (a 2D vector of integers) so we can follow the snakes and ladders. Finally, we’ll pass the size of the board (just N, since our board is always square) and the “goal” location so that we don’t have to recalculate these every time:

pub fn neighbors(n: usize, goal: usize, board: &Vec<Vec<i32>>, loc: usize) -> Vec<usize> {
    let mut results = Vec::new();
    ...
    return results;
}

The basic idea of this function is that we’ll loop through the possible die rolls (1 to 6) and return the resulting location from each roll. If we find that the roll would take us past the goal, then we can safely break:

pub fn neighbors(n: usize, goal: usize, board: &Vec<Vec<i32>>, loc: usize) -> Vec<usize> {
    let mut results = Vec::new();
    for i in 1..=6 {
        if loc + i > goal {
            break;
        }
        ...
    }
    return results;
}

How do we actually get the resulting location? We need to use the board, but in order to use the board, we have to convert the location into 2D coordinates. So let’s just write the frame for a function converting a location into coordinates. We’ll fill it in later:

pub fn convert(n: usize, loc: usize) -> (usize, usize) {
    ...
}

Assuming we have this function, the rest of our neighbors logic is easy. We check the corresponding value for the location in board. If it is -1, we just use our prior location added to the die roll. Otherwise, we use the location given in the cell:

pub fn neighbors(n: usize, goal: usize, board: &Vec<Vec<i32>>, loc: usize) -> Vec<usize> {
    let mut results = Vec::new();
    for i in 1..=6 {
        if loc + i > goal {
            break;
        }
        let (row, col) = convert(n, loc + i);
        let next = board[row][col];
        if next == -1 {
            results.push(loc + i);
        } else {
            results.push(next as usize);
        }
    }
    return results;
}

So let’s fill in this conversion function. It’s tricky because of the snaking order of the board and because we start from the bottom (highest row index) and not the top. Nonetheless, we want to start by getting the quotient and remainder of our location with the side-length. (We subtract 1 since our locations are 1-indexed).

pub fn convert(n: usize, loc: usize) -> (usize, usize) {
    let rowBase = (loc - 1) / n;
    let colBase = (loc - 1) % n;
    ...
}

To get the final row, we simply take n - rowBase - 1. The column is trickier. We need to consider if the row base is even or odd. If it is even, the row is going from left to right. Otherwise, it goes from right to left. In the first case, the modulo for the column gives us the right column. In the second case, we need to subtract from n like we did with rows.

pub fn convert(n: usize, loc: usize) -> (usize, usize) {
    let rowBase = (loc - 1) / n;
    let colBase = (loc - 1) % n;
    let row = n - rowBase - 1;
    let col = 
        if rowBase % 2 == 0 {
            colBase
        } else {
            n - colBase - 1
        };
    return (row, col);
}

But that’s all we need for conversion!

Now that our neighbors function is closed up, we can finally write the core solution. For the Rust solution, we’ll define our “search state” as including the location and the number of steps we took to reach it, so a tuple (usize, usize). We’ll create a VecDeque of these, which is Rust’s structure for a queue, and insert our initial state (location 1, count 0):

use std::collections::VecDeque;

pub fn snakes_and_ladders(board: Vec<Vec<i32>>) -> i32 {
    let n = board.len();
    let goal = board.len() * board[0].len();
    let mut queue: VecDeque<(usize, usize)> = VecDeque::new();
    queue.push_back((1,0));
    ...
}

We also want to track the locations we’ve already visited. This will be a hash set of the locations but not the counts. This is necessary to prevent infinite loops. Once we’ve visited a location there is no advantage to considering it again on a later branch (with this problem at least). We’ll also follow the practice of considering a cell “visited” once it is enqueued.

use std::collections::VecDeque;
use std::collections::HashSet;

pub fn snakes_and_ladders(board: Vec<Vec<i32>>) -> i32 {
    let n = board.len();
    let goal = board.len() * board[0].len();
    let mut queue: VecDeque<(usize, usize)> = VecDeque::new();
    queue.push_back((1,0));
    let mut visited = HashSet::new();
    visited.insert(1);
    ...
}

Now we’ll run a loop popping the front of the queue and finding the “neighboring” locations. If our queue is empty, this indicates no path was possible, so we return -1.

use std::collections::VecDeque;
use std::collections::HashSet;

pub fn snakes_and_ladders(board: Vec<Vec<i32>>) -> i32 {
    let n = board.len();
    let goal = board.len() * board[0].len();
    let mut queue: VecDeque<(usize, usize)> = VecDeque::new();
    queue.push_back((1,0));
    let mut visited = HashSet::new();
    visited.insert(1);
    while let Some((idx, count)) = queue.pop_front() {
        let ns = neighbors(n, goal, &board, idx);
        ...
    }
    return -1;
}

Now processing each neighbor is simple. First, if the neighbor is the goal, we’re done! Just return the dequeued count plus 1. Otherwise, check if we’ve visited the neighbor before. If not, push it to the back of the queue, along with an increased count:

pub fn snakes_and_ladders(board: Vec<Vec<i32>>) -> i32 {
    let mut queue: VecDeque<(usize, usize)> = VecDeque::new();
    queue.push_back((1,0));
    let n = board.len();
    let goal = board.len() * board[0].len();
    let mut visited = HashSet::new();
    visited.insert(1);
    while let Some((idx, count)) = queue.pop_front() {
        let ns = neighbors(n, goal, &board, idx);
        for next in ns {
            if next == goal {
                return (count + 1) as i32;
            }
            if !visited.contains(&next) {
                queue.push_back((next, count + 1));
                visited.insert(next);
            }
        }
    }
    return -1;                 
}

This completes our BFS solution! Here is the complete code:

use std::collections::VecDeque;
use std::collections::HashSet;

pub fn convert(n: usize, loc: usize) -> (usize, usize) {
    let rowBase = (loc - 1) / n;
    let colBase = (loc - 1) % n;
    let row = n - rowBase - 1;
    let col = 
        if rowBase % 2 == 0 {
            colBase
        } else {
            n - colBase - 1
        };
    return (row, col);
}

pub fn neighbors(n: usize, goal: usize, board: &Vec<Vec<i32>>, loc: usize) -> Vec<usize> {
    let mut results = Vec::new();
    for i in 1..=6 {
        if loc + i > goal {
            break;
        }
        let (row, col) = convert(n, loc + i);
        let next = board[row][col];
        if next == -1 {
            results.push(loc + i);
        } else {
            results.push(next as usize);
        }
    }
    return results;
}


pub fn snakes_and_ladders(board: Vec<Vec<i32>>) -> i32 {
    let mut queue: VecDeque<(usize, usize)> = VecDeque::new();
    queue.push_back((1,0));
    let n = board.len();
    let goal = board.len() * board[0].len();
    let mut visited = HashSet::new();
    visited.insert(1);
    while let Some((idx, count)) = queue.pop_front() {
        let ns = neighbors(n, goal, &board, idx);
        for next in ns {
            if next == goal {
                return (count + 1) as i32;
            }
            if !visited.contains(&next) {
                queue.push_back((next, count + 1));
                visited.insert(next);
            }
        }
    }
    return -1;                 
}

Haskell Solution

For our Haskell solution, we’re going to use a special shortcut. We’ll make use of the Algorithm.Search library to handle the mechanics of the BFS for us. The function we’ll use has this type signature (slightly simplified):

bfs :: (state -> [state]) -> (state -> Bool) -> state -> Maybe [state]

We provide 3 inputs. First is the “neighbors” function, taking one state and returning its neighbors. Second is the “goal” function, telling us if a state is our final goal state. Finally we give it the initial state. If a goal is reachable, we receive a path to that goal. If not, we receive Nothing. Since this library provides the full path for us automatically, we won’t track the number of steps in our state. Our “state” will simply be the location. So let’s begin by framing out our function:

snakesAndLadders :: A.Array (Int, Int) Int -> Int
snakesAndLadders board = ...
  where
    ((minRow, minCol), (maxRow, _)) = A.bounds board
    n = maxRow - minRow + 1
    goal = n * n

    convert :: Int -> (Int, Int)

    neighbor :: Int -> Int

    neighbors :: Int -> [Int]

Let’s start with convert. This follows the same rules we used in our Rust solution, so there’s not much to say here. We just have to make sure we account for non-zero start indices in Haskell arrays by adding minRow and minCol.

snakesAndLadders :: A.Array (Int, Int) Int -> Int
snakesAndLadders board = ...
  where
    ((minRow, minCol), (maxRow, _)) = A.bounds board
    n = maxRow - minRow + 1
    goal = n * n

    convert :: Int -> (Int, Int)
    convert loc =
      let (rowBase, colBase) = (loc - 1) `quotRem` n
          row = minRow + (n - rowBase - 1)
          col = minCol + if even rowBase then colBase else n - colBase - 1
      in  (row, col)

Now we’ll write a neighbor helper that converts a single location. This just makes our neighbors function a lot cleaner. We use the same logic of checking for -1 in the board, or else using the value we find there.

snakesAndLadders :: A.Array (Int, Int) Int -> Int
snakesAndLadders board = ...
  where
    ((minRow, minCol), (maxRow, _)) = A.bounds board
    n = maxRow - minRow + 1
    goal = n * n

    convert = ...

    neighbor :: Int -> Int
    neighbor loc =
      let coord = convert loc
          onBoard = board A.! coord
      in  if onBoard == -1 then loc else onBoard

Now we can write neighbors with a simple list comprehension. We look through each roll of 1-6, add it to the current location, filter if this location is past the goal, and then calculate the neighbor.

snakesAndLadders :: A.Array (Int, Int) Int -> Int
snakesAndLadders board = ...
  where
    ((minRow, minCol), (maxRow, _)) = A.bounds board
    n = maxRow - minRow + 1
    goal = n * n

    convert = ...

    neighbor = ...

    neighbors :: Int -> [Int]
    neighbors loc =
      [neighbor (loc + i) | i <- [1..6], loc + i <= goal]

Now for the coup-de-grace. We call bfs with our neighbors function. The “goal” function is just (== goal), and the starting state is just 1. It will return our shortest path, and so we just return its length:

snakesAndLadders :: A.Array (Int, Int) Int -> Int
snakesAndLadders board = case bfs neighbors (== goal) 1 of
  Nothing -> (-1)
  Just path -> length path
  where
    ((minRow, minCol), (maxRow, _)) = A.bounds board
    n = maxRow - minRow + 1
    goal = n * n

    convert :: Int -> (Int, Int)
    convert loc =
      let (rowBase, colBase) = (loc - 1) `quotRem` n
          row = minRow + (n - rowBase - 1)
          col = minCol + if even rowBase then colBase else n - colBase - 1
      in  (row, col)
    
    neighbor :: Int -> Int
    neighbor loc =
      let coord = convert loc
          onBoard = board A.! coord
      in  if onBoard == -1 then loc else onBoard
    
    neighbors :: Int -> [Int]
    neighbors loc =
      [neighbor (loc + i) | i <- [1..6], loc + i <= goal]

And that’s our complete Haskell solution!

Conclusion

If you take our Solve.hs course, Module 3 is your go-to for learning about graph algorithms! You’ll implement BFS from scratch in Haskell, and learn how to apply other helpers from Algorithm.Search. In next week’s article, we’ll do one more graph problem that goes beyond the basic ideas of DFS and BFS.

by James Bowen at September 08, 2025 08:30 AM

So you want to control flow in PT2

With contributions from Richard Zou.

PT2’s dominant internal representation, FX graphs, do not directly support control flow (if statements, while loops): they only represent straight-line basic blocks. Most of our graph capture mechanisms are tracing based (fx.symbolic_trace, make_fx, Dynamo), which means that we expect to be able to linearize all conditionals we encounter into a straight line program. Sometimes, you want to work with code that has control flow while working the compiler stack. There is no silver bullet, instead there are a lot of different options with different tradeoffs.

Regional compilation

We have a perfectly good general purpose language that supports control flow: Python. To handle control flow, compile only regions/submodules of your program that have no internal control flow, and then string them together with a standard Python control flow constructs. PT2 compiled regions are compositional with non-compiled regions, “it works.”

Pro:

• Simple: requires no major model changes
• Universal: it always works (including data dependent flow, calling into third-party libraries, making an HTTP request, anything!)

Cons:

• You will not get a full graph this way; you will only get graphs for each region. In particular, you will not be able to do truly global optimizations, nor will you be able to serialize a self-contained Python-less representation of the entire model
• It can sometimes be inconvenient to structure your program so all the regions you want are compilable. Suppose you have this call graph between modules: A -> B -> C. C is compileable; A is compileable except for its call to B, which is what does the control flow. It’s easy to compile C, but you can’t directly compile A, as it has a B-shaped bit that can’t be compiled. What to do? If you split A so it is pipelined as A1, B, A2, you can then compile A1 and A2, but not B. Dynamo also supports “graph breaks” to automatically perform this split for you, in which case you just disable compilation on B, but graph break generated graphs can be difficult to reason about as the inputs to A2 are implicitly inferred.

Link: Reducing torch.compile cold start compilation time with regional compilation

Multiple graphs dispatched with guards

When the control flow is controlled by arguments that are known ahead of time (no data-dependent), you can also compile at the top level and get the flattened straight-line program for the particular branching you had in this case. Because Dynamo is a symbolic bytecode interpreter, it can automatically determine what inputs were used as part of control flow, and generate guards to validate that we would take the same paths again. If those values change, we will recompile the program at the new values. We dispatch between all the different unrollings of the program we have generated.

Pros:

• Simple: requires no major model changes
• You get a full graph for a particular unrolling of loops / conditionals, so global optimizations are possible

Cons:

• Doesn’t work with data-dependent shapes.
• You will end up with a graph for every unrolling; for example, if you have a loop that ranges from 1 to 32, you will end up with 32 different graphs. This will increase compile time.

Black box via custom operator

An FX graph just calls operators. The operator internally can have whatever control flow in them they want. So you can always black box a problematic region of your model into an operator and preserve compilation for everything else.

Pros:

• You get a single, full graph that works for all possible branches

Cons:

• A custom operator only supports inputs/outputs that fall inside our type system, which means you can only pass simple types like Tensor, int, bool (or pytree-able containers containing these things). There is some in progress work to relax this to allow more opaque types.
• You have to explicitly declare all the inputs/outputs for the custom operator. This can be tiresome if the black boxed region represents a Module, since all the parameters also have to be directly passed in as well. The larger the region you black box, the bigger the arguments are.
• You don’t actually get to see the inside of the custom operator from the outside graph, so no optimization over both inside and outside of the custom operator is possible. (Of course, you can always special case this operator in a pass on the outer graph.)
• There are some bugs related to doing another torch.compile region inside of a custom operator, although these are workaroundable: https://github.com/pytorch/pytorch/issues/151328

Conditional operators / Unroll to max iterations

Do you really, really need a conditional? If you’re doing an if-branch, can you instead rewrite it so that you run both branches and torch.where dispatch to the results? If you’re doing a while-loop, can you unroll it to the max number of iterations and rely on dynamic shapes to cause it to no-op when you’re done and running extra iterations. Basically, this option is to rewrite your model so it doesn’t have Python-level control flow anymore (the conditional can either be done host or GPU side).

Pros:

• You get a single, full graph that works for all possible branches
• You are able to optimize inside and outside of the control flow

Cons:

• You have to rewrite your model
• For unrolling, if you are close to being CPU-dispatch bound, unrolling and running with zero size could push you over the brink (as zero size dispatches are still not free)
• For conditional operators, unconditionally both branches increases the compute you need to do, which can be bad if you are compute-bound.

Control flow HOP

torch has special structured control flow operators that avoid unrolling large loops or needing to execute both branches of a control flow statement. If you’re familiar with JAX, these are very similar to the JAX equivalents. They have specific constraints that allow them to be directly compilable by torch.compile. For example, torch.cond accepts two functions (a true_fn and a false_fn) for the two branches and requires that outputs of each function must have the same properties (e.g. shape, dtype).

So far, we have the following “higher-order” operators (HOPs):

• torch.cond (differentiable)
• torch.while_loop (not yet differentiable)
• torch._higher_order_ops.scan (differentiable, ignore the docs)

These are relatively new, have been used in torch.export for inference, but have not been battle tested for training or performance.

The semantics of these control flow operators are as follows:

def cond(pred, true_branch, false_branch, operands):
    if pred:
        return true_branch(*operands)
    else:
        return false_branch(*operands)

def while_loop(cond_fn, body_fn, carried_inputs):
    val = carried_inputs
    while cond_fn(*val):
        val = body_fn(*val)
    return val

def scan(combine_fn, init, xs, length=None):
    carry = init
    ys = []
    for x in xs:
        carry, y = f(carry, x)
        ys.append(y)
    return carry, np.stack(ys)

Pros:

• You get a single, full graph that works for all possible branches
• You are able to optimize inside and outside of the control flow

Cons:

• You have to rewrite your model.
• The control flow HOPs are structured: they have specific constraints on the functions (true_fn, false_fn (cond) or body_fn (while_loop)) that can be passed to them. One such constraint is that these functions may not mutate any of their inputs. This may make rewrites difficult because you have to think about code in a “functional”, JAX-like way.
• Still WIP and they have some quirks especially for training. For example, the backward pass of torch.scan currently requires re-computing the forward pass (instead of just saving intermediates from each iteration of scan).

CFG over FX graphs

If FX graphs give you basic blocks, you can use them as building blocks for a language that does support conditionals, stringing them together with basic blocks. In fact, Helion, a kernel DSL language, does exactly this, as it is common to need to directly write data-dependent conditionals and loops when writing kernels (it otherwise uses all PyTorch API functions, similar to conventional FX graphs). To do this, you would need to write your own Python frontend that parses Python directly to generate the CFG. TorchScript also does this, but TorchScript frontend is unmaintained and we don’t recommend using it (and it also doesn’t generate FX graphs by default.)

Pros:

• You get a single graph that works for all possible branches
• You are able to optimize inside and outside of control flow
• In principle, you can write exactly the control flow you want

Cons:

• You have to write the frontend, we don’t have one ready for you (TorchScript is not it, you’re princess is in another castle)
• If your language looks too much like Python and too general purpose, prepare to get on the endless treadmill of feature requests for adding “just one more Python feature” (can we have lists? dataclasses? etc etc) in the frontend (it is more tractable for Helion, as it’s not a general purpose language.)

by Edward Z. Yang at September 05, 2025 02:01 PM

Better Haskell stack traces via user annotations

Getting an accurate and precise backtrace is the key to debugging unexpected exceptions in Haskell programs. We recently implemented a family of functions that enable the user to push user-defined annotations to the native Haskell stack. The native stack decoder can display this information to the user when an unexpected exception is thrown.

This facility offers a number of advantages over the existing backtrace collection mechanisms:

• It is not necessary modify the function API (unlike HasCallStack)
• A “continuous chain” of modifications is not necessary (unlike HasCallStack)
• The annotations work in all ways of compilation (unlike cost centre stacks)
• The backtrace is expressed in terms of predictable source locations (unlike some IPE backtraces)

In this post we wil introduce the API for stack annotation, give some examples of how to use the annotation functions and discuss some trade-offs we have noticed with the design.

We’re interested in feedback from users on this feature. We’re expecting it to be available from GHC 9.16, as our implementation already landed in GHC HEAD (!14538).

Annotation stack frames

The core of the design is a new primop, annotateStack#, which when executed pushes an “annotation stack-frame” to the stack. Semantically, the frame is a no-op, but the payload contains a pointer to an arbitrary user-defined annotation. When decoding the native Haskell stack the annotation can be rendered to provide the user with additional context about the current location of the program.

The primop annotateStack# is exposed to the user via an IO-based API in GHC.Stack.Annotation.Experimental from the ghc-experimental package:¹

annotateStackIO :: (Typeable a, StackAnnotation a) => a -> IO b -> IO b

This will push the annotation value a onto the stack for the duration of the IO b action. The constraints allow the value to be rendered to a string or have its type inspected, similarly to the Exception class.

There are also specialised variants:

annotateCallStackIO   :: HasCallStack => IO b -> IO b  -- Annotate with the current source location
annotateStackStringIO :: String       -> IO b -> IO b  -- Annotate with an arbitrary String
annotateStackShowIO   :: Show a => a  -> IO b -> IO b  -- Annotate with the result of 'show' on a value

In addition, there are “pure” variants for use in non-IO code. However, these tend to be less intuitive due to the combination of lazy evaluation and imprecise exceptions, so the IO versions will generally produce better stack traces more reliably.

Note, annotateStack# is heavily inspired by annotated-exception and can be used together with annotated-exception for even better stack traces.

Example of the status quo

Let’s use the annotation functions to improve the backtrace for a program reported in a GHC ticket (#26040). The program implements a simple REST API using servant. When the endpoint is requested with a parameter which is larger than or equal to 100, the endpoint will error. topHandler catches all exceptions thrown by the handler and turns them into an HTTP 505 error. Finally, the exception handler prints any exceptions that might be thrown by the endpoint.

main :: IO ()
main = do
  setBacktraceMechanismState IPEBacktrace True
  run 8086 mkServer

type Api = Capture "x" Int :> Get '[PlainText] Text

mkServer :: Application
mkServer =
  serve
    (Proxy @Api)
    (hoistServer (Proxy @Api) topHandler api)

topHandler :: IO a -> Handler a
topHandler action = do
  result <- liftIO $
    (Right <$> action) `catch` \(exc :: SomeException) -> do
      liftIO $ putStrLn $ "Exception: " <> displayExceptionWithInfo exc
      pure $ Left err500

  either throwError pure result

api :: ServerT Api IO
api = handler

handler :: Int -> IO Text
handler x =
  if x >= 100
    then throw $ ErrorCall "Oh no!"
    else pure (pack "handler")

With the current version of GHC, when calling this API via http://localhost:8086/105, this stack trace is printed:

Exception: ghc-internal:GHC.Internal.Exception.ErrorCall:

Oh no!

IPE backtrace:
  Main.liftIO (src/Servant/Server/Internal/Handler.hs:30:36-42)
  Servant.Server.Internal.Delayed.runHandler' (src/Servant/Server/Internal/Handler.hs:27:31-41)
  Control.Monad.Trans.Resource.runResourceT (./Control/Monad/Trans/Resource.hs:(192,14)-(197,18))
  Network.Wai.Handler.Warp.HTTP1.processRequest (./Network/Wai/Handler/Warp/HTTP1.hs:195:20-22)
  Network.Wai.Handler.Warp.HTTP1.processRequest (./Network/Wai/Handler/Warp/HTTP1.hs:(195,5)-(203,31))
  Network.Wai.Handler.Warp.HTTP1.http1server.loop (./Network/Wai/Handler/Warp/HTTP1.hs:(141,9)-(157,42))
HasCallStack backtrace:
  collectExceptionAnnotation, called at libraries/ghc-internal/src/GHC/Internal/Exception.hs:170:37 in ghc-internal:GHC.Internal.Exception
  toExceptionWithBacktrace, called at libraries/ghc-internal/src/GHC/Internal/Exception.hs:90:42 in ghc-internal:GHC.Internal.Exception
  throw, called at app/Main.hs:42:10 in backtrace-0.1.0.0-inplace-server:Main

In this example there are two different backtraces:

• The “IPE backtrace” is constructed by decoding the Haskell stack, using information stored in the binary by -finfo-table-map, where each frame is automatically associated with a source location. (The compiler option -finfo-table-map was originally introduced for profiling.)
• On the the other hand, the “HasCallStack backtrace” is built using the implicitly passed HasCallStack constraints, which are automatically supplied by the type-checker, provided HasCallStack appears in the type.

The HasCallStack backtrace seems the most useful, telling us exactly where our program went wrong. However, the backtrace is very brief, as the rest of the program doesn’t have any HasCallStack constraints. As such, this stack trace might be unhelpful in larger programs, if the call to error was placed behind many layers of abstraction.

The IPE backtrace looks impressive, but doesn’t even show us where the exception is thrown! We get more intermediate source locations, but not the source of the exception. The function from which the exception is thrown is not even listed.

The reason the IPE backtrace may be unhelpful lies in the way the Haskell call stack works. We show the IPE info for each stack frame, which doesn’t relate precisely to the original source code and the resulting stack trace feels unintuitive. One reason for this is many function calls are tail-calls which don’t result in stack frames.

For more of an overview of the different backtrace mechanisms consult the discussion section of GHC Proposal #330.

Better stack traces with annotateCallStackIO

The IPE backtrace can be improved by manually annotating important parts of the program which should always appear in a backtrace.

For example, we always want to know in which handler the exception was thrown in, so the handler function is annotated with annotateCallStackIO. Further, we annotate the location where the exception is thrown.

handler :: Int -> IO Text
handler x = annotateCallStackIO $ do
  if x >= 100
    then annotateCallStackIO $ throw $ ErrorCall "Oh no!"
    else pure (pack "handleIndex")

When running this program again, the stack trace will now contain the source location of the handler where exception was thrown from:

Exception: ghc-internal:GHC.Internal.Exception.ErrorCall:

Oh no!

IPE backtrace:
  annotateCallStackIO, called at app/Main.hs:42:10 in backtrace-0.1.0.0-inplace-server:Main
  annotateCallStackIO, called at app/Main.hs:40:13 in backtrace-0.1.0.0-inplace-server:Main
  Main.handler (app/Main.hs:(40,1)-(43,30))
  Main.liftIO (src/Servant/Server/Internal/Handler.hs:30:36-42)
  Servant.Server.Internal.Delayed.runHandler' (src/Servant/Server/Internal/Handler.hs:27:31-41)
  Control.Monad.Trans.Resource.runResourceT (./Control/Monad/Trans/Resource.hs:(192,14)-(197,18))
  Network.Wai.Handler.Warp.HTTP1.processRequest (./Network/Wai/Handler/Warp/HTTP1.hs:195:20-22)
  Network.Wai.Handler.Warp.HTTP1.processRequest (./Network/Wai/Handler/Warp/HTTP1.hs:(195,5)-(203,31))
  Network.Wai.Handler.Warp.HTTP1.http1server.loop (./Network/Wai/Handler/Warp/HTTP1.hs:(141,9)-(157,42))
HasCallStack backtrace:
  collectExceptionAnnotation, called at libraries/ghc-internal/src/GHC/Internal/Exception.hs:170:37 in ghc-internal:GHC.Internal.Exception
  toExceptionWithBacktrace, called at libraries/ghc-internal/src/GHC/Internal/Exception.hs:90:42 in ghc-internal:GHC.Internal.Exception
  throw, called at app/Main.hs:42:32 in backtrace-0.1.0.0-inplace-server:Main

Note the first two entries of the IPE backtrace:

annotateCallStackIO, called at app/Main.hs:42:10 in backtrace-0.1.0.0-inplace-server:Main
annotateCallStackIO, called at app/Main.hs:40:13 in backtrace-0.1.0.0-inplace-server:Main

These have been added due to our manual annotation of our source program via annotateCallStackIO!

They give us precise source location where the exception is thrown, making the IPE backtrace just as useful as the HasCallStack backtrace. However, note, we did not have to change the type signature of handler at all to get a much more informative stack trace.

throwIO vs throw vs error

Some readers may have noticed that we used throw instead of error, which is usually the go to function for throwing example errors (or from within pure code). At the moment, throw and error produce noticeably different stack traces, because error evaluates the exception annotations lazier than throw, which leads to failing to capture the call stack when throwing the exception. This should be possible to resolve; see GHC issue #25430.

On the other hand, throwIO behaves more predictably within IO code and the IPE backtrace includes the source location of the exception throwing:

IPE backtrace:
  Main.handler (app/Main.hs:42:10-45)
  Main.liftIO (src/Servant/Server/Internal/Handler.hs:30:36-42)
  Servant.Server.Internal.Delayed.runHandler' (src/Servant/Server/Internal/Handler.hs:27:31-41)
  Control.Monad.Trans.Resource.runResourceT (./Control/Monad/Trans/Resource.hs:(192,14)-(197,18))
  Network.Wai.Handler.Warp.HTTP1.processRequest (./Network/Wai/Handler/Warp/HTTP1.hs:195:20-22)
  Network.Wai.Handler.Warp.HTTP1.processRequest (./Network/Wai/Handler/Warp/HTTP1.hs:(195,5)-(203,31))
  Network.Wai.Handler.Warp.HTTP1.http1server.loop (./Network/Wai/Handler/Warp/HTTP1.hs:(141,9)-(157,42))

This means that how the exception is thrown is important to get reasonable stack traces. Unsurprisingly, you should use throwIO whenever you are within the IO monad.

Summary

Annotation stack frames are a lightweight way to add extra information to stack traces. By modifying the execution stack, the information is always available and can be used by the native stack decoder to display informative backtraces to users. We’re interested to hear what users think about this feature and how libraries will be adapted to take advantage of the new annotation frames.

This work has been performed in collaboration with Mercury, who have a long-term commitment to the scalability and robustness of the Haskell ecosystem. Well-Typed are always interested in projects and looking for funding to improve GHC and other Haskell tools. Please contact info@well-typed.com if we might be able to work with you!

---

1. The ghc-experimental package ships with GHC, but is distinct from base, and has weaker stability guarantees. This allows new APIs to be introduced and fine-tuned before eventually being stabilised and added to base.↩︎

by hannes, matthew at September 04, 2025 12:00 AM

Introduction to the dependency graph

A dependency graph is a representation of how different parts of a software project rely on each other. Understanding the dependency graph helps a software engineer see the bigger picture of how their component fits into the whole project and why certain changes might affect other areas. It’s a useful tool for organizing, debugging, and improving the source code.

Engineers responsible for managing the development and build environments also benefit greatly from understanding dependency graph concepts and how they are used by the build system. This knowledge is crucial for optimizing build times since it allows engineers to identify opportunities to parallelize and improve the incrementality of builds. Understanding the dependency graph also helps in troubleshooting build failures, managing changes safely, and ensuring that updates or refactors do not worsen the overall design of the codebase.

In this blog post, we’ll take a fresh look at dependency graphs, starting from the basic concepts and building up from there. You will learn what a dependency graph is, some terminology required to be successful in managing it, and what it is used for.

What is a dependency graph?

A dependency graph is a visual map that explains the connectivity between parts of a software project.

Let’s use a contrived example of a dependency graph in a tiny codebase and lay out some key terminology.

Nodes and edges

A node in a dependency graph represents an individual item which can be a software package, a module, or a component.

The edges (connections) between nodes represent dependencies, meaning one node relies on another to function or build correctly.

Dependencies

appA depends on libX directly therefore libX is a direct dependency of appA. For example, if you import the requests package in your Python module, this would be that module’s direct dependency.

appB depends on commons via libY therefore commons is a transitive dependency of appB. For example, if your C++ program depends on libcurl, then it also depends (transitively) on every external library that libcurl depends on such as OpenSSL or zlib.

Dependents

libX and libY directly depend on commons. This could also be reversed — commons has two direct dependents: libX and libY. In fact, the dependents are often called reverse dependencies. Similarly, secrets have two reverse dependencies: one direct - appB, and one transitive - testB.

Shape and orientation

A simple dependency graph can sometimes look like a tree, with one common base component at the root, supporting multiple dependents (components pointing back towards the root), which in turn are depended on by the leaves (components with no further dependents).

However, dependency graphs are usually more complex than trees and belong to a more general family of graphs known as directed acyclic graphs (DAG), where you can only follow the arrows in one direction, and you can never end up back at the same node you started from. We’ll talk about the word “acyclic” in more detail later in the post.

When describing this project, we could emphasize that commons is foundational - the root that everything else builds upon. Libraries and apps become the trunk and branches, with tests as leaves. Without clearly defining how arrows show dependencies, we might easily draw all arrows pointing the opposite way (a reverse dependency graph¹):

This makes terms like “roots” or “leaves” potentially confusing, but it’s important to be aware of them as you will likely hear them being used when talking about graphs.

What is it used for?

Dependency graph concepts have lots of applications:

• Dependency resolution techniques such as Minimal Version Selection and Backtracking are used by package managers.

• In artifact-based build systems such as Bazel, a dependency graph is used to determine the order in which different parts of a project should be built. Having access to this allows building only what is necessary and in the correct sequence.

• GNU Make uses a dependency graph implicitly through its rules: each target specifies its dependencies, and Make constructs a graph to determine the order in which to build targets.

• Native programming language build tools use the dependency graph to fetch and build modules in the correct order, e.g., in Go, it is used to maintain a cache of passing test results (where go test checks whether any of the transitive dependencies of the tests have changed since the last run).

Graph theory applications

Graph theory is a branch of mathematics focused on networks of connected items. Understanding some graph theory ideas can make managing dependencies much smarter. Being familiar with the terminology also helps to find relevant tooling, for instance, knowing that part of the graph is called subgraph would let you find more relevant results when searching for algorithms to extract a part of the graph.

Connected Components

A connected component is a group of nodes where each one can reach every other by following edges in either direction. In a dependency graph, this means a set of source code modules that are all linked together by a dependency link (or a reverse dependency link) — what’s important is that there is some sort of connection.

When two applications share modules in the same connected component, they become indirectly connected which might make it hard to test or deploy them separately. In a worse scenario, if the modules of these apps actually import from each other, then code changes in one app can unexpectedly break another. Applications with isolated dependencies are much easier to extract and move to separate repositories.

In the example below, the configuration is shared among three applications making them part of the same connected component. That is, you can’t move any of the applications along with the shared configuration out of the codebase. This could be refactored by splitting the shared configuration into separate configurations for each application.

Making changes specific to the appA in the shared-config no longer triggers rebuilds of all applications and running all their tests.

One connected component:

Three connected components:

Isolated nodes (nodes that don’t have any edges connected) also are connected components which may represent software units that are no longer needed. For instance, a program might have once used a third-party library, but later stopped using its functionality. If nothing else in the codebase depends on that library, it is now isolated, and can be removed to avoid rebuilding.

Cut Points and Bridges

A cut point (also called a “point of connection” or “articulation point”) is a node that, if removed, would split the graph into separate components. A bridge is an edge whose removal would produce a new connected component.

In the example below, if we stop depending on the third-party library third-party-lib, we would stop depending transitively on all those third-party libraries that third-party-lib brought into the dependency graph of our project.

To remove a “cut point” like third-party-lib, you can replace its functionality with an existing dependency or reimplement it yourself. This can make builds faster (fewer downloads), more secure, and more reliable. The npm left-pad incident shows how third-party dependencies can cause problems.

Creating isolated groups in the dependency graph is often a good thing as it means those modules can now evolve, be tested, and deployed independently, reducing risk and complexity. However, in a large dependency graph, the hard part is to identify the best cut points as often breaking the dependency between two modules might still leave the part of the dependency graph you are concerned about connected to the rest of the codebase.

Breaking appA -> config1 (incorrectly assuming that this as a bridge) would still leave appA connected to the rest of the codebase via the libX connection. To identify that libX might still lead to the rest of the codebase via a chain of connections is not trivial and to be able to refactor the dependency graph so that one can reason about it, it is often required to use advanced dependency graph querying and visualization tooling. To estimate how much work it would be to break a connection, one can list all paths between your module and the undesired dependency, which will be discussed later.

Subgraphs

A subgraph is just a smaller part of the whole graph, focusing on a subset of nodes and their connections. Depending on the complexity and shape of your dependency graph, it might only make sense to interact with a subgraph of it. Take a look at the dependency graphs of the microservices at tech giants to appreciate the complexity of their dependency management.

Visualizing or analyzing a subgraph (e.g., all dependencies of a single service) helps you zoom in on what matters for your project. If the dependencies of a program are complicated, it may make sense to extract only its direct dependencies and their direct dependencies. In graph theory terms, this means focusing on nodes that are at most two degrees away from the program node. The degree of a node refers to the number of direct connections (dependencies) it has. We can extract a subgraph by limiting our view to nodes within a certain depth (in this case, a depth of two). By controlling the depth, you avoid being overwhelmed by the entire transitive chain of dependencies.

With the same dependency graph we had seen in the very first graph of the post,

we can extract the subgraph containing dependencies with depth of 2 for appB:

Transitivity

The transitive closure of a node in a graph is the set of all nodes that can be reached from that node by following edges. In the context of a dependency graph, the transitive closure² of a module is the entire “tree” of things required for that module to work.

In this dependency graph,

both appA and appB depend on secrets (directly) and cloud (directly and transitively). In this cluttered visualization of the graph, the direct dependency edge between appA/appB and cloud could be removed for clarity as we already know that they are connected:

The process of simplifying the graph by removing edges that are implied by other edges is called transitive reduction. Keep in mind that you would not normally want to do this for any other reason than clearer visualization of the graph.

If your build tool tracks node dependencies by reading build metadata (stored in files maintained by engineers), this information must stay up-to-date so the build system can correctly identify necessary build steps. Imagine that at some point in time appA used to import some code from cloud, however, after some refactoring, it doesn’t depend on it directly any longer:

Now, what if in the build metadata files, the direct dependencies of appA are still [cloud, secrets]? The stale build metadata information such as a redundant declaration of the direct dependency won’t be an issue from the build systems perspective: cloud will ultimately end up in the transitive closure of appA.

However, if after further refactorings, appA no longer depends on secrets, we end up with this graph used by the build system:

Since appA depends on cloud, it becomes dependent on the transitive closure of cloud which might lead to slower build times (all resources that cloud depends on now need to be downloaded to build appA).

Paths

Finding paths between arbitrary modules in a dependency graph helps understand how different parts of your system are connected. In this context, we are primarily interested in finding simple paths — paths where all nodes visited are distinct.

By finding a path from module A to module B, you can see if changes in A might affect B (or vice versa). This helps estimate the risk of changes and debug issues that propagate through dependencies. For example, if a module contains source code under a specific license, you might want to ensure no paths from applications with incompatible licenses lead to it, preventing its inclusion in the application bundle.

With this contrived example of a dependency graph,

there are two paths from appA to commons:

• appA -> libX -> libY -> commons
• appA -> secrets -> commons

In a large, highly connected dependency graph, there may be hundreds of paths between two modules.

When listing paths, shortest paths help to understand the minimal set of dependencies connecting two modules. In contrast, the longest path between two modules tells you how deep the dependency chains are. The higher the average number of nodes in all paths in the graph, the more interconnected your codebase is. Having a very interconnected dependency graph might be problematic because it becomes hard to reason about how changes will propagate and a change in a low-level module can ripple through many layers, increasing the risk of unexpected breakages.

Topological sort

Topological sort (or order) is a way of ordering the nodes in a dependency graph so that every node comes after all the nodes it depends on. A build system might use topological sort to determine what must be built first and which targets can be built in parallel.

Having access to this contrived dependency graph,

and oversimplifying what a modern build system would do with this dependency graph, we could produce a parallelizable list of build actions.

In order to build a particular node (say, produce a binary executable), we need to first build all nodes that this node depends on (transitively). For instance, let’s say we want to build appA:

1. To build appA, we need to first build its direct dependency, libX.
2. To build libX, we need to first build its direct dependencies, commons and secrets.
3. commons and secrets can be built immediately as they do not have any dependencies.

This means that our dependency graph nodes would be sorted like this:

[secrets,commons],libX,appA

secrets and commons can be built in parallel, and once both of them are built, we can start building libX, and, thereafter, appA.

Parallelism emerges only when the graph has branches, that is, multiple independent subgraphs that can be built concurrently once their dependencies are satisfied. Practically, this means that flattening overly nested or serial dependencies can unlock better parallelism leading to faster builds.

In an extreme case, if your graph is in the shape of a linked list such as app -> lib -> secrets -> commons, no parallelism can be achieved because every node would need to wait for its dependency to be built first. However, even when components must be built sequentially due to their dependencies, parallelism can still occur within each component, for instance, compiling multiple source files simultaneously within a single library.

Cycles

Cycles in a dependency graph mean that some components depend on each other in a loop, making it impossible to determine the order in the dependency chain. Build systems like Bazel require the dependency graph to be a directed graph without cycles (commonly known as Directed Acyclic Graph, or DAG) because cycles would lead to infinite build loops and prevent the system from knowing which component to build first.

With this graph having a cycle (libA -> libB -> libC), it is unclear in what order dependencies of app should be built:

When adopting a build system that needs to construct a DAG out of your dependency graph, you might need to make refactorings in the codebase to break cycles. This is particularly true for legacy codebases written in Python, JavaScript, or Ruby where native build tools might tolerate cycles in the dependency graph.

A DAG is a very common data structure used by various build systems such as Bazel, Pants, and Buck2, process orchestration software such as Dagster, Flyte, and AirFlow, and software engineering tooling such as Git.

---

In this post, we have reviewed the basic principles related to graph theory and talked about dependency graphs that consist of modules in a codebase. In sophisticated build systems, you’ll find that more kinds of graphs exist, with differences between them. In Bazel, there is a build graph (what we have called dependency graph in this post for simplicity) and an action graph that breaks down each component into specific actions (like compiling a file or generating code) that need to be executed. There are some more advanced kinds of graphs you might run into such as the evaluation graph (Skyframe graph) representing Bazel’s internal state (see skyscope to learn more) and the shadow dependency graph which is created when aspects are used.

In the next blog post, we will cover common problems associated with managing project dependencies and share best practices for keeping a large dependency graph healthy over time.

---

1. The reversed dependency graph concept is useful in scenarios like impact analysis (e.g., “If changes are made to this core library, what other components will be affected?”).↩
2. You won’t see this term often, but the transitive closure that also includes the node itself from which we start the search is called a reflexive transitive closure.↩

September 04, 2025 12:00 AM

F91 in Lean

Back in March, with version 4.17.0, Lean introduced partial_fixpoint, a new way to define recursive functions. I had drafted a blog post for the official Lean FRO blog back then, but forgot about it, and with the Lean FRO blog discontinued, I’ll just publish it here, better late than never.

With the partial_fixpoint mechanism we can model possibly partial functions (so those returning an Option) without an explicit termination proof, and still prove facts about them. See the corresponding section in the reference manual for more details.

On the Lean Zulip, I was asked if we can use this feature to define the McCarthy 91 function and prove it to be total. This function is a well-known tricky case for termination proofs.

First let us have a brief look at why this function is tricky to define in a system like Lean. A naive definition like

def f91 (n : Nat) : Nat :=
  if n > 100
  then n - 10
  else f91 (f91 (n + 11))

does not work; Lean is not able to prove termination of this functions by itself.

Even using well-founded recursion with an explicit measure (e.g. termination_by 101 - n) is doomed, because we would have to prove facts about the function’s behaviour (namely that f91n = f91101 = 91 for 90 ≤ n ≤ 100) and at the same time use that fact in the termination proof that we have to provide while defining the function. (The Wikipedia page spells out the proof.)

We can make well-founded recursion work if we change the signature and use a subtype on the result to prove the necessary properties while we are defining the function. Lean by Example shows how to do it, but for larger examples this approach can be hard or tedious.

With partial_fixpoint, we can define the function as a partial function without worrying about termination. This requires a change to the function’s signature, returning an Option Nat:

def f91 (n : Nat) : Option Nat :=
  if n > 100
    then pure (n - 10)
    else f91 (n + 11) >>= f91
partial_fixpoint

From the point of view of the logic, Option.none is then used for those inputs for which the function does not terminate.

This function definition is accepted and the function runs fine as compiled code:

#eval f91 42

prints some 91.

The crucial question is now: Can we prove anything about f91 In particular, can we prove that this function is actually total?

Since we now have the f91 function defined, we can start proving auxillary theorems, using whatever induction schemes we need. In particular we can prove that f91 is total and always returns 91 for n ≤ 100:

theorem f91_spec_high (n : Nat) (h : 100 < n) : f91 n = some (n - 10) := by
  unfold f91; simp [*]

theorem f91_spec_low (n : Nat) (h₂ : n ≤ 100) : f91 n = some 91 := by
  unfold f91
  rw [if_neg (by omega)]
  by_cases n < 90
  · rw [f91_spec_low (n + 11) (by omega)]
    simp only [Option.bind_eq_bind, Option.some_bind]
    rw [f91_spec_low 91 (by omega)]
  · rw [f91_spec_high (n + 11) (by omega)]
    simp only [Nat.reduceSubDiff, Option.some_bind]
    by_cases h : n = 100
    · simp [f91, *]
    · exact f91_spec_low (n + 1) (by omega)

theorem f91_spec (n : Nat) : f91 n = some (if n ≤ 100 then 91 else n - 10) := by
  by_cases h100 : n ≤ 100
  · simp [f91_spec_low, *]
  · simp [f91_spec_high, Nat.lt_of_not_le ‹_›, *]

-- Generic totality theorem
theorem f91_total (n : Nat) : (f91 n).isSome := by simp [f91_spec]

(Note that theorem f91_spec_low is itself recursive in a somewhat non-trivial way, but Lean can figure that out all by itself. Use termination_by? if you are curious.)

This is already a solid start! But what if we want a function of type f91! (n : Nat) : Nat, without the Option? Then can derive that from the partial variant, as we have just proved that to be actually total:

def f91! (n : Nat) : Nat  := (f91 n).get (f91_total n)

theorem f91!_spec (n : Nat) : f91! n = if n ≤ 100 then 91 else n - 10 := by
  simp [f91!, f91_spec]

Using partial_fixpoint one can decouple the definition of a function from a termination proof, or even model functions that are not terminating on all inputs. This can be very useful in particular when using Lean for program verification, such as with the aeneas package, where such partial definitions are used to model Rust programs.

by Joachim Breitner (mail@joachim-breitner.de) at September 03, 2025 08:18 PM

Starting out with Graph Algorithms: Basic DFS

For a few weeks now, we’ve been tackling problems related to data structures, with a sprinkling of algorithmic ideas in there. Last week, we covered sets and heaps. Prior to that, we considered Matrices and the binary search algorithm.

This week, we’ll cover our first graph problem! Graph problems often build on a lot of fundamental layers. You need to understand the algorithm itself. Then you need to use the right data structures to apply it. And you’ll also still need the core problem solving patterns at your disposal. These 3 areas correspond to the first 3 modules of Solve.hs, our Haskell problem solving course! Check out that course to level up your Haskell skills!

The Problem

Today’s problem is called Number of Islands. We are given a 2D array as input, where every cell is either “land” or “sea” (either represented as the characters 1 and 0, or True and False). We want to find the number of distinct islands in this grid. Two “land” cells are part of the same island if we can draw a path from one cell to the other that only uses other land cells and other travels up, down, left and right (but not diagonally).

Let’s suppose we have this example:

111000
100101
100111
110000
000110

This grid has 3 islands. The island in the top left corner comprises 7 connected cells. Then there’s a small island in the bottom right with only 2 cells. Finally, we have a third island in the middle right with 5 tiles. While it is diagonally adjacent to the first island, we do not count this as a connection.

The Algorithm

This is one of the most basic questions you’ll see that requires a graph search algorithm, like Depth-First-Search (DFS) or Breadth-First-Search (BFS). The basic principle is that we will select a starting coordinate for a search. We will use one of these algorithms to find all the land cells that are part of that cell’s island. We’ll then increment a counter for having found this island.

We need to track all the cells that are part of this island. We’ll then keep iterating for new start locations to find new islands, but we have to exclude any locations that have already been explored.

While BFS is certainly possible, the solutions we’ll write here will use DFS. Our solution will consist of 3 components:

1. A “neighbors” function that finds all adjacent land tiles to a given tile.
2. A “visit” function that will take a starting coordinate and populate a “visited” set with all of the cells on the same island as the starting coordinate.
3. A core “loop” that will consider each coordinate as a possible starting value for an island.

This ordering represents more of a “bottom up” approach to solving the problem. Going “top down” also works, and may be easier if you’re unfamiliar with graph algorithms. But as you get more practice with them, you’ll get a feel for knowing the bottom layers you need right away.

Rust Solution

To write our solution, we’ll write the components in our bottom up order. We’ll start with our neighbors function. This will take the island grid (LeetCode supplies us with a Vec<Vec<char>>) and the current location. We’ll represent locations as tuples, (usize, usize). This function will return a vector of locations.

use std::collections::HashSet;

pub fn neighbors(
        grid: &Vec<Vec<char>>,
        loc: &(usize,usize)) -> Vec<(usize,usize)> {
    ...
}

We’ll start this function by defining a few values. We want to know the length and width of the grid, as well as defining r and c to quickly reference the current location.

use std::collections::HashSet;

pub fn neighbors(
        grid: &Vec<Vec<char>>,
        loc: &(usize,usize)) -> Vec<(usize,usize)> {
    let m = grid.len();
    let n = grid[0].len();
    let r = loc.0;
    let c = loc.1;
    let mut result: Vec<(usize,usize)> = Vec::new();
    ...
}

Now we just have to look in each of the four directions. Each direction is included as long as it is a land tile and that it is not out of bounds. We’ll do our “visited” checks elsewhere.

pub fn neighbors(
        grid: &Vec<Vec<char>>,
        loc: &(usize,usize)) -> Vec<(usize,usize)> {
    let m = grid.len();
    let n = grid[0].len();
    let r = loc.0;
    let c = loc.1;
    let mut result: Vec<(usize,usize)> = Vec::new();
    if (r > 0 && grid[r - 1][c] == '1') {
        result.push((r - 1, c));
    }
    if (c > 0 && grid[r][c - 1] == '1') {
        result.push((r, c - 1));
    }
    if (r + 1 < m && grid[r + 1][c] == '1') {
        result.push((r + 1, c));
    }
    if (c + 1 < n && grid[r][c + 1] == '1') {
        result.push((r, c + 1));
    }
    return result;
}

Now let’s write the visit function. Remember, this function’s purpose is to populate the visited set starting from a certain location. We’ll use a HashSet of tuples for the visited set.

pub fn visit(
        grid: &Vec<Vec<char>>,
        visited: &mut HashSet<(usize,usize)>,
        loc: &(usize,usize)) {
    ...
}

First, we’ll check if this location is already visited and return if so. Otherwise we’ll insert it.

pub fn visit(
        grid: &Vec<Vec<char>>,
        visited: &mut HashSet<(usize,usize)>,
        loc: &(usize,usize)) {
    if (visited.contains(loc)) {
        return;
    visited.insert(*loc);
    ...
}

All we have to do now is find the neighbors of this location, and recursively “visit” each one of them!

pub fn visit(
        grid: &Vec<Vec<char>>,
        visited: &mut HashSet<(usize,usize)>,
        loc: &(usize,usize)) {
    if (visited.contains(loc)) {
        return;
    }
    visited.insert(*loc);
    let ns = neighbors(grid, visited, loc);
    for n in ns {
        visit(grid, &n);
    }
}

We’re not quite done, as we have to loop through our grid to call this function on each possible start. This isn’t so bad though. We start our function by defining key terms.

pub fn num_islands(grid: Vec<Vec<char>>) -> i32 {
    let m = grid.len();
    let n = grid[0].len();
    let mut visited: HashSet<(usize,usize)> = HashSet::new();
    let mut islandCount = 0;
    ...
    // islandCount will be our final result
    return islandCount;
}

Now we’ll “loop” through each possible starting location:

pub fn num_islands(grid: Vec<Vec>) -> i32 { let m = grid.len(); let n = grid[0].len(); let mut visited: HashSet<(usize,usize) data-preserve-html-node="true"> = HashSet::new(); let mut islandCount = 0; for row in 0..m { for col in 0..n { ... } // islandCount will be our final result return islandCount; }

The last question is, what do we do for each location? If the location is land AND it is still unvisited, we treat it as the start of a new island. This means we increase the island count and then “visit” the location. When we consider other cells on this island, they’re already visited, so we won’t increase the island count when we find them!

```rust
pub fn num_islands(grid: Vec<Vec<char>>) -> i32 {
    let m = grid.len();
    let n = grid[0].len();
    let mut visited: HashSet<(usize,usize)> = HashSet::new();
    let mut islandCount = 0;
    for row in 0..m {
        for col in 0..n {
            islandCount += 1;
            visit(&grid, &mut visited, &loc);
        }
    return islandCount;
}

Here’s our complete solution:

use std::collections::HashSet;

pub fn neighbors(
        grid: &Vec<Vec<char>>,
        loc: &(usize,usize)) -> Vec<(usize,usize)> {
    let m = grid.len();
    let n = grid[0].len();
    let r = loc.0;
    let c = loc.1;
    let mut result: Vec<(usize,usize)> = Vec::new();
    if (r > 0 && grid[r - 1][c] == '1') {
        result.push((r - 1, c));
    }
    if (c > 0 && grid[r][c - 1] == '1') {
        result.push((r, c - 1));
    }
    if (r + 1 < m && grid[r + 1][c] == '1') {
        result.push((r + 1, c));
    }
    if (c + 1 < n && grid[r][c + 1] == '1') {
        result.push((r, c + 1));
    }
    return result;
}

pub fn visit(
        grid: &Vec<Vec<char>>,
        visited: &mut HashSet<(usize,usize)>,
        loc: &(usize,usize)) {
    if (visited.contains(loc)) {
        return;
    }
    visited.insert(*loc);
    let ns = neighbors(grid, visited, loc);
    for n in ns {
        visit(grid, &n);
    }
}


pub fn num_islands(grid: Vec<Vec<char>>) -> i32 {
    let m = grid.len();
    let n = grid[0].len();
    let mut visited: HashSet<(usize,usize)> = HashSet::new();
    let mut islandCount = 0;
    for row in 0..m {
        for col in 0..n {
            let loc: (usize,usize) = (row,col);
            if grid[row][col] == '1' && !(visited.contains(&loc)) {
                islandCount += 1;
                visit(&grid, &mut visited, &loc);
            }
        }
    }
    return islandCount;
}

Haskell Solution

The structure of this solution translates well to Haskell, since it’s a recursive solution at its root. We’ll just use a couple of folds to handle the other loops. Let’s outline the solution:

numberOfIslands :: A.Array (Int, Int) Bool -> Int
numberOfIslands grid = ...
  where
    ((minRow, minCol), (maxRow, maxCol)) = A.bounds grid

    neighbors :: (Int, Int) -> [(Int, Int)]

    visit :: (Int, Int) -> HS.HashSet (Int, Int) -> HS.HashSet (Int, Int)

    loop :: (Int, Int) -> (Int, HS.HashSet (Int, Int)) -> (Int, HS.HashSet (Int, Int))

Since we’re writing our functions “in line”, we don’t need to pass the grid around like we did in our Rust solution (though inline functions are also possible there). What you should observe immediately is that visit and loop have a similar structure. They both fit into the a -> b -> b pattern we want for foldr! We’ll use this to great effect!

But first, let’s fill in neighbors. Each of the 4 directions requires the same two conditions we used before. We make sure it’s not out of bounds, and that the next tile is “land”. Here’s how we check the “up” direction:

numberOfIslands :: A.Array (Int, Int) Bool -> Int
numberOfIslands grid = ...
  where
    ((minRow, minCol), (maxRow, maxCol)) = A.bounds grid

    neighbors :: (Int, Int) -> [(Int, Int)]
    neighbors (row, col) = 
      let up =  if row > minRow && grid A.! (row - 1, col) then Just (row - 1, col) else Nothing
      ...

We return Nothing if it is not a valid neighbor. Then we just combine the four directional options with catMaybes to complete this helper:

numberOfIslands :: A.Array (Int, Int) Bool -> Int
numberOfIslands grid = ...
  where
    ((minRow, minCol), (maxRow, maxCol)) = A.bounds grid

    neighbors :: (Int, Int) -> [(Int, Int)]
    neighbors (row, col) = 
      let up =  if row > minRow && grid A.! (row - 1, col) then Just (row - 1, col) else Nothing
          left = if col > minCol && grid A.! (row, col - 1) then  Just (row, col - 1) else Nothing
          down = if row < maxRow && grid A.! (row + 1, col) then Just (row + 1, col) else Nothing
          right = if col < maxCol && grid A.! (row, col + 1) then Just (row, col + 1) else Nothing
      in  catMaybes [up, left, down, right]

Now we start the visit function by checking if we’ve already visited the location, and add it to the set if not:

numberOfIslands :: A.Array (Int, Int) Bool -> Int
numberOfIslands grid = ...
  where
    ((minRow, minCol), (maxRow, maxCol)) = A.bounds grid

    visit :: (Int, Int) -> HS.HashSet (Int, Int) -> HS.HashSet (Int, Int)
    visit coord visited = if HS.member coord visited then visited else
      let visited' = HS.insert coord visited
      ...

Now we have to get the neighbors and “loop” through the neighbors so that we keep the visited set updated. This is where we’ll apply our first fold. We’ll recursively fold over visit on each of the possible neighbors, which will give us the final visited set from this process. That’s all we need for this helper!

numberOfIslands :: A.Array (Int, Int) Bool -> Int
numberOfIslands grid = ...
  where
    ((minRow, minCol), (maxRow, maxCol)) = A.bounds grid

    visit :: (Int, Int) -> HS.HashSet (Int, Int) -> HS.HashSet (Int, Int)
    visit coord visited = if HS.member coord visited then visited else
      let visited' = HS.insert coord visited
      in  foldr visit visited’ ns

Now our loop function will consider only a single coordinate. We think of this as having two pieces of state. First, the number of accumulated islands (the Int). Second, we have the visited set. So we check if the coordinate is unvisited land. If so, we increase the count, and get our “new” visited set by calling visit on it. If not, we return the original inputs.

numberOfIslands :: A.Array (Int, Int) Bool -> Int
numberOfIslands grid = ...
  where
    loop :: (Int, Int) -> (Int, HS.HashSet (Int, Int)) -> (Int, HS.HashSet (Int, Int))
    loop coord (count, visited) = if grid A.! coord && not (HS.member coord visited)
      then (count + 1, visit coord visited)
      else (count, visited)

Now for the final flourish. Our loop also has the structure for foldr. So we’ll loop over all the indices of our array, which will give us the final number of islands and the visited set. Our final answer is just the fst of these:

numberOfIslands :: A.Array (Int, Int) Bool -> Int
numberOfIslands grid = fst (foldr loop (0, HS.empty) (A.indices grid))
  where

    loop :: (Int, Int) -> (Int, HS.HashSet (Int, Int)) -> (Int, HS.HashSet (Int, Int))

Here’s our final solution:

numberOfIslands :: A.Array (Int, Int) Bool -> Int
numberOfIslands grid = fst (foldr loop (0, HS.empty) (A.indices grid))
  where
    ((minRow, minCol), (maxRow, maxCol)) = A.bounds grid

    neighbors :: (Int, Int) -> [(Int, Int)]
    neighbors (row, col) = 
      let up =  if row > minRow && grid A.! (row - 1, col) then Just (row - 1, col) else Nothing
          left = if col > minCol && grid A.! (row, col - 1) then  Just (row, col - 1) else Nothing
          down = if row < maxRow && grid A.! (row + 1, col) then Just (row + 1, col) else Nothing
          right = if col < maxCol && grid A.! (row, col + 1) then Just (row, col + 1) else Nothing
      in  catMaybes [up, left, down, right]

    visit :: (Int, Int) -> HS.HashSet (Int, Int) -> HS.HashSet (Int, Int)
    visit coord visited = if HS.member coord visited then visited else
      let visited' = HS.insert coord visited
          ns = neighbors coord
      in  foldr visit visited' ns

    loop :: (Int, Int) -> (Int, HS.HashSet (Int, Int)) -> (Int, HS.HashSet (Int, Int))
    loop coord (count, visited) = if grid A.! coord && not (HS.member coord visited)
      then (count + 1, visit coord visited)
      else (count, visited)

A Note on the Graph Algorithm

It seems like we solved this without even really apply a “graph” algorithm! We just did a loop and a recursive call and everything worked out! There are a couple elements of this problem that make it one of the easiest graph problems out there.

Normally, we have to use some kind of structure to store a search state, telling us the next nodes in our graph to search. For BFS, this is a queue. For Dijkstra or A*, it is a heap. For DFS it is normally a stack. However, we are using the call stack to act as the stack for us!

When we make a recursive call to “visit” a location, we don’t need to keep track of which node we return to after we’re done. The function returns, and the prior node is already sitting there on the call stack.

The other simplifying factor is that we don’t need to do any backtracking or state restoration. Sometimes with a DFS, you need to “undo” some of the steps you took if you don’t find your goal. But this algorithm is just a space-filling algorithm. We are just trying to populate our “visited” set, and we never take nodes out of this set once we have visited them.

Conclusion

We’ve got a couple more graph problems coming up next. If you want to learn more about applying graph algorithms in Haskell (including implementing them for yourself!) check out Solve.hs, where Module 3 will teach you about algorithms including DFS, BFS, A* and beyond!

by James Bowen at September 01, 2025 08:30 AM

Alpha-beta pruning is just minimax in a lattice of clamping functions

A lazy take on a classic game theory algorithm.

Haskell extensions and imports used in this post

{-# LANGUAGE
  DataKinds,
  DeriveGeneric,
  DeriveTraversable,
  DerivingStrategies,
  GeneralizedNewtypeDeriving,
  RankNTypes,
  ScopedTypeVariables,
  StandaloneDeriving,
  TypeFamilies #-}

import Data.Ord (Down(Down, getDown))
import Data.List.NonEmpty (NonEmpty(..))
import qualified GHC.Generics as GHC
import Generics.SOP (Generic, HasDatatypeInfo, NP(..), K(..))
import Test.QuickCheck
import Test.StrictCheck

Minimax

Minimax is a general algorithm for finding optimal strategies. It’s not meant to be efficient or practical. It is more of a basic concept of game theory, and a reference against which to compare other game-solving algorithms.

We consider a simple model of two-player games. They take turns playing moves until reaching an end state with a final score. One player’s goal is to maximize the score, whereas the other player’s goal is to minimize it. Let us call these players Max and Min respectively, short for Maximizer and Minimizer.

We represent such a game by its game tree, which is made up of three constructors: a Max (resp. Min) node represents a game state where Max (resp. Min) chooses the next move, each move resulting in a new game state, and an End leaf represents an end state as its score.

data Game score
  = Max (NonEmpty (Game score))
  | Min (NonEmpty (Game score))
  | End score
  deriving stock (Show, Functor, Foldable)

Note that Max and Min nodes must have at least one possible move. You may be wondering about games that end when one player can no longer play: instead of an empty Min or Max node, such game states simply correspond to an End leaf, making the final score explicit.

Most real games just have a win/tie/lose end condition. They naturally correspond to applying Game to a type with three possible scores:

data WinLose = MinWins | Tie | MaxWins
  deriving (Eq, Ord, Show)

In practice, chess engines don’t work with the whole game tree since it is too massive. Instead, they build approximations by pruning certain branches of the tree and replacing them with leaves. The score on each leaf is a number which estimates how favorable the game state is to either player. So we end up with Game ℝ, or Game Double.

In general, the type Game represents two-player games with complete information and zero-sum objectives.

We shall assume that score is a totally ordered set. This requirement corresponds to a constraint Ord score in Haskell. In that case, there exists an “optimal strategy” for each player which guarantees them an “optimal score” m in the sense that as long as one player sticks to their “optimal strategy”, the other player cannot score better than m. This situation is what we call a Nash equilibrium in game theory. For win/tie/lose games, the existence of a Nash equilibrium means that either there is a winning strategy for one of the players, or they must tie by playing optimally.

The “optimal score” m is unique, and can be computed by a fold of the game tree, replacing Max and Min constructors with the functions maximum and minimum. This is the minimax algorithm:

minimax :: Ord score => Game score -> score
minimax (Max gs) = maximum (minimax <$> gs)
minimax (Min gs) = minimum (minimax <$> gs)
minimax (End s) = s

minimax is quite an inefficient algorithm: it must traverse the whole game tree. Indeed, maximum and minimum must traverse the whole list to find the maximum or minimum element.

Often, we can do much better. For instance, consider the following tree:

Max [ End 0,
      Min [ End (-1),
            t ] ]

The minimax of that tree does not depend on the subtree t. Indeed, minimum [-1, minimax t] is guaranteed to be at most -1, so the maximum between that value and 0 is guaranteed to be 0. Thus we can compute the minimax without inspecting the subtree t, which may be arbitrarily large. That idea leads to a more efficient algorithm to compute the minimax.

Alpha-beta

The alpha-beta pruning algorithm¹ is a modification of minimax with an extra pair of arguments:

alphabeta :: Ord score => Game score -> (score, score) -> score

The pair (alpha, beta) represents a “relevance interval” which relaxes the possible outputs of alphabeta. Either alphabeta t (alpha, beta) produces a score within that interval, in which case it is guaranteed to be equal to minimax. Otherwise, alphabeta t (alpha, beta) produces a value outside of the interval, in which case its exact value does not matter; it only has to be on the same side of the interval as minimax t. More rigorously:

• if alpha < minimax t < beta, then alphabeta t (alpha, beta) = minimax t;
• if minimax t <= alpha, then alphabeta t (alpha, beta) <= alpha;
• if beta <= minimax t, then beta <= alphabeta t (alpha, beta).

Leaving the value of alphabeta underspecified when outside of the interval allows the implementation to short-circuit: we can stop searching through Max nodes as soon as we can guarantee a score greater than beta, and we can stop searching through Min nodes as soon as we can guarantee a score smaller than alpha.

We can then use alphabeta to redefine minimax:

-- Minimax using alpha-beta pruning
minimaxAB :: (Ord score, Bounded score) => Game score -> score
minimaxAB t = alphabeta t (minBound, maxBound)

assuming that score is Bounded with extreme values minBound :: score and maxBound :: score. It’s possible to avoid the Bounded constraint by changing the interval type (score, score) to (Maybe score, Maybe score), which amounts to adding distinguished top and bottom elements. We’ll stick with Bounded to keep things a bit simpler.

Implementing alphabeta is a standard exercise. It is even easier when you have a formal specification like the above to guide the implementation.

alphabeta :: Ord score => Game score -> (score, score) -> score
alphabeta (Max (g0 :| [])) i = alphabeta g0 i
alphabeta (Max (g0 :| g1 : gs)) (alpha, beta) =
  let m0 = alphabeta g0 (alpha, beta) in
  if beta <= m0 then m0
  else m0 `max` alphabeta (Max (g1 :| gs)) (max alpha m0, beta)
alphabeta (Min (g0 :| [])) i = alphabeta g0 i
alphabeta (Min (g0 :| g1 : gs)) (alpha, beta) =
  let m0 = alphabeta g0 (alpha, beta) in
  if m0 <= alpha then m0
  else m0 `min` alphabeta (Min (g1 :| gs)) (alpha, min beta m0)
alphabeta (End s) _ = s

But still, it is at least a little finicky and tedious to make sure that you haven’t mixed your alphas and betas.

As we will see in this post, we can streamline the implementation of alpha-beta pruning by factoring the short-circuiting logic out of the “minimax” logic.

Generalized minimax

Remark that minimax only uses min and max (via minimum and maximum), rather than the comparison functions of Ord (compare, (<=), etc.).

We can reduce the dependency footprint of minimax by defining a new class with only the necessary operations, the class of lattices:

class Lattice a where
  -- Join, least upper bound, max
  (\/) :: a -> a -> a 
  -- Meet, greatest lower bound, min
  (/\) :: a -> a -> a

In mathematics, lattices are algebraic structures with two operations (\/) (“join”) and (/\) (“meet”) satisfying commutativity, associativity, as well as the absorption laws:

x \/ (x /\ y) = x
x /\ (x \/ y) = x

In this post, we will only be looking at lattices that arise out of total orders, so this class is rather just a way of saying that we only depend on min and max.

Binary operations can be iterated to combine lists of arguments, similarly to the maximum and minimum functions:

-- maximum
joins :: Lattice a => NonEmpty a -> a
joins = foldr1 (\/)

-- minimum
meets :: Lattice a => NonEmpty a -> a
meets = foldr1 (/\)

Minimax in lattices is defined by replacing Max and Min nodes with the joins and meets operations.

-- Minimax in lattices
minimaxL :: Lattice score => Game score -> score
minimaxL (Max gs) = joins (minimaxL <$> gs)
minimaxL (Min gs) = meets (minimaxL <$> gs)
minimaxL (End x) = x

minimaxL generalizes minimax since every decidable total order is a lattice (because you can use (<=) to define min/max). Ideally this fact would be made explicit by making Lattice into a superclass of Ord. Unfortunately in Haskell this would require us to modify Ord or redefine it. Another way to express the relation between Lattice and Ord is through a newtype.

newtype OrdLattice a = OrdLattice a
   deriving newtype (Eq, Ord, Bounded)

unOrdLattice :: OrdLattice a -> a
unOrdLattice (OrdLattice x) = x

instance Ord a => Lattice (OrdLattice a) where
  OrdLattice x \/ OrdLattice y = OrdLattice (max x y)
  OrdLattice x /\ OrdLattice y = OrdLattice (min x y)

With that, we recover the starting minimax by specializing minimaxL to OrdLattice s, and then unwrapping OrdLattice:

minimaxO :: Ord score => Game score -> score
minimaxO = unOrdLattice . minimaxL . fmap OrdLattice

Clamping functions

Focus on the type (score, score) -> score which appears in the signature of alphabeta. More specifically, we are interested in a subset of those functions that we shall call clamping functions.

Intuitively, a clamping function f is a delayed representation of a constant s: the goal of f is to compute s, but it may also stop early with an approximation if it’s not necessary to know the exact value of s.

The name “clamping function” is a reference to the clamp function:

clamp :: Ord score => score -> (score, score) -> score
clamp s (alpha, beta) = max alpha (min s beta)

We can think of the partially applied function clamp s as an encoding of the constant s, which may or may not be output depending on the interval (alpha, beta).

More formally, a clamping function with value s is a function f :: (score, score) -> score that satisfies the following, for all (alpha, beta) such that alpha < beta:

• if alpha < s < beta, then f (alpha, beta) = s;
• if s <= alpha, then f (alpha, beta) <= alpha;
• if beta <= s, then beta <= f (alpha, beta).

Two clamping functions with the same value s are considered equal. In particular, as clamping functions, const s is equal to clamp s. Making the notion of equality explicit is necessary to make sense of equations (laws for lattices, homomorphisms, and isomorphisms).

We enshrine the definition of clamping functions in a newtype:

-- Type of clamping functions, satisfying the properties above.
newtype Clamping score = Clamping ((score, score) -> score)

unClamping :: Clamping score -> (score, score) -> score
unClamping (Clamping f) = f

For any value s, we can construct the constant clamping function:

clamping :: score -> Clamping score
clamping s = Clamping (\_ -> s)

Note that \_ -> s and clamp s are both clamping functions with value s, so both are valid definitions of clamping s. We prefer the constant function \_ -> s because it does less work.

Conversely, we can project clamping functions back into their values by passing the whole interval (minBound, maxBound):

declamp :: Bounded score => Clamping score -> score
declamp (Clamping f) = f (minBound, maxBound)

Those two functions form an isomorphism between score and Clamping score, meaning that they satisfy the following equations:

declamp . clamping = id
clamping . declamp = id

We now get to the secret sauce of this post: the maximum of two clamping functions (as well as the minimum). This operation can be defined in two ways. First is the naive definition, for reference:

-- "max" for clamping functions, naive variant
maxC :: Ord s => Clamping s -> Clamping s -> Clamping s
maxC (Clamping f) (Clamping g) = Clamping (\i -> max (f i) (g i))

Second is the lazy definition: if f (alpha, beta) is greater than the given upper bound beta, then the max of f and g will be even greater:

beta <= f (alpha, beta) <= max (f (alpha, beta)) (g (alpha, beta)) 

In that case, the maximum of f and g is allowed to output f (alpha, beta) without looking at g. Otherwise we must evaluate g, but we can tighten the interval by updating the lower bound to max alpha (f (alpha, beta)).

-- "max" for clamping functions, lazy variant
lazyMaxC :: Ord s => Clamping s -> Clamping s -> Clamping s
lazyMaxC (Clamping f) (Clamping g) = Clamping (\(alpha, beta) ->
  let fi = f (alpha, beta) in
  if beta <= fi then fi else fi `max` g (max alpha fi, beta))

Dually, we also have a lazyMinC.

lazyMinC :: Ord s => Clamping s -> Clamping s -> Clamping s
lazyMinC (Clamping f) (Clamping g) = Clamping (\(alpha, beta) ->
  let fi = f (alpha, beta) in
  if fi <= alpha then fi else fi `min` g (alpha, min beta fi))

To avoid repeating ourselves, we can also reuse lazyMaxC to implement lazyMinC. Use Down to invert the ordering of an Ord:

lazyMinC :: Ord s => Clamping s -> Clamping s -> Clamping s
lazyMinC f g = undualize (lazyMaxC (dualize f) (dualize g))
  where
    dualizeWith from to (Clamping h) =
      Clamping (\(beta, alpha) -> from (h (to alpha, to beta)))
    dualize   = dualizeWith Down getDown -- Clamping s -> Clamping (Down s)
    undualize = dualizeWith getDown Down -- Clamping (Down s) -> Clamping s

These “naive” and “lazy” functions denote the same value (maxC = lazyMaxC and minC = lazyMinC), but lazyMaxC and lazyMinC may do less work, either by ignoring their second argument or by applying it to a smaller interval than expected.

The point is that these “lazy” functions embody the short-circuiting logic of alpha-beta pruning exactly. All that’s left to do is to plug them into minimax.

The lattice of clamping functions

With the lazy min and max that we just defined, we get a lattice:

instance Ord score => Lattice (Clamping score) where
  (\/) = lazyMaxC
  (/\) = lazyMinC

Specialize minimax in the lattice of clamping functions:

minimaxC :: Ord score => Game (Clamping score) -> Clamping score
minimaxC = minimaxL

This doesn’t look like much, but we have actually implemented the alpha-beta pruning algorithm. With a tiny bit of plumbing, we can redefine the function alphabeta from earlier:

alphabeta' :: Ord score => Game score -> (score, score) -> score
alphabeta' = unClamping . minimaxC . fmap clamping

Then we want to partially apply alphabeta' to the interval (minBound, maxBound). This amounts to replacing unClamping with declamp in the body of alphabeta'. Behold our final implementation of minimax by alpha-beta pruning:

minimaxAB' :: (Ord score, Bounded score) => Game score -> score
minimaxAB' = declamp . minimaxC . fmap clamping

To sum up, we implemented alpha-beta pruning as a simple combination of:

• minimax, generalized from orders to lattices (minimaxL);
• the lattice of clamping functions (Lattice (Clamping score)).

This alternative approach does not completely absolve you from effort: you still have to juggle alphas and betas correctly to implement the lattice (lazyMinC and lazyMaxC). But unlike in the original alphabeta, you don’t have to do all that juggling in the middle of a recursive function. The logic of alpha-beta pruning is neatly decomposed into bite-sized pieces.

Correctness for free

Since we just reused the code of minimax, it’s also easier to prove that that alpha-beta pruning yields the same result:

minimax = minimaxAB'

As we are about to see, this is a direct consequence of the free theorem² for minimaxL: any function of type forall s. Lattice s => Game s -> s, such as minimaxL, commutes with any lattice homomorphism³ f, in the following sense:

f . minimaxL = minimaxL . fmap f

We can picture that equation as a commutative diagram:

\[\require{AMScd} \begin{CD} \small\texttt{Game s} @>{\texttt{minimaxL}}>> \small\texttt{s} \\ @V{\texttt{fmap f}}VV @VV{\texttt{f}}V \\ \small\texttt{Game t} @>{\texttt{minimaxL}}>> \small\texttt{t} \end{CD}\]

If f has an inverse f⁻¹, we can rewrite that to

minimaxL = f⁻¹ . minimaxL . fmap f

By replacing (f, f⁻¹) with the isomorphism (clamping, declamp) defined earlier, we obtain exactly the equality between minimax and alpha-beta pruning:

minimaxL = declamp . minimaxL . fmap clamping
         = minimaxAB'

As a commutative diagram:

\[\require{AMScd} \begin{CD} \small\texttt{Game s} @>{\texttt{minimaxAB’}\text{ (alpha-beta)}}>> \small\texttt{s} \\ @V{\texttt{fmap clamping}}VV @AA{\texttt{declamp}}A \\ \scriptsize\texttt{Game (Clamping s)} @>{\texttt{minimaxL}}>> \scriptsize\texttt{Clamping s} \end{CD}\]

QED.

(To be pedantic, the above proof conflates minimaxL with minimax/minimaxO, which relies on pretending that Lattice is a superclass of Ord. Below is another proof that doesn’t take that shortcut, by going through the OrdLattice newtype explicitly, so this proof applies more directly to the Haskell definitions as written here.)

A somewhat more rigorous proof

We want to prove that the alpha-beta-pruning minimaxAB' is equivalent to the naive minimax:

minimax = minimaxAB'

Recall the free theorem of minimaxL. For any lattice isomorphism (f, f⁻¹):

minimaxL = f⁻¹ . minimaxL . fmap f

Replace (f, f⁻¹) with the lattice isomorphism (clamping . unOrdLattice, OrdLattice . declamp) between the lattices OrdLattice score and Clamping score.

minimaxL = OrdLattice . declamp . minimaxL . fmap (clamping . unOrdLattice)

Now we can prove the equality between minimax and minimaxAB', using the above equation as the middle step, followed by canceling inverses:

minimax
= minimaxO
= unOrdLattice . minimaxL . fmap OrdLattice
= unOrdLattice . OrdLattice . declamp . minimaxL . fmap (clamping . unOrdLattice) . fmap OrdLattice
= declamp . minimaxL . fmap clamping
= minimaxAB'

The above is only a proof of functional correctness: minimax and minimaxAB' compute the same result.

To verify that minimaxAB' does so more efficiently is another problem for another day. For now, we can test it.

Strictness check

We test that our “fancy” implementation of alpha-beta (minimaxAB') has the same strictness as the “classical” implementation (minimaxAB), which we presume to be much lazier than minimax.

We use StrictCheck for property-testing of strictness behaviors in Haskell. The following test checks that minimaxAB and minimaxAB' have the same demand on random inputs. We use the function observe1 from StrictCheck to observe the demand of a function f: observe1 applies f it to an instrumented copy of the provided input g, it forces the output (f g of type Int) using the provided forcing function (`seq` ()), and finally returns the demand on the input tree g that was observed by forcing the instrumented copy of g.

main :: IO ()
main = do
  quickCheck $ \(g :: Game Int) ->
    label (bucket (length g)) $
    let demand f = snd (observe1 (`seq` ()) f g) in
    demand minimaxAB === demand minimaxAB'

From the source repository of this blog, the following command compiles and runs this blog post:

cabal run alpha-beta

Instances and auxiliary definitions

-- Histogram of generated value sizes
bucket :: Int -> String
bucket n | n == 1 = "= 1"
         | n < 10 = "< 10"
         | n < 100 = "< 100"
         | n < 1000 = "< 1000"
         | otherwise = ">= 1000"

-- Instances
deriving stock instance GHC.Generic (Game a) 
instance Generic (Game a)
instance HasDatatypeInfo (Game a)
instance Shaped a => Shaped (Game a)

instance Arbitrary a => Arbitrary (Game a) where
  arbitrary = sized $ \n -> if n == 0 then End <$> arbitrary else
    resize (n `div` 2) $ frequency
      [(1, End <$> arbitrary), (2, Max <$> arbitrary), (2, Min <$> arbitrary)]
  shrink (Max (g :| gs)) = g : gs ++ (Max <$> shrink (g :| gs))
  shrink (Min (g :| gs)) = g : gs ++ (Min <$> shrink (g :| gs))
  shrink (End s) = End <$> shrink s

instance Arbitrary a => Arbitrary (NonEmpty a) where
  arbitrary = liftA2 (:|) arbitrary arbitrary
  shrink (x :| xs) = [y :| ys | y : ys <- shrink (x : xs)]

Conclusion

I came up with this idea a while back on Stack Overflow, as an answer to Alpha-beta pruning with recursion schemes. My understanding of alpha-beta pruning changed overnight from a somewhat tricky algorithm to a completely trivial solution. Getting to reuse minimax is not only a satisfying achievement in refactoring, it enables a neat proof of correctness by parametricity (via free theorems).

The role of laziness should also be underscored. If you try to do the same thing in a call-by-value language, the implementation of “generalized minimax” must explicitly delay computations, obscuring the point:

Alpha-beta pruning is just minimax in a lattice of clamping functions.

---

1. For a clearer presentation, see the talk Alpha-Beta Pruning Explored, Extended and Verified (2024) by Tobias Nipkow.↩︎

2. Theorems for free! by Philip Wadler. Free theorems involving type constructor classes by Janis Voigtländer.↩︎

3. A lattice homomorphism f is a function that commutes with the lattice operations:

   f (x /\ y) = f x /\ f y
   f (x \/ y) = f x \/ f y

   ↩︎

by Lysxia at September 01, 2025 12:00 AM

The Parallelism Mesh Zoo

When training large scale LLMs, there is a large assortment of parallelization strategies which you can employ to scale your training runs to work on more GPUs. There are already a number of good resources for understanding how to parallelize your models: I particularly recommend How To Scale Your Model and The Ultra-Scale Playbook. The purpose of this blog post is to discuss parallelization strategies in a more schematic way by focusing only on how they affect your device mesh. The device mesh is an abstraction used by both PyTorch and JAX that takes your GPUs (however many of them you've got in your cluster!) and organizes them into a N-D tensor that expresses how the devices communicate with each other. When we parallelize computation, we shard a tensor along one dimension of the mesh, and then do collectives along that dimension when there are nontrivial dependencies between shards. Being able to explain why a device mesh is set up the way it is for a collection of parallelization strategies is a good check for seeing if you understand how the parallelization strategies work in the first place! (Credit: This post was influenced by Visualizing 6D Mesh Parallelism.)

tl;dr

• DP, FSDP: ["dp"]
• HSDP: ["dp_replicate", "dp_shard"]
• DP+TP, DP+TP+SP: ["dp", "tp"]
• DP+UlyssesSP: ["dp", "sp"] (verl)
• DP+CP: ["dp", "cp"]
• DP+CP+TP: ["dp", "cp", "tp"]
• PP+DP+...: ["pp", "dp", ...] (torchtitan), ["dp", "pp", ...] (Megatron)
• PP+DP+CP+TP+EP: ["pp", "dp_replicate", "dp_shard_mod_ep", "dp_shard_in_ep", "cp", "tp"] (torchtitan)

Prologue: Why device mesh? Before we jump into the zoo, why do we have multi-dimensional meshes in the first place? One intuition is that the dimensions of the device mesh are a reflection of the physical constraints of networking between GPUs (there's a reason why all of the scaling books talk extensively about how the networking for GPUs works; you can't reason about what parallelization strategy you should use without knowing about this!) Let's imagine you have 1024 NVIDIA GPUs. You don't want to treat this 1024 GPUs as an undifferentiated blob of GPUs. Physically, these GPUs are grouped into nodes of eight which have much faster NVLink connections compared to cross-node communication which is done on a slower Infiniband connection. Intuitively, you will want to do something different depending on if you're doing intra-node communication or inter-node communication.

The device mesh imposes structure on this collection of GPUs. A mesh is typically specified as a tensor size (e.g., (128, 8)) as well as string axis names ala named tensor (e.g., ["dp", "tp"]), and is simply an N-D tensor over a range of GPU indices (typically [0, 1, 2, 3, ...] for GPUs, and a mostly ascending but occasionally permuted sequence for TPUs). We typically think of 2D and 3D tensors as grids and cubes, but I find it is more helpful (especially in higher dimensions) to think of the device mesh as imposing some self-similar (fractal) structure on the GPUs. In the simplest 2D mesh that accounts for intra versus inter node communication, GPUs are first organized into nodes on the inner-most dimension, and then the nodes are collected together in the outer-most dimension to form the cluster. (The self-similar nature of the nodes is important because it tells us how communication occurs across the cluster: to communicate over the outer-most mesh dimension, all the GPU 0s on each node talk to each other, all the GPU 1s, etc.) This is only the very simplest mesh we can create, however; with more complicated parallelization strategies we may impose extra levels of structure, e.g., we may organize nodes into pods of two and four, or we might further divide the eight GPUs of a single node. In other words, the mesh tells us about which GPUs communicate to which other GPUs. This is important to know, because when I want to parallelize our model, I am making choices about how to shard tensors across my GPUs. The mesh tells me which GPUs have the other shards of my tensor; in other words, they are who I have to communicate with when I am doing a computation that requires information about the full tensor and cannot be done with the local shards only.

In the zoo, when we talk about a parallelism strategy, we will talk to how it typically relates to other parallelization strategies in the model, and the device mesh will tell us if it is orthogonal to other parallelisms (a new dimension), multiplexed with another strategy (a reused dimension) or perhaps a completely different hierarchy of communication (multiple meshes in the same model that don't factor into the other).

Without further ado, here is the zoo!

Data parallelism (DP). Data parallelism predates the concept of device meshes, since you don't actually need any nontrivial mesh structure to do data parallelism: if you are only doing data parallel, you just shard your input on the batch axis for however many devices you have. This sharding propagates through forwards and backwards until you allreduce to compute the final global gradient for a parameter. If you did make a 1D device mesh (this is useful to think about, because most higher dimensional parallelisms will include some form of data parallelism), you'd probably name your mesh ["dp"], ["ddp"] or perhaps ["batch"].

Let's talk briefly about how people tend to name device mesh axes. In the PyTorch world, it's most common to name the axis after the parallelism that it is responsible, so either "dp" or "ddp" (you really shouldn't call it ddp, but the DataParallel taboo in PyTorch is very real!) The batch name is common in JAX, and is very natural there because when you annotate the sharding of your input, you need to say for each dimension tensor what mesh dim it is sharded over. So when you shard the batch dimension over the batch mesh dim, it looks just like you're labeling the batch dimension of your tensor as batch, e.g., P("batch", None). (This situation doesn't happen in PyTorch because shardings of a tensor are specified per device mesh dim, but that's a story for another day!)

Fully-sharded data parallel (FSDP). This is best understood as an augmentation over DP where weights are also sharded over all GPUs and you just all-gather weights before performing operations (and reduce-scatter in backwards). Because this all-gather is also among all devices, you don't need another axes in your mesh, and your mesh might also be called ["dp"] in this case, even though you're actually doing FSDP. Occasionally, you'll see people name their mesh ["fsdp"] in this case.

Hybrid sharded data parallel (HSDP). HSDP is an extension of FSDP where you shard weights (FSDP) up to the point where you can't actually do a giant all-gather/reduce-scatter over every GPU, and then replicate these shards to cover the rest of your cluster (DP). It's also amenable to fault tolerance techniques that make the modeling assumption that it's OK to lose samples of your batch if a replica fails (you won't model this with device mesh though!). This is probably the first time you will encounter a 2D device mesh (indeed, the DeviceMesh tutorial in PyTorch specifically uses hybrid sharding as its motivating example), since HSDP doesn't require any extra model changes on top of FSDP. There are a few common ways to name the mesh axes for HSDP. One way to think about it is that it is FSDP on the inner dimension and DP on the outer dimension, in which case you would say ["dp", "fsdp"]. Another way is to think about what happens to parameters at the various layers of the mesh: the inner dimension shards, while the outer dimension replicates, so you would say ["replicate", "shard"] or perhaps ["dp_replicate", "dp_shard"] to make it clear that you are still doing data parallelism across both of these device mesh dims (in particular, when you split your batches, you split on both the dp_replicate and dp_shard dims--although, to get the final gradients, you can do the reduction hierarchically by first doing a reduce-scatter on "dp_shard" and then doing an allreduce on "dp_replicate").

Tensor parallelism (TP). Depending on who you ask, tensor parallelism is either about letting you reduce your effective batch size for training or moving you towards reducing the memory usage of activations in your model. In the "reduce effective batch size" framing, the idea behind TP is that you can only scale up DP until your cluster is as large as your batch size. From a modeling perspective, it can be undesirable to have a batch size that is too large, so you can't just keep increasing your batch size to get more parallelism. Instead, TP allows us to get some extra scaling by sharding over the feature dimension of our matrix multiplies [1] (you can shard over either the columns or the rows of your weight matrix, so we will frequently specify if a TP Linear is column-wise or row-wise; in attention, column-wise linear effectively parallelizes the attention computation over attention heads). The communication needed to do TP is fairly exposed (unless you're doing async tensor parallel), so you typically want to keep the communications for it within a single node. This leads to this classic 2D device mesh for DP+TP: ["dp", "tp"] (or, if you're a JAXer, you might write ["batch", "model"], where model is used to indicate the inner feature dimension of the model weights being parallelized over.) When someone says 2D parallelism, they're usually referring to this combo of parallelisms (although I do not recommend using this term--as you can see, it is obviously ambiguous!) Note that tp is the inner mesh dimension, since it benefits the most from the high bandwidth network between GPUs on a single node.

You don't have to stop with DP+TP, however. If you're using FSDP with tensor parallelism (remember, "dp" can mean FSDP!), intra-node TP doesn't improve the amount of inter-node FSDP communication you have to do: however much TP you do, within one TP node you only have one slice of the model and have to talk to everyone else to get their slices. You could solve this by expanding TP to also cross nodes, but in practice mixed intra/inter-node collectives are a lot slower than pure inter-node collectives. This limits the scaling you can get from TP, and so if you're still hitting limits on FSDP, it can still be useful to apply HSDP to avoid running collectives that are too large. In that case, you'd end up with a mesh like ["dp_replicate", "dp_shard", "tp"].

Sequence parallelism (SP). For this section, we specifically take the definition of sequence parallelism from the Ultrascale Playbook (as distinguished from context parallelism). Although we said that TP is the first step towards reducing the memory usage of activations [2], if you literally implement DP+TP based on my descriptions above, you will still end up with more memory spent on activations than you want because there are still parts of the model around the FFN like the LayerNorm need the full hidden dimension to compute mean and variance [3]. To reduce the memory usage in these segments, you need to shard on something else. So typically what you will see is that the model will alternate between TP (hidden dimension is sharded) and SP (sequence dimension is sharded). Consequently, if you look at the device mesh for a model using DP+TP+SP, it will typically still look like ["dp", "tp"], and instead the tp dimension is multiplexed to be used both for TP and SP. Because TP and SP never occur at the same time, you don't need a separate dimension for them.

Ulysses sequence parallelism. Ulysses sequence parallelism from DeepSpeed Ulysses is another sequence parallelism strategy that is implemented by verl (because verl is forked so often, it shows up quite prominently if you are looking for examples of init_device_mesh on GitHub code search). It aims to alleviate memory pressure from extremely long sequences, so sequences are sharded on input, and only when attention needs to be computed is an alltoall issued to re-shard on the attention heads rather than the sequence (doing another alltoall to restore the sequence sharding after the attention is done). Importantly, this means it competes with TP for sharding on the attention heads, which is why you also see people use it to replace TP in MoE models, since it has much less communication than TP (at the cost of having to replicate the attention weights). In verl, you will just see a device mesh ["dp", "sp"] when you are using their FSDP backend (which is what supports Ulysses).

Context parallelism (CP). Context parallelism is another form of "sequence" parallelism. Like Ulysses sequence parallelism, sequences are sharded on input; the difference, however, is instead of using an alltoall to re-shard on attention heads, you just do a (distributed) attention on the entire context. You can do this the easy way by just using allgather to get the full context (as was done in llama4) or you can use a fancy kernel like ring attention, which carefully overlaps communication and computation when performing attention. A popular implementation of context parallelism lives in Megatron, which doesn't directly use PyTorch's native DeviceMesh abstraction but has an analogous HyperCommGrid. The mesh we see here will be something like ["dp", "cp"] or more commonly ["dp", "cp", "tp"]. Notice that we can have a dedicated mesh dim for CP: CP operates very similarly to SP outside of the attention calls (as it is just plain data parallelism when there is no cross-token dependency), but because it never shards on attention heads, it doesn't compete with TP and can be used completely orthogonally to TP (TP shards hidden, CP shards sequence).

CP has a pretty interesting interaction with FSDP. Both DP and CP shard the input data (on batch and sequence respectively). It's pretty common when you do FSDP to just shard over both "dp" ("dp_shard" in HSDP) and "cp". In torchtitan, we create a flattened mesh dim "dp_shard_cp" specifically for FSDP sharding (a flattened mesh dim is what happens if you take your mess and "forget" about some of the structure; e.g., if you were to do an all-gather, you just all-gather over all the flattened axes). In the HSDP world, "dp_cp" is still a useful concept because this is the combination of axes you want to all-reduce over to, e.g., compute the global average loss.

Pipeline parallelism (PP). Pipeline parallelism is kind of an ugly duckling and people tend to hate on it because you have to rewrite your models to introduce pipeline stages, and you can't really use things like DTensor with it (unless you do really strange things like how the GSPMD paper "supports" pipeline parallelism--the general consensus is automatic parallelism does not like PP). PP still goes in the device mesh, because it affects how you are organizing your GPUs, but, for example, torchtitan solely uses it to setup PGs for doing the point-to-point communications. I've seen both ["dp", "pp", ...] or ["pp", "dp", ...] for meshes with PP, but the order probably doesn't make too much of a difference as you are likely solidly inter-node at this point. Pipeline parallelism bandwidth use is very low, and latency can be covered up as you can immediately start processing the next batch after triggering an asynchronous send of the previous batch.

Expert parallelism (EP). EP is its own kettle of fish. Expert parallelism only applies over the expert computation of the model, but within this region, we are not sharding parameters as FSDP conventionally sees it: we will commonly have the entire expert's weights on our node. torchtitan's WIP expert parallelism implementation, when it has ALL parallelisms on, would look like ["pp", "dp_replicate", "dp_shard_mod_ep", "dp_shard_in_ep", "cp", "tp"], where dp_shard has been split into two mesh dimensions (DP shard modulo EP, and DP shard in EP). dp_shard_mod_ep is conventionally one, but when it is not it represents further FSDP-style sharding of expert weights inside of the expert region (there's some complication here if you have shared experts along-side your EP-sharded experts). But then dp_shard_in_ep, cp and optionally tp are combined together to give you the expert parallel dimension. It's actually more intuitive to imagine that you have two distinct meshes: ["pp", "dp_replicate", "dp_shard", "cp", "tp"] and ["pp", "dp_shard_mod_ep", "ep", "tp"]. The keen-eyed may also notice that there is no intrinsic reason the tp mesh size inside and outside of the expert parallel region, but this is not easily done if you have to have a single global device mesh for everything. In fact, there is a WIP PR to have two meshes, one for inside the expert region and one for outside: https://github.com/pytorch/torchtitan/pull/1660

Conclusion. The general concept behind mesh parallelism is that you can compose parallelization strategies without too much fuss. Indeed, the use of, e.g., TP to improve scaling is precisely because it lets you cover your device space without having to expand DP beyond the batch size you want to do. However, as you can see from these concrete examples, it's not always quite as simple as just stacking all of the parallelisms together one on top of each other. In the end, all the device mesh is doing is creating PGs behind groups of devices as defined by the mesh, so if you want some weird setup where you're swapping between two device meshes, PyTorch's general philosophy has been to say, have fun!

Thanks to Horace He, Tianyu Liu and Natalia Gimelshein for helping fact check this post. Any remaining errors are mine!

[1]

One more subtlety I want to point out: while we tend to think of TP as sharding the feature dimension of parameters, when we "propagate" this sharding through the network, other intermediate tensors end up getting sharded on the TP dimension as well. In particular, in a transformer block, you will typically have a column-wise linear followed by a row-wise linear, and the intermediate activation will be temporarily sharded on the TP dimension before the row-wise linear runs.

[2]

I am very carefully using "activation memory" here and not total memory, because total memory usage (what you actually care about) is also a function of peak memory usage, which is subject to transient peaks such as when FSDP does an all-gather to collect parameters. In fact, even without SP, TP will improve your peak memory usage, because unlike FSDP, it's not necessary to all-gather the full weight matrix to actually perform the matrix multiply. TPs peak memory usage occurs when it all-gathers activations.

[3]

You will get a little improvement between the column-wise and row-wise linear, since the activations there are sharded. You can turn this into a big improvement by using selective activation checkpointing and forcing recomputation of activations that aren't sharded! (Plain activation checkpointing tends not to work so well because of the all-gather of the activations.)

by Edward Z. Yang at August 31, 2025 03:20 AM

Welcoming a new Haskell Ecosystem Supporter: Standard Chartered

Following on from our announcement of Haskell Ecosystem Support Packages, Well-Typed are delighted to introduce Standard Chartered as our first Gold Haskell Ecosystem Supporter.

At Standard Chartered Bank, Haskell is used in a core software library supporting the entire Markets division – a business line with 3 billion USD operating income in 2023. Typed functional programming is used across the entire tech stack, including foundational APIs and CLIs for deal valuation and risk analysis, server-side components for long-running batches or sub-second RESTful services, and end-user GUIs. Thousands of users across Markets interact with software built using functional programming, and over one hundred write functional code.

Well-Typed’s Haskell Ecosystem Support Packages, offered in partnership with the Haskell Foundation, allow companies using Haskell to

• invest in the maintenance and future development of the core Haskell toolchain,
• access Well-Typed’s team of Haskell experts for private development or technical support, and
• fund the Haskell Foundation to sustain key community infrastructure.

You can read more about the toolchain maintenance activities these packages fund in our regular reports. Many thanks to Standard Chartered, to the existing Haskell Ecosystem Supporters, and to our other clients who fund open-source development work, for making this possible.

If your company relies on Haskell, and depends on its core toolchain and vibrant open-source ecosystem, why not read more about our offer?

by adam at August 29, 2025 12:00 AM

CodeQL: code organization, metadata, and running in CI

In the previous blog post of this series, I talked about CodeQL, a static analyzer from GitHub that performs semantic search queries on source code to extract structured data. I described how I wrote my first CodeQL query and how I executed it locally. In this second blog post, I want to go beyond that.

I will cover aspects that are required for putting custom queries into production. I’ll explain:

• how CodeQL sources are organized,
• what query metadata is,
• how to run CodeQL in GitHub Actions, and
• how to visualize results.

While the first two topics are specific to teams that need to write their own queries, the last two are applicable both to teams that write their own queries and to teams relying on the default queries shipped with CodeQL (which do capture a vast number of issues already).

I won’t dive deep on any topic, but rather give an overview of the features you will most likely need to put your own CodeQL queries into production. I’ll often link to GitHub’s official documentation, so that you have quick access to the documentation most useful to you. Finding what you need can be a bit of a challenge, because CodeQL’s documentation is spread over both https://docs.github.com/en/code-security and https://codeql.github.com/docs/.

Structure of CodeQL sources

There are four main types of CodeQL file:

• *.ql files are query files. A query is an executable request and a query file must contain exactly one query. I will describe the query syntax below. A query file cannot be imported by other files.

• *.qll files are library files. A library file can contain types and predicates, but it cannot contain a query. Library files can be imported.

• *.qls files are YAML files describing query suites. They are used to select queries, based on various filters such as a query’s filename, name, or metadata. Query suites are documented in detail in the official documentation.

• *.qlpack files are YAML files describing packs. Packs are containers for the three previous kind of files. A pack can either be a query pack, containing queries to be run; a library pack, containing code to be reused; or a model pack, which is an experimental kind of pack meant to extend existing CodeQL rules. Packs are described in detail here.

  When developing custom queries, I need to wrap them in a query pack in order to declare on what parts of the CodeQL standard library my queries depend (here’s an example to show how to depend on the Java standard library).

Queries in *.ql files have the following structure (as explained in more detail in the official documentation):

from /* ... variable declarations ... */
where /* ... logical formula ... */
select /* ... expressions ... */

This can be understood like an SQL query:

• First, the from clause declares typed variables that can be referenced in the rest of the query. Because types define predicates, this clause already constrains the possible instances returned by the where clause that follows.
• The where clause constrains the query to only return the variables that satisfy the logical formula it contains. It can be omitted, in which case all instances of variables with the type specified in the from clause are returned.
• The select clause limits the query to operate on the variables declared in the from clause. The select clause can also contain formatting instructions, so that the results of the query are more human readable.

To give an example of a query, if I need to write a query to track tainted data in Java, in a file named App.java, I’ll write this to start somewhere and will refine the where clause iteratively, based on the query’s result:

from DataFlow::Node node // A node in the syntax tree
where node.getLocation().getFile().toString() = "App"  // .java extension is stripped
select node, "node in App"

select clauses must obey the following constraints with respect to the number of columns selected:

• A problem query (see below) must select an even number of columns. The format is supposed to be: select var1, formatting_for_var1, var2, formatting_for_var2, ... where formatting_for_var* must be an expression returning a string, as described earlier in the select paragraph. If you omit the formatting, the query is executed, but a warning is issued.
• A path-problem query must select four columns, the first three referring to syntax nodes and the fourth one a string describing the issue. This assumption is required by the CodeQL Query Results view in VSCode to show the results as paths (using the alerts style in the drop down):

Query metadata

The header of a query defines a set of properties called query metadata:

/**
 * @name Code injection
 * @description Interpreting unsanitized user input as code allows a malicious user to perform arbitrary
 *              code execution.
 * @kind path-problem
 * @problem.severity error
 * ...
 */

Query metadata is documented in detail in CodeQL’s official documentation. I don’t want to repeat GitHub’s documentation here, so I’m focusing on the important information:

• @kind can take two values: problem and path-problem. The former is for queries that flag one specific location, while the latter is for queries that track tainted data flow from a source to a sink.
• Severity of issues is defined through two means, depending on whether the query is considered a security-related one or not 🤷
  • @problem.severity is used for queries that don’t have @tags security. @problem.severity can be one of error, warning, or recommendation.
  • @security-severity is a score between 0.0 and 10.0, for queries with @tags security.

Metadata is most useful for filtering queries in qls files. This is used extensively in queries shipped with CodeQL itself, as visible for example in security-experimental-selectors.yml¹. To give an idea of the filtering capability, here is an excerpt of this file that declares filtering criteria:

- include:
    kind:
      - problem
      - path-problem
    precision:
      - high
      - very-high
    tags contain:
      - security
- exclude:
    query path:
      - Metrics/Summaries/FrameworkCoverage.ql
      - /Diagnostics/Internal/.*/
- exclude:
    tags contain:
      - modeleditor
      - modelgenerator

To smooth the introduction of CodeQL (and security tools in general), I recommend starting small and only reporting the most critical alerts at first (in other words: filtering aggressively). This helps to convince teammates that CodeQL reports useful insights, and it doesn’t make the task of fixing security vulnerabilities look insurmountable.

Once the most critical alerts are fixed, I advise loosening the filtering, so that pressing — but not critical — issues can be addressed.

Running CodeQL in GitHub Actions

The following GitHub Actions are required to run CodeQL:

1. github/codeql-action/init installs CodeQL and creates the database. It can be customized to specify the list of programming languages to analyze, as well as many other options. Customization is done in the YAML workflow file, or via an external YAML configuration file, as explained in the customize advanced setup documentation.
2. github/codeql-action/autobuild is required if you are analyzing a compiled language (such as C# or Java, as opposed to Python). This action can either work out of the box, guessing what to do based on the presence of the build files that are idiomatic in your programming language’s ecosystem. I must admit this is not very principled — you need to look up the corresponding documentation to see how CodeQL is going to behave for your programming language and platform. If the automatic behavior doesn’t work out of the box, you can manually specify the build commands to perform.
3. github/codeql-action/analyze runs the queries. Its results are used to populate the Security tab, as shown below.

Since the actions work out of the box on GitHub, replicating them in another CI/CD system is non-trivial: you will have to build your own solution.

Visualizing results

Once CodeQL executes successfully in CI, GitHub’s UI picks up its results automatically and shows them in the Security tab:

You may wonder why you cannot see the Security tab on the repository used to create this post’s screenshots yourself. This is because, as GitHub’s documentation explains, security alerts are only visible to people with the necessary rights to the repository. The required rights depend on whether the repository is owned by a user or an organisation. In any case, security alerts cannot be made visible to people who do not have at least some rights to the relevant repository. Clicking on View alerts brings up the main CodeQL view:

As visible in the screenshot, this view allows you to filter the alerts in multiple ways, as well as to select the branch from which the alerts are shown.

Conclusion

In this post, I covered multiple aspects that you need to know to put your custom queries in production. I described how CodeQL codebases are organized and the constraints that individual queries must obey. I described queries’ metadata and how metadata is used. I concluded by showing how to run queries in CI and how everyone in a team can visualize the alerts found. Equipped with this knowledge, I think you are ready to experiment with CodeQL and later pitch it to your stakeholders, as part of your security posture 😉

---

1. The file doesn’t have the qls extension, but its content is valid qls content; because it is applyied: the apply clause simply inserts a file within a qls file.↩

August 28, 2025 12:00 AM

Finding Bugs in a Coding Agent with Lightweight DST

Amp is a coding agent which I’ve been working on the last six months at Sourcegraph. And in the last couple of weeks, I’ve been building on a testing rig inspired by Deterministic Simulation Testing (DST) to test the most crucial parts of the system. DST is closely related to fuzzing and property-based testing.

The goal is to get one of Amp’s most central pieces, the ThreadWorker, under heavy scrutiny. We’ve had a few perplexing bug reports, where users experienced corrupted threads, LLM API errors from invalid tool calls, and more vague issues like “it seems like it’s spinning forever.” Reproducing such problems manually is usually somewhere between impractical and impossible. I want to reproduce them deterministically, and in a way where we can debug and fix them. And beyond the known ones, I’d like to find the currently unknown ones before our users hit them.

Generative testing to the rescue!

Approach: Lightweight DST in TypeScript

Amp is written in TypeScript, which is an ecosystem currently not drowning in fuzzing tools. My starting point was using jsfuzz, which I hadn’t used before but it looked promising. However, I had a bunch of problems getting it to run together with our Bun stack. One could use fast-check, but as far as I can tell, the model-based testing they support doesn’t fit with our needs. We don’t have a model of the system, and we need to generate values in multiple places as the test runs. So, I decided to build something from scratch for our purposes.

I borrowed an idea I got from matklad last year: instead of passing a seeded PRNG to generate test input, we generate an entropy Buffer with random contents, and track our position in that array with a cursor. Drawing a random byte consumes the byte at the current position and increments the cursor. We don’t know up-front how many bytes we need for a given fuzzer, so the entropy buffer grows dynamically when needed, appending more random bytes. This, together with a bunch of methods for drawing different types of values, is packaged up in an Entropy class:

class Entropy {  random(count): UInt8Array { ... }  randomRange(minIncl: number, maxExcl: number): number { ... }  // ... lots of other stuff }

A fuzzer is an ES module written in TypeScript, exporting a single function:

export async function fuzz(entropy: Entropy) {  // test logic here }

Any exception thrown by fuzz is considered a test failure. We use the node:assert module for our test assertions, but it could be anything.

Another program, the fuzz runner, imports a built fuzzer module and runs as many tests it can before a given timeout. If it finds a failure, it prints out the command to reproduce that failure:

Fuzzing example.fuzzer.js iteration 1000... Fuzzing example.fuzzer.js iteration 2000... Fuzzer failed: AssertionError [ERR_ASSERTION]: 3 != 4 at [...] Reproduce with: bun --console-depth=10 scripts/fuzz.ts \ dist/example.fuzzer.js \ --verbose \ --reproduce=1493a513f88d0fd9325534c33f774831

Why use this Entropy rather than a seed? More about that at the end of the post!

The ThreadWorker Fuzzer

In the fuzzer for our ThreadWorker, we stub out all IO and other nondeterministic components, and we install fake timers to control when and how asynchronous code is run. In effect, we have determinism and simulation to run tests in, so I guess it qualifies as DST.

The test simulates a sequence of user actions (send message, cancel, resume, and wait). Similarly, it simulates responses from tool calls (like the agent reading a file) and from inference backends (like the Anthropic API). We inject faults and delays in both tool calls and inference requests to test our error handling and possible race conditions.

After all user actions have been executed, we make sure to approve any pending tool calls that require confirmation. Next, we tell the fake timer to run all outstanding timers until the queue is empty; like fast-forwarding until there’s nothing left to do. Finally, we check that the thread is idle, i.e. that there’s no ongoing inference and that all tool calls have terminated. This is a liveness property.

After the liveness property, we check a bunch of safety properties:

• all messages posted by the user are present in the thread
• all message pairs involving tools calls are valid according to Anthropic’s API specification
• all tool calls have settled in expected terminal states

Some of these are targeted at specific known bugs, while some are more general but have found bugs we did not expect.

Here’s a highly simplified version of the fuzzer:

export async function fuzz(entropy: Entropy) {  const clock = sinon.useFakeTimers({  loopLimit: 1_000_000,  })  const worker = setup() // including stubbing IO, etc   try {  const resumed = worker.resume()  await clock.runAllAsync()  await resumed   const actions: UserAction[] = []  async function run() {  for (let round = 0; round < entropy.randomRange(1, 50); round++) {  const action = await generateNextAction(entropy, worker)  switch (action.type) {  case 'user-message':  await worker.handle({  ...action,  type: 'user:message',  })  break  case 'cancel':  await worker.cancel()  break  case 'resume':  await worker.resume()  break  case 'sleep':  await sleep(action.milliseconds)  break  case 'approve': {  await approveTool(action.threadID, action.toolUseID)  break  }  }  }   // Approve any remaining tool uses to ensure termination into an   // idle thread state  const blockedTools = await blockedToolUses()  await Promise.all(blockedTools.map(approve))  }   const done = run()  await clock.runAllAsync()  await done   // check liveness and safety properties  // ...  } finally {  sinon.restore()  } }

Now, let’s dig into the findings!

Results

Given I’ve been working on this for about a week in total, I’m very happy with the outcome. Here are some issues the fuzzer found:

Corrupted thread due to eagerly starting tool calls during streaming

While streaming tool use blocks from the Anthropic API, we invoked tools eagerly, while not all of them were finished streaming. This, in combination with how state was managed, led to tool results being incorrectly split across messages. Anthropic’s API would reject any further requests, and the thread would essentially be corrupted. This was reported by a user and was the first issue we found and fixed using the fuzzer.

Another variation, which the fuzzer also found, this was a race condition where user messages interfered at a particular timing with ongoing tool calls, splitting them up incorrectly.

Subagent tool calls not terminating when subthread tool calls were rejected

Due to a recent change in behavior, where we don’t run inference automatically after tool call rejection, subagents could end up never signalling their termination, which led to the main thread never reaching an idle state.

I confirmed this in both VSCode and the CLI: infinite spinners, indeed.

Tool calls blocked on user not getting cancelled after user message

Due to how some tool calls require confirmation, like reading files outside the workspace or running some shell commands, in combination how we represent and track termination of tools, there’s a possibility for such tools to be resumed and then, after an immediate user cancellation, not be properly cancelled. This leads to incorrect mutations of the thread data.

I’ve not yet found the cause of this issue, but it’s perfectly reproducible, so that’s a start.

Furthermore, we were able to verify an older bug fix, where Anthropic’s API would send an invalid message with an empty tool use block array. That used to get the agent into an infinite loop. With the fuzzer, we verified and improved the old fix which had missed another case.

How about number of test runs and timeouts? Most of these bugs were found almost immediately, i.e. within a second. The last one in the list above takes longer, around a minute normally. We run a short version of each fuzzer in every CI build, and longer runs on a nightly basis. This is up for a lot of tuning and experimentation.

Why the Entropy Buffer?

So why the entropy buffer instead of a seeded PRNG? The idea is to use that buffer to mutate the test input, instead of just bombarding with random data every time. If we can track which parts of the entropy was used where, we can make those slices “smaller” or “bigger.” We can use something like gradient descent or simulated annealing to optimize inputs, maximizing some objective function set by the fuzzer. Finally, we might be able to minimize inputs by manipulating the entropy.

In case the JavaScript community gets some powerful fuzzing framework like AFL+, that could also just be plugged in. Who knows, but I find this an interesting approach that’s worth exploring. I believe the entropy buffer approach is also similar to how Hypothesis works under the hood. Someone please correct me if that’s not the case.

Anyhow, that’s today’s report from the generative testing mines. Cheers!

August 27, 2025 10:00 PM

Streamlining CodeQL Analysis: Modus Create's CodeQL Wrapper Solution

In software development today, security can no longer be treated as an afterthought. The earlier vulnerabilities are identified, the cheaper and safer they are to fix. This is why Static Application Security Testing (SAST) has become a cornerstone of modern DevSecOps practices. Among the available tools, GitHub’s CodeQL has emerged as a standout. It doesn’t just look for known patterns—it analyzes code as if it were a database, uncovering subtle and complex vulnerabilities that other tools often miss without increasing the false positive findings. But for all its power, integrating CodeQL into large organizations, especially those with monorepos and heterogeneous CI/CD platforms, can be a real challenge.

To solve this, we built two complementary solutions: the codeql-wrapper and the codeql-wrapper-pipelines. Together, they make CodeQL adoption significantly easier for development teams and security organizations alike.

Highlights of codeql-wrapper:

While GitHub’s CodeQL works well for single-project repositories, monorepos present unique challenges that break the standard workflow.

In a monorepo, teams need to:

• Analyze multiple projects, each with different languages, build systems, and configurations
• Run scans only on changed code during PR reviews for efficiency
• Maintain consistent security policies across diverse projects

The problems with standard CodeQL Actions in monorepos:

• No dynamic project discovery – You can’t generate a job matrix from runtime data, forcing you to hard-code every project
• Inflexible configuration – Each project may need different CodeQL queries, build commands, or language-specific settings
• CI/CD fragmentation – Every platform (Azure DevOps, CircleCI, etc) requires custom implementation
• Inefficient PR scanning – Analyzing the entire monorepo for every PR wastes time and resources

If you’ve read our previous CodeQL blog post, here’s what you’d naturally want to write:

# This doesn't work - matrix can't be built from runtime discovery
jobs:
  analyze:
    strategy:
      matrix:
        project: ${{ steps.discover.outputs.projects }} # Not supported, we would need a `step` before to populate this variable

  steps:
    - name: Initialize CodeQL
      uses: github/codeql-action/init@v3
      with:
        languages: ${{ project.programming_language }}

    - name: Perform CodeQL Analysis
      uses: github/codeql-action/analyze@v3
      with:
        category: "/language:${{ project.programming_language }}"

With the wrapper, you’re done with this one-liner:

- run: codeql-wrapper analyze . --monorepo --only-changed-files --upload-sarif

In the rest of this post, we detail the problems that codeql-wrapper solves and how it does so.

Understanding CodeQL: Why It Matters

At its core, CodeQL is a semantic code analysis engine. It transforms source code into a relational database, allowing queries to detect vulnerable patterns, logic flaws, and unsafe data flows. This capability is powerful because it lets organizations:

• Automate security checks – CodeQL integrates directly into CI/CD pipelines, scanning every pull request or commit.
• Catch complex vulnerabilities – By modeling data and control flows, CodeQL goes far beyond simple regex-based scanners. To the academical reader, such capability is called inter-procedural analysis. Its upside is that it can detect vulnerabilities spanning multiple functions and code source files. Its downside is that it can be slow, and so one needs to be careful how CodeQL models and queries are written, so that performance stays acceptable.
• Run variant analysis – Once you identify a bug, you can find every similar instance across a codebase in minutes. This is particularly important to scale your findings to large organizations.
• Customize queries – Security teams can author their own CodeQL queries tailored to the organization’s specific risk profile. We explained how to write custom queries in our first post in this CodeQL series.
• Cover multiple languages – CodeQL supports a wide set of languages, fitting polyglot environments.
• Integrate with GitHub Advanced Security – Findings are uploaded as SARIF reports and appear directly in GitHub’s security dashboards and pull requests.

For companies under compliance requirements (PCI DSS, FedRAMP, HIPAA) or simply those scaling rapidly, CodeQL is a way to shift security left—catching problems earlier, reducing remediation costs, and strengthening overall security posture.

The CodeQL Wrapper: Make CodeQL Easy on Every Codebase

Despite these benefits, running CodeQL at scale isn’t always straightforward. Complex repositories, custom build processes, and multiple CI/CD environments introduce friction.

This is where the CodeQL Wrapper we developed comes in. It’s a universal Python CLI that abstracts away much of the setup pain and provides a consistent way to run CodeQL across projects. Codeql Wrapper streamlines the usage of CodeQL in many different ways:

• CI/CD agnostic: Works with GitHub Actions, Jenkins, Azure Pipelines, CircleCI, Harness, and more.
• SARIF uploads: Built-in support for sending results directly to GitHub Advanced Security.
• Auto-installation: Fetches and installs the correct version of the CodeQL CLI automatically.
• Flexible .codeql.json config: Lets teams define build modes, queries, and paths centrally.

In particular, Codeql Wrapper is designed to gracefully handle monorepos, addressing both their polyglot nature (monorepos tend to feature multiple programming langauges) and the need for performance (because monorepos tend to be big, analysis on the entire repository doesn’t scale):

• Smart language detection: The idiomatic GitHub Action requires to specify the programming language to analyse. This doesn’t work in monorepos, that are typically polygot (i.e. they mix multiple programming languages). CodeQL Wrapper lifts this burden: you don’t need to configure target languages manually.
• Performance tuned: Supports parallel processing to keep scans efficient in large repositories.

Typically, language detection gets cumbersome in monorepos:

• Constant updates: Every new project requires workflow modifications
• Language mixing: Projects often contain multiple languages (e.g., Java backend with JavaScript tests)
• Human error: Forgetting to add new languages leads to incomplete security coverage
• Maintenance overhead: Teams spend time updating CI/CD configurations instead of writing code

Project-Level Parallelization The primary parallelization strategy operates at the project level in monorepos. Multiple projects are analyzed simultaneously using Python’s ProcessPoolExecutor.

Language-Level Parallelization Within each project, multiple languages are analyzed concurrently. If a project contains Python, JavaScript, and Java code, all three languages are processed in parallel rather than sequentially.

Adaptive Worker Allocation The wrapper automatically determines optimal concurrency based on Available CPU cores and System memory. You can also run a Manual override: --max-workers parameter for fine-tuning

Performance Benefits This multi-level approach delivers significant speedups:

• Monorepo analysis: 5+ projects analyzed simultaneously instead of sequentially
• Mixed-language projects: Python + JavaScript + Java processed in parallel
• Resource efficiency: Maximizes CPU utilization while respecting memory constraints
• Scalable: Performance scales with available hardware resources

For large monorepos with dozens of projects, this can reduce analysis time from hours to minutes.

Getting Started

Install from PyPI:

pip install codeql-wrapper

This will install the tool in your environment. Once installed, you’ll have access to two commands:

• install – Installs CodeQL CLI and query packs (you can pin a specific version if needed).
• analyze – Runs CodeQL analysis on your project(s), with automatic project detection and parallelized scans. If you only need the CodeQL CLI (and don’t want to run a scan yet), just run:

codeql-wrapper install

This will pull the latest version of the CLI and query packs. If you need a different version you can use the --version argument. The real magic happens with the analyze command. It:

• Checks if CodeQL is installed (and installs it if it’s missing).
• Detects your project structure and languages.
• Creates CodeQL databases.
• Runs analysis in parallel, making the most of your CPU. Here are some ways to run it: Run a basic analysis:

# Check if CodeQL is installed, if not it will install it
# Create Code CLI database for each language detected
# Analyze the databases using the default queries and build-mode: none
# You can use `--upload-sarif` to upload the result to Github
codeql-wrapper analyze ./repo

For monorepos:

# Like above, and Detect Projects (each folder inside the monorepo folder will be treated as a project)
codeql-wrapper analyze ./monorepo --monorepo

You can also customize the behavior using a .codeql.json file as follows:

{
  "projects": [
    {
      "path": "./backend",
      "build-mode": "manual",
      "build-script": "./build/project-java-1.sh",
      "queries": ["java-security-extended"],
      "language": "java"
    }
  ]
}


```bash
codeql database analyze db-javascript --format=sarif-latest --output results.sarif

As seen in the .codeql.json snippet above, you can also specify the query to execute in the field queries of a project.

Benefits of This Approach

This approach gives you the flexibility to:

• Use different queries per project in a monorepo
• Maintain consistent query policies across different CI/CD platforms
• Override queries without modifying pipeline files

Changed Files Detection Algorithm

The CodeQL wrapper implements a sophisticated Git-based differential analysis algorithm to detect which files have changed, enabling efficient analysis of only modified code in pull requests and monorepo scenarios.

Algorithm Overview

The changed files detection works through these key steps:

1. Git Reference Resolution: Determines the base commit for comparison using CI/CD environment variables or manual specification
2. Repository Fetching: Ensures the latest commit data is available using git fetch
3. Diff Calculation: Compute differences between base and current commits
4. Project Filtering: Maps changed files to specific projects in monorepo configurations

This unified approach eliminates the need for platform-specific implementations while maintaining robust change detection across all major CI/CD systems.

Files Detection Benefits

This algorithm provides significant performance improvements:

• Selective Analysis: Only projects containing changed files are analyzed
• Reduced Resource Usage: Avoids unnecessary CodeQL database creation for unchanged code
• Faster Feedback: Pull request scans complete in minutes rather than hours for large monorepos
• Cost Optimization: Reduces CI/CD compute time and associated costs

CodeQL Wrapper Pipelines: Real-World Integration Examples

Of course, simplifying local execution is only half the battle. Enterprises need repeatable, automated CI/CD integrations. That’s why Modus Create also released the codeql-wrapper-pipelines repository. This companion project provides ready-to-use templates for popular CI/CD systems, demonstrating exactly how to embed the wrapper in automated workflows.

Why this matters: CodeQL’s standard implementation is tightly coupled to GitHub Actions. The official github/codeql-action assumes you’re running on GitHub-hosted runners with specific environment variables and GitHub APIs available. Adapting CodeQL to other CI/CD platforms typically requires:

• Manually installing the CodeQL CLI and managing versions
• Reimplementing authentication and SARIF upload logic
• Handling language detection and build automation from scratch
• Writing platform-specific scripts for each CI/CD system

By decoupling CodeQL from GitHub Actions, our wrapper enables true CI/CD portability. Supported platforms include:

• GitHub Actions – first-class support with PR integration
• Azure Pipelines – tested YAML templates for enterprise environments
• CircleCI – workflows with CodeQL scanning built in
• Harness – templates for modern CI/CD pipelines

Each platform template handles unique authentication, artifact management, and reporting requirements while maintaining a consistent interface. This means security teams can enforce the same CodeQL policies whether code is built in GitHub, Azure DevOps, or any other platform.

By providing these blueprints, Modus helps teams move from “we should scan with CodeQL” to “we are scanning every PR with CodeQL” in a matter of hours—not weeks.

Conclusion

It’s our experience working with global enterprises adopting GitHub - and GitHub Advanced Security - that made us create codeql-wrapper and codeql-wrapper-pipelines. These tools are the result of our field experience working with monorepos:

• They encapsulate lessons learned from real-world enterprise rollouts.
• They reduce friction for developers and security engineers alike.
• They standardize how CodeQL is runs across organizations, improving consistency and reliability.

These tools are accelerators for companies that want to strengthen their DevSecOps posture without burdening engineering teams. Try them and reach out back to us on the GitHub repositories if you need support!

August 26, 2025 12:00 AM

Sets & Heaps in Haskell and Rust

In the last few articles, we’ve spent some time doing manual algorithms with binary trees. But most often, you won’t have to work with binary trees yourself, as they are built in to the operations of other data structures.

Today, we’ll solve a problem that relies on using the “set” data structure as well as the “heap” data structure. To learn more details about using these structures in Haskell, sign up for our Solve.hs course, where you’ll spend an entire module on data structures!

The Problem

Today’s problem is Find k pairs with smallest sums. Our problem input consists of two sorted arrays of integers as well as a number k. Our job is to return the k pairs of numbers that have the smallest sum, where a “pair” consists of one number from the first array, and one number from the second array.

Here’s an example input and output:

inputNums1 = [1,10,101,102]
inputNums2 = [7,8,9,10,11]
k = 11

output =
  [ (1,7), (1,8), (1,9), (1,10), (1,11)
  , (10,7), (10,8), (10,9), (10,10)
  , (10,11), (101,7)
  ]

Observe that we are returning the numbers themselves in pairs, rather than the sums, and not the indices of the numbers.

While the (implicit) indices of each pair must be unique, the numbers do not need to be unique. For each, if we have the lists [1,1], [5, 7], and k is 2, we should return [(1,5), (1,5)], where both of the 1’s from the first list are paired with the 5 from the second list.

The Algorithm

At the center of our algorithm is a min-heap. We want to store elements that contain pairs of numbers. But we want those elements to be ordered by their sum. We also want the element to contain the corresponding indices for the each number in their array.

We’ll start by making a pair of the first element from each array, and inserting that into our heap, because this pair must be the smallest. Then we’ll do a loop where we extract the minimum from the heap, and then try adding its “neighbors” into the heap. A “neighbor” of the index pair (i1, i2) comes from incrementing one of the two indices, so either (i1 + 1, i2) or (i1, i2 + 1). We continue until we have extracted k elements (or our heap is empty).

Each time we insert a pair of numbers into the heap, we’ll insert the pair of indices into a set. This will allow us to avoid double counting any pairs.

So using the first example in the section above, here are the first few steps of our process. Inside the heap is a 3-tuple with the sum, the indices (a 2-tuple), and the values (another 2-tuple).

Step 1:
Heap: [(8, (0,0) (1, 7))]
Visited: [(0,0)]
Output: []

Step 2:
Heap: [(9, (0,1), (1,8)), ]
Visited: [(0,0), (0,1), (1,0)]
Output: [(1,7)]

Step 3:
Heap: [(10, (0,2), (1,9)), (17, (1,0), (10,7)), (18, (1,1), (10,8))]
Visited: [(0,0), (0,1), (0,2), (1,0), (1,1)]
Output: [(1,7), (1,8)]

And so we would continue this process until we gathered k outputs.

Haskell Solution

The core structure of this problem isn’t hard. We define some initial terms, such as our data structures and outputs, and then we have a single loop. We’ll express this single loop as a recursive function. It will take the number of remaining values, the visited set, the heap, and the accumulated output, and ultimately return the output. Throughout this problem we’ll use the type alias I2 to refer to a tuple of two integers.

import qualified Data.Heap as H
import qualified Data.Set as S

type I2 = (Int, Int)

findKPairs :: V.Vector Int -> V.Vector Int -> Int -> [I2]
findKPairs arr1 arr2 k = ...
  where
    n1 = V.length arr1
    n2 = V.length arr2

    f :: Int -> S.Set I2 -> H.MinHeap (Int, I2, I2) -> [I2] -> [I2]
    f remaining visited heap acc = ...

Let’s fill in our loop. We can start with the edge cases. If the k is 0, or if our heap is empty, we should return the results list (in reverse).

findKPairs :: V.Vector Int -> V.Vector Int -> Int -> [I2]
findKPairs arr1 arr2 k = ...
  where
    f :: Int -> S.Set I2 -> H.MinHeap (Int, I2, I2) -> [I2] -> [I2]
    f 0 _ _ acc = reverse acc
    f remaining visited heap acc = case H.view heap of
      Nothing -> reverse acc
      Just ((_, (i1, i2), (v1, v2)), restHeap) -> ...

Our primary case now results from extracting the min element of the heap. We don’t actually need its sum. We just put that in the first position of the tuple so that it is the primary sorting value for the heap. Let’s define the next possible coordinate pairs from adding to i1 and i2, as well as the new sums we get from using those indices:

findKPairs :: V.Vector Int -> V.Vector Int -> Int -> [I2]
findKPairs arr1 arr2 k = ...
  where
    f :: Int -> S.Set I2 -> H.MinHeap (Int, I2, I2) -> [I2] -> [I2]
    f 0 _ _ acc = reverse acc
    f remaining visited heap acc = case H.view heap of
      Nothing -> reverse acc
      Just ((_, (i1, i2), (v1, v2)), restHeap) ->
        let c1 = (i1 + 1, i2)
            c2 = (i1, i2 + 1)
            inc1 = arr1 V.! (i1 + 1) + v2
            inc2 = v1 + arr2 V.! (i2 + 1)
        in  ...

Now we need to try adding these values to the remaining heap. If the index is too large, or if we’ve already visited the coordinate, we don’t add the new value, returning the old heap. Otherwise we insert it into our heap. For the second value, we just use heap1 (from trying to add the first value) as the baseline.

findKPairs :: V.Vector Int -> V.Vector Int -> Int -> [I2]
findKPairs arr1 arr2 k = ...
  where
    f :: Int -> S.Set I2 -> H.MinHeap (Int, I2, I2) -> [I2] -> [I2]
    f 0 _ _ acc = reverse acc
    f remaining visited heap acc = case H.view heap of
      Nothing -> reverse acc
      Just ((_, (i1, i2), (v1, v2)), restHeap) ->
        let c1 = (i1 + 1, i2)
            c2 = (i1, i2 + 1)
            inc1 = arr1 V.! (i1 + 1) + v2
            inc2 = v1 + arr2 V.! (i2 + 1)
            heap1 = if i1 + 1 < n1 && S.notMember c1 visited
                      then H.insert (inc1, c1, (arr1 V.! (i1 + 1), v2)) restHeap else restHeap
            heap2 = if i2 + 1 < n2 && S.notMember c2 visited
                      then H.insert (inc2, c2, (v1, arr2 V.! (i2 + 1))) heap1 else heap1
        in  ...

Now we complete our recursive loop function, by adding these new indices to the visited set and make a recursive call. We decrement the remaining number, and append the values to our accumulated list.

findKPairs :: V.Vector Int -> V.Vector Int -> Int -> [I2]
findKPairs arr1 arr2 k = ...
  where
    f :: Int -> S.Set I2 -> H.MinHeap (Int, I2, I2) -> [I2] -> [I2]
    f 0 _ _ acc = reverse acc
    f remaining visited heap acc = case H.view heap of
      Nothing -> reverse acc
      Just ((_, (i1, i2), (v1, v2)), restHeap) ->
        let c1 = (i1 + 1, i2)
            c2 = (i1, i2 + 1)
            inc1 = arr1 V.! (i1 + 1) + v2
            inc2 = v1 + arr2 V.! (i2 + 1)
            heap1 = if i1 + 1 < n1 && S.notMember c1 visited
                      then H.insert (inc1, c1, (arr1 V.! (i1 + 1), v2)) restHeap else restHeap
            heap2 = if i2 + 1 < n2 && S.notMember c2 visited
                      then H.insert (inc2, c2, (v1, arr2 V.! (i2 + 1))) heap1 else heap1
            visited' = foldr S.insert visited ([c1, c2] :: [I2])
        in  f (remaining - 1) visited' heap2 ((v1,v2) : acc)

To complete the function, we define our initial heap and make the first call to our loop function:

findKPairs :: V.Vector Int -> V.Vector Int -> Int -> [I2]
findKPairs arr1 arr2 k = f k (S.singleton (0,0)) initialHeap []
  where
    val1 = arr1 V.! 0
    val2 = arr2 V.! 0
    initialHeap = H.singleton (val1 + val2, (0,0), (val1, val2))

    f :: Int -> S.Set I2 -> H.MinHeap (Int, I2, I2) -> [I2] -> [I2]
    f = ...

Now we’re done! Here’s our complete solution:

type I2 = (Int, Int)

findKPairs :: V.Vector Int -> V.Vector Int -> Int -> [I2]
findKPairs arr1 arr2 k = f k (S.singleton (0,0)) initialHeap []
  where
    val1 = arr1 V.! 0
    val2 = arr2 V.! 0
    initialHeap = H.singleton (val1 + val2, (0,0), (val1, val2))

    n1 = V.length arr1
    n2 = V.length arr2

    f :: Int -> S.Set I2 -> H.MinHeap (Int, I2, I2) -> [I2] -> [I2]
    f 0 _ _ acc = reverse acc
    f remaining visited heap acc = case H.view heap of
      Nothing -> reverse acc
      Just ((_, (i1, i2), (v1, v2)), restHeap) ->
        let c1 = (i1 + 1, i2)
            c2 = (i1, i2 + 1)
            inc1 = arr1 V.! (i1 + 1) + v2
            inc2 = v1 + arr2 V.! (i2 + 1)
            heap1 = if i1 + 1 < n1 && S.notMember c1 visited
                      then H.insert (inc1, c1, (arr1 V.! (i1 + 1), v2)) restHeap else restHeap
            heap2 = if i2 + 1 < n2 && S.notMember c2 visited
                      then H.insert (inc2, c2, (v1, arr2 V.! (i2 + 1))) heap1 else heap1
            visited' = foldr S.insert visited ([c1, c2] :: [I2])
        in  f (remaining - 1) visited' heap2 ((v1,v2) : acc)

Rust Solution

Now, on to our Rust solution. We’ll start by defining our terms. These follow the pattern laid out in our algorithm and the Haskell solution:

pub fn k_smallest_pairs(nums1: Vec<i32>, nums2: Vec<i32>, k: i32) -> Vec<Vec<i32>> {
   let mut heap: BinaryHeap<Reverse<(i32, (usize,usize), (i32,i32))>> = BinaryHeap::new();
    let val1 = nums1[0];
    let val2 = nums2[0];
    heap.push(Reverse((val1 + val2, (0,0), (val1, val2))));
    let mut visited: HashSet<(usize, usize)> = HashSet::new();
    visited.insert((0,0));
    let mut results = Vec::new();
    let mut remaining = k;
    let n1 = nums1.len();
    let n2 = nums2.len();
    ...
    return results;
}

The most interesting of these is the heap. We parameterize the type of the BinaryHeap using the same kind of tuple we had in Haskell. But in order to make it a “Min” heap, we have to wrap our values in the Reverse type.

Now let’s define the outline of our loop. We keep going until remaining is 0. We will also break if we can’t pop a value from the heap.

pub fn k_smallest_pairs(nums1: Vec<i32>, nums2: Vec<i32>, k: i32) -> Vec<Vec<i32>> {
    ...
    
    while remaining > 0 {
        if let Some(Reverse((sumNum, (i1, i2), (v1, v2)))) = heap.pop() {
            ...
        } else {
            break;
        }
        remaining -= 1;
    }

    return results;
}

Now we’ll define our new coordinates, and add tests for whether or not these can be added to the heap:

pub fn k_smallest_pairs(nums1: Vec<i32>, nums2: Vec<i32>, k: i32) -> Vec<Vec<i32>> {
    ...
    
    while remaining > 0 {
        if let Some(Reverse((sumNum, (i1, i2), (v1, v2)))) = heap.pop() {
            let c1 = (i1 + 1, i2);
            let c2 = (i1, i2 + 1);
            if i1 + 1 < n1 && !visited.contains(&c1) {
                let inc1 = nums1[i1 + 1] + v2;
                ...
            }
            if i2 + 1 < n2 && !visited.contains(&c2) {
                let inc2 = v1 + nums2[i2 + 1];
                ...
            }
        } else {
            break;
        }
        remaining -= 1;
    }

    return results;
}

In each case, we add the new coordinate to visited, and push the new element on to the heap. We also push the values onto our results array.

pub fn k_smallest_pairs(nums1: Vec<i32>, nums2: Vec<i32>, k: i32) -> Vec<Vec<i32>> {
    ...
    
    while remaining > 0 {
        if let Some(Reverse((sumNum, (i1, i2), (v1, v2)))) = heap.pop() {
            let c1 = (i1 + 1, i2);
            let c2 = (i1, i2 + 1);
            if i1 + 1 < n1 && !visited.contains(&c1) {
                let inc1 = nums1[i1 + 1] + v2;
                visited.insert(c1);
                heap.push(Reverse((inc1, c1, (nums1[i1 + 1], v2))));
            }
            if i2 + 1 < n2 && !visited.contains(&c2) {
                let inc2 = v1 + nums2[i2 + 1];
                visited.insert(c2);
                heap.push(Reverse((inc2, c2, (v1, nums2[i2 + 1]))));
            }
            results.push(vec![v1,v2]);
        } else {
            break;
        }
        remaining -= 1;
    }

    return results;
}

And that’s all we need!

pub fn k_smallest_pairs(nums1: Vec<i32>, nums2: Vec<i32>, k: i32) -> Vec<Vec<i32>> {
    let mut heap: BinaryHeap<Reverse<(i32, (usize,usize), (i32,i32))>> = BinaryHeap::new();
    let val1 = nums1[0];
    let val2 = nums2[0];
    heap.push(Reverse((val1 + val2, (0,0), (val1, val2))));
    let mut visited: HashSet<(usize, usize)> = HashSet::new();
    visited.insert((0,0));
    let mut results = Vec::new();
    let mut remaining = k;
    let n1 = nums1.len();
    let n2 = nums2.len();
    
    while remaining > 0 {
        if let Some(Reverse((sumNum, (i1, i2), (v1, v2)))) = heap.pop() {
            let c1 = (i1 + 1, i2);
            let c2 = (i1, i2 + 1);
            if i1 + 1 < n1 && !visited.contains(&c1) {
                let inc1 = nums1[i1 + 1] + v2;
                visited.insert(c1);
                heap.push(Reverse((inc1, c1, (nums1[i1 + 1], v2))));
            }
            if i2 + 1 < n2 && !visited.contains(&c2) {
                let inc2 = v1 + nums2[i2 + 1];
                visited.insert(c2);
                heap.push(Reverse((inc2, c2, (v1, nums2[i2 + 1]))));
            }
            results.push(vec![v1,v2]);
        } else {
            break;
        }
        remaining -= 1;
    }

    return results;
}

Conclusion

Next time, we’ll start exploring some graph problems, which also rely on data structures like we used here!

I didn’t explain too much in this article about the details of using these various data structures. If you want an in-depth exploration of how data structures work in Haskell, including the “common API” that helps you use almost all of them, you should sign up for our Solve.hs course! Module 2 is completely dedicated to teaching you about data structures, and you’ll get a lot of practice working with these structures in sample problems.

by James Bowen at August 25, 2025 08:30 AM

69: Jurriaan Hage

Today’s guest is Jurriaan Hage. Jurriaan is a professor at Heriot-Watt University in Edinburgh who’s worked with and on Haskell for many years. He’s known for the Helium Haskell compiler, specifically designed for teaching, and he has plenty of other projects related to Haskell, including improvements to the type system, the generation of better error messages, or detection of plagiarism. 

by Haskell Podcast at August 25, 2025 07:00 AM

A Fast Bytecode VM for Arithmetic: The Compiler

In this series of posts, we write a fast bytecode compiler and a virtual machine for arithmetic in Haskell. We explore the following topics:

• Parsing arithmetic expressions to Abstract Syntax Trees (ASTs).
• Unit testing for our parser.
• Interpreting ASTs.
• Compiling ASTs to bytecode.
• Disassembling and decompiling bytecode.
• Unit testing for our compiler.
• Property-based testing for our compiler.
• Efficiently executing bytecode in a virtual machine (VM).
• Unit testing and property-based testing for our VM.
• Benchmarking our code to see how the different passes perform.
• All the while keeping an eye on performance.

In this post, we write the compiler for our AST to bytecode, and a decompiler for the bytecode.

This post was originally published on abhinavsarkar.net.

This is the second post in a series of posts:

1. A Fast Bytecode VM for Arithmetic: The Parser
2. A Fast Bytecode VM for Arithmetic: The Compiler
3. A Fast Bytecode VM for Arithmetic: The Virtual Machine

Introduction

AST interpreters are well known to be slow because of how AST nodes are represented in the computer’s memory. The AST nodes contain pointers to other nodes, which may be anywhere in the memory. So while interpreting an AST, the interpreter jumps all over the memory, causing a slowdown. One solution to this is to convert the AST into a more compact and optimized representation known as Bytecode.

Bytecode is a flattened and compact representation of a program, usually manifested as a byte array. Bytecode is essentially an Instruction Set (IS), but custom-made to be executed by a Virtual Machine (VM), instead of a physical machine. Each bytecode instruction is one byte in size (that’s where it gets its name from). A bytecode and its VM are created in synergy so that the execution is as efficient as possible¹. Compiling source code to bytecode and executing it in a VM also allows the program to be run on all platforms that the VM supports without the developer caring much about portability concerns. The most popular combo of bytecode and VM is probably the Java bytecode and the Java virtual machine.

The VMs can be stack-based or register-based. In a stack-based VM, all values created during the execution of a program are stored only in a Stack data-structure residing in the memory. Whereas, in a register-based VM, there is also an additional set of fixed number of registers that are used to store values in preference to the stack². Register-based VMs are usually faster, but stack-based VMs are usually simpler to implement. For our purpose, we choose to implement a stack-based VM.

We are going to write a compiler that compiles our expression AST to bytecode. But first, let’s design the bytecode for our stack-based VM.

The Bytecode

Here is our expression AST as a reminder:

data Expr
  = Num !Int16
  | Var !Ident
  | BinOp !Op Expr Expr
  | Let !Ident Expr Expr
  deriving (Eq, Generic)

newtype Ident = Ident BS.ByteString
  deriving (Eq, Ord, Generic, Hashable)

data Op = Add | Sub | Mul | Div deriving (Eq, Enum, Generic)

Let’s figure out the right bytecode for each case. First, we create Opcodes for each bytecode, which are sort of mnemonics for actual bytecode. Think of them as Assembly is to Machine Code.

Num

For a number literal, we need to put it directly in the bytecode so that we can use it later during the execution. We also need an opcode to push it on the stack. Let’s call it OPush with an Int16 parameter.

BinOp

Binary operations recursively use Expr for their operands. To evaluate a binary operation, we need its operands to be evaluated before, so we compile them first to bytecode. After that, all we need is an opcode per operator. Let’s call them OAdd, OSub, OMul, and ODiv for Add, Sub, Mul, and Div operators respectively.

Var and Let

Variables and Let expressions are more complex³. In the AST interpreter we chucked the variables in a map, but we cannot do that in a VM. There is no environment map in a VM, and all values must reside in the stack. How do we have variables at all then? Let’s think for a bit.

Each expression, after being evaluated in the VM, must push exactly one value on the stack: its result. Num expressions are a trivial case. When a binary operation is evaluated, first its left operand is evaluated. That pushes one value on the stack. Then its right operand is evaluated, and that pushes another value on the stack. Finally, the operation pops the two values from the top of the stack, does its thing, and pushes the resultant value back on the stack—again one value for the entire BinOp expression.

A Let expression binds a variable’s value to its name, and then the variable can be referred from the body of the expression. But how can we refer to a variable when the stack contains only values, not names? Let’s imagine that we are in middle of evaluating a large expression, wherein we encounter a Let expression. First we evaluate its assignment expression, and that pushes a value on the top of the stack. Let’s say that the stack has n values at this point. After this we get to evaluate the body expression. At all times when we are doing that, the value from assignment stays at the same point in the stack because evaluating sub-expressions, no matter how complicated, only adds new values to the stack, without popping an existing value from before. Therefore, we can use the stack index of the assignment value (n−1) to refer to it from within the body expression. So, we encode Var as an opcode and an integer index into the stack.

We choose to use a Word8 to index the stack, limiting us to a stack depth of 256. We encode the variable references with an opcode OGet, which when executed gets the value from the stack at the given index and pushes it on the stack.

For a Let expression, after we compile its assignment and body expressions, we need to make sure that the exactly-one-value invariant holds. Evaluating the assignment and body pushes two values on the stack, but we can have only one! So we overwrite the assignment value with the body value, and pop the stack to remove the body value. We invent a new opcode OSwapPop to do this, called so because its effect is equivalent to swapping the topmost two values on the stack, and then popping the new top value⁴.

Putting all the opcodes together, we have the Opcode ADT:

data Opcode
  = OPush !Int16        -- 0
  | OSwapPop            -- 1
  | OGet !Word8         -- 2
  | OAdd                -- 3
  | OSub                -- 4
  | OMul                -- 5
  | ODiv                -- 6
  deriving (Show, Read, Eq, Generic)

instance NFData Opcode

Notice that we also assigned bytecodes—that is, a unique byte value—to each Opcode above, which are just their ordinals. Now we are ready to write the compiler.

The Compiler

The compiler takes an expression with the bytecode size, and compiles it to a strict ByteString of that size. Recall that in the previous post, we wrote our parser such that the bytecode size for each AST node was calculated while parsing it. This allows us to pre-allocate a bytestring of required size before compiling the AST. We compile to actual bytes here, and don’t use the opcodes.

type Bytecode = BS.ByteString

compile :: SizedExpr -> Result Bytecode
compile = compile' defaultStackSize

compile' :: Int -> SizedExpr -> Result Bytecode
compile' stackSize (expr, bytecodeSize) =
  uncurry (fmap . const) . BSI.unsafeCreateUptoN' bytecodeSize $ \fp -> do
    (bytecodeSize,)
      <$> fmap
        Right
        (compileIO bytecodeSize stackSize fp fp expr >>= checkSize fp . TS.fst)
        `catch` (pure . Left)
  where
    checkSize fp ip = do
      let actualBytecodeSize = ip `minusPtr` fp
      unless (actualBytecodeSize == bytecodeSize) $
        throwIO . Error Compile $
          "Compiled bytecode size " <> show actualBytecodeSize
            <> " is not same as expected size: " <> show bytecodeSize

compileIO ::
  Int -> Int -> Ptr Word8 -> Ptr Word8 -> Expr -> IO (Pair (Ptr Word8) Int)
compileIO bytecodeSize stackSize fp ip = go Map.empty 0 ip
  where
    ep = fp `plusPtr` bytecodeSize

    go env !sp !ip = \case
      Num n | sp + 1 <= stackSize -> do
        let !lb = fromIntegral $ n .&. 0xff
            !mb = fromIntegral $ ((fromIntegral n :: Word16) .&. 0xff00) `shiftR` 8
        writeByte ip 0 -- OPush
        writeByte (ip `plusPtr` 1) lb
        writeByte (ip `plusPtr` 2) mb
        pure (ip `plusPtr` 3 :!: sp + 1)
      Num _ -> throwCompileError "Stack overflow"
      BinOp op a b -> do
        (ip' :!: sp') <- go env sp ip a
        (ip'' :!: sp'') <- go env sp' ip' b
        writeByte ip'' $ translateOp op
        pure (ip'' `plusPtr` 1 :!: sp'' - 1)
      Let x assign body -> do
        (ip' :!: sp') <- go env sp ip assign
        (ip'' :!: sp'') <- go (Map.insert x sp env) sp' ip' body
        writeByte ip'' 1 -- OSwapPop
        pure (ip'' `plusPtr` 1 :!: sp'' - 1)
      Var x | sp + 1 <= stackSize -> case Map.lookup x env of
        Nothing -> throwCompileError $ "Unknown variable: " <> show x
        Just varScope
          | varScope < stackSize && varScope < fromIntegral (maxBound @Word8) -> do
              writeByte ip 2 -- OGet
              writeByte (ip `plusPtr` 1) $ fromIntegral varScope
              pure (ip `plusPtr` 2 :!: sp + 1)
        Just _ -> throwCompileError "Stack overflow"
      Var _ -> throwCompileError "Stack overflow"

    writeByte :: Ptr Word8 -> Word8 -> IO ()
    writeByte !ip !val
      | ip < ep = poke ip val
      | otherwise = throwCompileError $
          "Instruction index " <> show (ip `minusPtr` fp)
            <> " out of bound " <> show (bytecodeSize - 1)

    translateOp = \case
      Add -> 3 -- OAdd
      Sub -> 4 -- OSub
      Mul -> 5 -- OMul
      Div -> 6 -- ODiv

    throwCompileError = throwIO . Error Compile

defaultStackSize :: Int
defaultStackSize = 256

We use the unsafeCreateUptoN' function from the Data.ByteString.Internal module that allocates enough memory for the provided bytecode size, and gives us a pointer to the allocated memory. We call this pointer fp for frame pointer. Then we traverse the AST recursively, writing bytes for opcodes and arguments for each case. We use pointer arithmetic and the poke function to write the bytes. Int16 numbers are encoded as two bytes in little endian fashion.

In the recursive traversal function go, we pass and return the current stack pointer sp and instruction pointer ip. We update these correctly for each case⁵. We also take care of checking that the pointers stay in the right bounds, failing which we throw appropriate errors.

We also pass an env parameter that is similar to the variable names to values environment we use in the AST interpreter, but this one tracks variable names to stack indices at which they reside. We update this information before compiling the body of a Let expression to capture the stack index of its assignment value. When compiling a Var expression, we use the env map to lookup the variable’s stack index, and encode it in the bytecode.

At the end of compilation, we check that the entire bytestring is filled with bytes till the very end, failing which we throw an error. This check is required because otherwise the bytestring may have garbage bytes, and may fail inexplicably during execution.

All the errors are thrown in the IO monad using the throwIO function, and are caught after compilation using the catch function. The final result or error is returned wrapped into Result.

Let’s see it in action:

$ echo -n "1 + 2 - 3 * 4" | arith-vm compile | hexdump -C
00000000  00 01 00 00 02 00 03 00  03 00 00 04 00 05 04     |...............|
0000000f

$ echo -n "let x = 4 in let y = 5 in x + y" | arith-vm compile | hexdump -C
00000000  00 04 00 00 05 00 02 00  02 01 03 01 01           |.............|
0000000d

You can verify that the resultant bytes are indeed correct. I assume that it is difficult for you to read raw bytes. We’ll fix this in a minute. Meanwhile, let’s ponder upon some performance characteristics of our compiler.

Compiling, Fast and Slow

You may be wondering why I chose to write the compiler in this somewhat convoluted way of pre-allocating a bytestring and using pointers. The answer is: performance. I didn’t actually start with pointers. I iterated through many different data and control structures to find the fastest one.

The table below shows the compilation times for a benchmark expression file when using different data structures to implement the compileIO function:

Data structure	Time (ms)	Incremental speedup	Overall speedup
List	4345	1x	1x
Seq	523	8.31x	8.31x
DList	486	1.08x	8.94x
BS Builder	370	1.31x	11.74x
Pre-allocated BS	54	6.85x	80.46x
Bytearray	52	1.02x	83.55x

I started with the bread-and-butter data structure of Haskellers, the humble and known to be slow List, which was indeed quite slow. Next, I moved on to Seq and thereafter DList, which are known to be faster at concatenation/consing. Then I abandoned the use of intermediate data structures completely, choosing to use a bytestring Builder to create the bytestring. Finally, I had the epiphany that the bytestring size was known at compile time, and rewrote the function to pre-allocate the bytestring, thereby reaching the fastest solution.

I also tried using Bytearray, which has more-or-less same performance of bytestring, but it is inconvenient to use because there are no functions to do IO with bytearrays. So I’d anyway need to use bytestrings for reading from STDIN or writing to STDOUT, and converting to-and-fro between bytearray and bytestring is a performance killer. Thus, I decided to stick to bytestrings.

The pre-allocated bytestring approach is 80 times faster than using lists, and almost 10 times faster than using Seq. For such gain, I’m okay with the complications it brings to the code. Here are the numbers in a chart (smaller is better):

The other important data structure used here is the map (or dictionary) in which we add the mappings from identifiers to their stack indices. This data structure needs to be performant because we do a lookup for each variable we encounter while compiling. I benchmarked compilation for some data structures:

Data structure	Time (ms)	Slowdown
Data.HashMap.Strict.HashMap	55	1.00x
Data.List.List6	63	1.14x
Data.Map.Strict.Map	71	1.29x
Data.Trie.Trie	80	1.45x
Data.Vector.Hashtables.Dictionary	104	1.89x
Data.HashTable.IO.BasicHashTable	312	5.67x

Strict hashmap turns out to be the fasted one, but interestingly, linked list is a close second. Mutable hashtable is the slowest even though I expected it to be the fastest. Here are the times in a chart (smaller is better):

Another choice I had to make was how to write the go function. I ended up passing and returning pointers and environment map, and throwing errors in IO, but a number of solutions are possible. I tried out some of them, and noted the compilation times for the benchmark expression file:

Control structure	Time (ms)	Slowdown
IO	57.4	1.00x
IO + IORef	65.0	1.13x
IO + ReaderT	60.9	1.06x
IO + StateT	65.6	1.14x
IO + ExceptT	65.9	1.15x
IO + ReaderT + ExceptT	107.1	1.87x
IO + StateT + ExceptT	383.9	6.69x
IO + StateT + ReaderT	687.5	11.98x
IO + StateT + ReaderT + ExceptT	702.0	12.23x
IO + CPS	78.2	1.36x
IO + DCPS	78.4	1.37x
IO + ContT	76.5	1.33x

I tried putting the pointer in IORefs and StateT state instead of passing them back-and-forth. I tried putting the environment in a ReaderT config. I tried using ExceptT for throwing errors instead of using IO errors. Then I tried various combinations of these monad transformers.

Finally, I also tried converting the go function to be tail-recursive by using Continuation-passing style (CPS), and then defunctionalizing the continuations, as well as, using the ContT monad transformer. All of these approaches resulted in slower code. The times are interesting to compare (smaller is better):

There is no reason to use IORefs here because they result in slower and uglier code. Using one monad transformer at a time results in slight slowdowns, which may be worth the improvement in the code. But using more than one of them degrades performance by a lot. Also, there is no improvement caused by CPS conversion, because GHC is smart enough to optimize the non tail-recursive code to be faster then handwritten tail-recursive one that allocates a lot of closures (or objects in case of defunctionalization).

Moving on …

The Decompiler

It is a hassle to read raw bytes in the compiler output. Let’s write a decompiler to aid us in debugging and testing the compiler. First, a disassembler that converts bytes to opcodes:

type Program = Seq Opcode

disassemble :: Bytecode -> Result Program
disassemble bytecode = go 0 Seq.empty
  where
    !size = BS.length bytecode

    go !ip !program
      | ip == size = pure program
      | otherwise = case readInstr bytecode ip of
          0 | ip + 2 < size ->
            go (ip + 3) $ program |> OPush (readInstrArgInt16 bytecode ip)
          0 -> throwIPOOBError $ ip + 2
          1 -> go (ip + 1) $ program |> OSwapPop
          2 | ip + 1 < size ->
            go (ip + 2) $ program |> OGet (readInstrArgWord8 bytecode ip)
          2 -> throwIPOOBError $ ip + 1
          3 -> go (ip + 1) $ program |> OAdd
          4 -> go (ip + 1) $ program |> OSub
          5 -> go (ip + 1) $ program |> OMul
          6 -> go (ip + 1) $ program |> ODiv
          n -> throwDisassembleError $
            "Invalid bytecode: " <> show n <> " at: " <> show ip

    throwIPOOBError ip = throwDisassembleError $
      "Instruction index " <> show ip <> " out of bound " <> show (size - 1)

    throwDisassembleError = throwError . Error Disassemble

A disassembled program is a sequence of opcodes. We simply go over each byte of the bytecode, and append the right opcode for it to the program, along with any parameters it may have. Note that we do not verify that the disassembled program is correct.

Here are the helpers that read instruction bytes and their arguments from a bytestring:

readInstr :: BS.ByteString -> Int -> Word8
readInstr = BS.unsafeIndex
{-# INLINE readInstr #-}

readInstrArgWord8 :: BS.ByteString -> Int -> Word8
readInstrArgWord8 bytecode ip = readInstr bytecode (ip + 1)
{-# INLINE readInstrArgWord8 #-}

readInstrArgInt16 :: BS.ByteString -> Int -> Int16
readInstrArgInt16 bytecode ip =
  let lb = readInstr bytecode (ip + 1)
      mb = readInstr bytecode (ip + 2)
      b1 :: Word16 = fromIntegral lb
      b2 = fromIntegral mb `shiftL` 8
   in fromIntegral (b1 .|. b2)
{-# INLINE readInstrArgInt16 #-}

Next, we decompile the opcodes to an expression:

decompile :: Program -> Result Expr
decompile program = do
  stack <- go Seq.empty program
  checkStack Decompile maxBound $ length stack
  let ast :<| _ = stack
  pure ast
  where
    go stack = \case
      Seq.Empty -> pure stack
      opcode :<| rest -> case opcode of
        OPush n -> go (stack |> Num n) rest
        OAdd -> decompileBinOp Add >>= flip go rest
        OSub -> decompileBinOp Sub >>= flip go rest
        OMul -> decompileBinOp Mul >>= flip go rest
        ODiv -> decompileBinOp Div >>= flip go rest
        OGet i -> go (stack |> Var (mkIdent $ mkName $ fromIntegral i)) rest
        OSwapPop -> decompileLet >>= flip go rest
      where
        decompileBinOp op = case stack of
          stack' :|> a :|> b -> pure $ stack' |> BinOp op a b
          _ -> throwDecompileError $
            "Not enough elements to decompile binary operation: " <> show op

        decompileLet = case stack of
          stack' :|> a :|> b ->
            pure $ stack' |> Let (mkIdent $ mkName $ length stack - 2) a b
          _ -> throwDecompileError "Not enough elements to decompile let"

    mkName i = names `Seq.index` i
    names = Seq.fromList $ tail $ combinations 2

    combinations = \case
      0 -> [""]
      n -> let prev = combinations (n - 1)
        in prev <> [x : xs | x <- ['a' .. 'z'], xs <- prev]

    throwDecompileError = throwError . Error Decompile

checkStack :: (MonadError Error m) => Pass -> Int -> Int -> m ()
checkStack pass stackSize = \case
  1 -> pure ()
  0 -> throwError $ Error pass "Final stack has no elements"
  n | n > stackSize -> throwError . Error pass $ "Stack overflow"
  n | n > 1 -> throwError . Error pass $ "Final stack has more than one element"
  _ -> throwError . Error pass $ "Stack underflow"

Decompilation is the opposite of compilation. While compiling there is an implicit stack of expressions that are yet to be compiled. We make that stack explicit here, capturing expressions as they are decompiled from opcodes. For compound expressions, we inspect the stack and use the already decompiled expressions as the operands of the expression being decompiled. This way we build up larger expressions from smaller ones, culminating in the single top-level expression at the end⁷. Finally, we check the stack to make sure that there is only one expression left in it. Note that like the disassembler, we do not verify that the decompiled expression is correct.

There is one tricky thing in decompilation: we lose the names of the variables when compiling, and are left with only stack indices. So while decompiling, we generate variable names from their stack indices by indexing a list of unique names. Let’s see it in action:

$ echo -n "1 + 2 - 3 * 4" | arith-vm compile | arith-vm disassemble
OPush 1
OPush 2
OAdd
OPush 3
OPush 4
OMul
OSub

$ echo -n "1 + 2 - 3 * 4" | arith-vm compile | arith-vm decompile
( ( 1 + 2 ) - ( 3 * 4 ) )

$ echo -n "let x = 4 in let y = 5 in x + y" | arith-vm compile | arith-vm disassemble
OPush 4
OPush 5
OGet 0
OGet 1
OAdd
OSwapPop
OSwapPop

$ echo -n "let x = 4 in let y = 5 in x + y" | arith-vm compile | arith-vm decompile
( let a = 4 in ( let b = 5 in ( a + b ) ) )

That’s all for compilation and decompilation. Now, we use them together to make sure that everything works.

Testing the Compiler

We write some unit tests for the compiler, targeting both success and failure cases:

compilerSpec :: Spec
compilerSpec = describe "Compiler" $ do
  forM_ compilerSuccessTests $ \(input, result) ->
    it ("compiles: \"" <> BSC.unpack input <> "\"") $ do
      parseCompile input `shouldBe` Right (Seq.fromList result)

  forM_ compilerErrorTests $ \(input, err) ->
    it ("fails for: \"" <> BSC.unpack input <> "\"") $ do
      parseCompile input `shouldSatisfy` \case
        Left (Error Compile msg) | err == msg -> True
        _ -> False

  it "fails for greater sized expr" $ do
    compile (Num 1, 4) `shouldSatisfy` \case
      Left
        ( Error Compile "Compiled bytecode size 3 is not same as expected size: 4"
        ) -> True
      _ -> False

  it "fails for lesser sized expr" $ do
    compile (Num 1, 2) `shouldSatisfy` \case
      Left (Error Compile "Instruction index 2 out of bound 1") -> True
      _ -> False
  where
    parseCompile = parseSized >=> compile' 4 >=> disassemble

compilerSuccessTests :: [(BSC.ByteString, [Opcode])]
compilerSuccessTests =
  [ ( "1",
      [OPush 1]
    ),
    ( "1 + 2 - 3 * 4 + 5 / 6 / 1 + 1",
      [ OPush 1, OPush 2, OAdd, OPush 3, OPush 4, OMul, OSub, OPush 5, OPush 6,
        ODiv, OPush 1, ODiv, OAdd, OPush 1, OAdd ]
    ),
    ( "1 + (2 - 3) * 4 + 5 / 6 / (1 + 1)",
      [ OPush 1, OPush 2, OPush 3, OSub, OPush 4, OMul, OAdd, OPush 5, OPush 6,
        ODiv, OPush 1, OPush 1, OAdd, ODiv, OAdd ]
    ),
    ( "let x = 4 in x + 1",
      [OPush 4, OGet 0, OPush 1, OAdd, OSwapPop]
    ),
    ( "let x = 4 in let y = 5 in x + y",
      [OPush 4, OPush 5, OGet 0, OGet 1, OAdd, OSwapPop, OSwapPop]
    ),
    ( "let x = 4 in let x = x + 1 in x + 2",
      [OPush 4, OGet 0, OPush 1, OAdd, OGet 1, OPush 2, OAdd, OSwapPop, OSwapPop]
    ),
    ( "let x = let y = 3 in y + y in x * 3",
      [ OPush 3, OGet 0, OGet 0, OAdd, OSwapPop, OGet 0, OPush 3, OMul, OSwapPop ]
    ),
    ( "let x = let y = 1 + let z = 2 in z * z in y + 1 in x * 3",
      [ OPush 1, OPush 2, OGet 1, OGet 1, OMul, OSwapPop, OAdd, OGet 0, OPush 1,
        OAdd, OSwapPop, OGet 0, OPush 3, OMul, OSwapPop ]
    ),
    ("1/0", [OPush 1, OPush 0, ODiv]),
    ("-32768 / -1", [OPush (-32768), OPush (-1), ODiv])
  ]

compilerErrorTests :: [(BSC.ByteString, String)]
compilerErrorTests =
  [ ("x", "Unknown variable: x"),
    ("let x = 4 in y + 1", "Unknown variable: y"),
    ("let x = y + 1 in x", "Unknown variable: y"),
    ("let x = x + 1 in x", "Unknown variable: x"),
    ("let x = 4 in let y = 1 in let z = 2 in y + x", "Stack overflow"),
    ("let x = 4 in let y = 5 in x + let z = y in z * z", "Stack overflow"),
    ("let a = 0 in let b = 0 in let c = 0 in let d = 0 in d", "Stack overflow")
  ]

In each test, we parse and compile an expression, and then disassemble the compiled bytes, which we match with expected list of opcodes, or an error message.

Let’s put these tests with the parser tests, and run them:

main :: IO ()
main = hspec $ do
  parserSpec
  astInterpreterSpec
  compilerSpec

Output of the test run

$ cabal test -O2
Running 1 test suites...
Test suite specs: RUNNING...

Parser
  parses: "1 + 2 - 3 * 4 + 5 / 6 / 0 + 1" [✔]
  parses: "1+2-3*4+5/6/0+1" [✔]
  parses: "1 + -1" [✔]
  parses: "let x = 4 in x + 1" [✔]
  parses: "let x=4in x+1" [✔]
  parses: "let x = 4 in let y = 5 in x + y" [✔]
  parses: "let x = 4 in let y = 5 in x + let z = y in z * z" [✔]
  parses: "let x = 4 in (let y = 5 in x + 1) + let z = 2 in z * z" [✔]
  parses: "let x=4in 2+let y=x-5in x+let z=y+1in z/2" [✔]
  parses: "let x = (let y = 3 in y + y) in x * 3" [✔]
  parses: "let x = let y = 3 in y + y in x * 3" [✔]
  parses: "let x = let y = 1 + let z = 2 in z * z in y + 1 in x * 3" [✔]
  fails for: "" [✔]
  fails for: "1 +" [✔]
  fails for: "1 & 1" [✔]
  fails for: "1 + 1 & 1" [✔]
  fails for: "1 & 1 + 1" [✔]
  fails for: "(" [✔]
  fails for: "(1" [✔]
  fails for: "(1 + " [✔]
  fails for: "(1 + 2" [✔]
  fails for: "(1 + 2}" [✔]
  fails for: "66666" [✔]
  fails for: "-x" [✔]
  fails for: "let 1" [✔]
  fails for: "let x = 1 in " [✔]
  fails for: "let let = 1 in 1" [✔]
  fails for: "let x = 1 in in" [✔]
  fails for: "let x=1 inx" [✔]
  fails for: "letx = 1 in x" [✔]
  fails for: "let x ~ 1 in x" [✔]
  fails for: "let x = 1 & 2 in x" [✔]
  fails for: "let x = 1 inx" [✔]
  fails for: "let x = 1 in x +" [✔]
  fails for: "let x = 1 in x in" [✔]
  fails for: "let x = let x = 1 in x" [✔]
AST interpreter
  interprets: "1" [✔]
  interprets: "1 + 2 - 3 * 4 + 5 / 6 / 1 + 1" [✔]
  interprets: "1 + (2 - 3) * 4 + 5 / 6 / (1 + 1)" [✔]
  interprets: "1 + -1" [✔]
  interprets: "1 * -1" [✔]
  interprets: "let x = 4 in x + 1" [✔]
  interprets: "let x = 4 in let x = x + 1 in x + 2" [✔]
  interprets: "let x = 4 in let y = 5 in x + y" [✔]
  interprets: "let x = 4 in let y = 5 in x + let z = y in z * z" [✔]
  interprets: "let x = 4 in (let y = 5 in x + y) + let z = 2 in z * z" [✔]
  interprets: "let x = let y = 3 in y + y in x * 3" [✔]
  interprets: "let x = let y = 1 + let z = 2 in z * z in y + 1 in x * 3" [✔]
  fails for: "x" [✔]
  fails for: "let x = 4 in y + 1" [✔]
  fails for: "let x = y + 1 in x" [✔]
  fails for: "let x = x + 1 in x" [✔]
  fails for: "1/0" [✔]
  fails for: "-32768 / -1" [✔]
Compiler
  compiles: "1" [✔]
  compiles: "1 + 2 - 3 * 4 + 5 / 6 / 1 + 1" [✔]
  compiles: "1 + (2 - 3) * 4 + 5 / 6 / (1 + 1)" [✔]
  compiles: "let x = 4 in x + 1" [✔]
  compiles: "let x = 4 in let y = 5 in x + y" [✔]
  compiles: "let x = 4 in let x = x + 1 in x + 2" [✔]
  compiles: "let x = let y = 3 in y + y in x * 3" [✔]
  compiles: "let x = let y = 1 + let z = 2 in z * z in y + 1 in x * 3" [✔]
  compiles: "1/0" [✔]
  compiles: "-32768 / -1" [✔]
  fails for: "x" [✔]
  fails for: "let x = 4 in y + 1" [✔]
  fails for: "let x = y + 1 in x" [✔]
  fails for: "let x = x + 1 in x" [✔]
  fails for: "let x = 4 in let y = 1 in let z = 2 in y + x" [✔]
  fails for: "let x = 4 in let y = 5 in x + let z = y in z * z" [✔]
  fails for: "let a = 0 in let b = 0 in let c = 0 in let d = 0 in d" [✔]
  fails for greater sized expr [✔]
  fails for lesser sized expr [✔]

Finished in 0.0147 seconds
73 examples, 0 failures
Test suite specs: PASS

Awesome, it works! That’s it for this post. Let’s update our checklist:

• Parsing arithmetic expressions to Abstract Syntax Trees (ASTs).
• Unit testing for our parser.
• Interpreting ASTs.
• Compiling ASTs to bytecode.
• Disassembling and decompiling bytecode.
• Unit testing for our compiler.
• Property-based testing for our compiler.
• Efficiently executing bytecode in a virtual machine (VM).
• Unit testing and property-based testing for our VM.
• Benchmarking our code to see how the different passes perform.
• All the while keeping an eye on performance.

In the next part, we write a virtual machine that runs our compiled bytecode, and do some benchmarking.

If you have any questions or comments, please leave a comment below. If you liked this post, please share it. Thanks for reading!

---

1. There are VMs that execute hardware ISs instead of bytecode. Such VMs are also called Emulators because they emulate actual CPU hardware. Some examples are QEMU and video game console emulators.↩︎

2. VMs use virtual registers instead of actual CPU registers, which are often represented as a fixed size array of 1, 2, 4 or 8 byte elements.↩︎

3. I call them variables here but they do not actually vary. A better name is let bindings.↩︎

4. We could have used two separate opcodes here: OSwap and OPop. That would result in same final result when evaluating an expression, but we’d have to execute two instructions instead of one for Let expressions. Using a single OSwapPop instruction speeds up execution, not only because we reduce the number of instructions, but also because we don’t need to do a full swap, only a half swap is enough because we pop the stack anyway after the swap. This also shows how we can improve the performance of our VMs by inventing specific opcodes for particular operations.↩︎

5. Notice the use of strict Pairs here, for performance reasons.↩︎

6. Used as Association List.↩︎

7. The decompiler is a bottom-up shift-reduce parser from the opcodes to the expression tree.↩︎

If you liked this post, please leave a comment.

by Abhinav Sarkar (abhinav@abhinavsarkar.net) at August 24, 2025 12:00 AM

Functional data structures in Swift

Functional data structures in Swift

One of the intriguing features of Swift is its distinction between value types and reference types. Conceptually, value types are always copied in assignments and passed-by-value in function calls — i.e., they are semantically immutable. In contrast, for reference types, Swift only copies a pointer to an object on an assignment and they are being passed-by-reference to functions. If such an object gets mutated, it changes for for all references. While most languages feature both value and reference types, Swift is unique in that (1) it makes it easy to define and use both flavours of types and (2) it supports fine-grained mutability control.

For large values, such as arrays, frequent copying carries a significant performance penalty. Hence, the Swift compiler goes to great length to avoid copying whenever it is safe. For large values, this effectively boils down to a copy-on-write strategy, where a large value is only copied when it actually is being mutated (on one code path). Swift facilitates for user-defined value types to also adopt this copy-on-write strategy.

In this talk, I will explain the semantic difference between value and reference types, and I will illustrate how this facilitates safe and robust coding practices in Swift. Moreover, I will explain how the copy-on-write strategy for large values works and how it interacts with Swift’s memory management system. Finally, I will demonstrate how you can define your own copy-on-write large value types.

August 23, 2025 04:19 PM

Arithmetic Functions

Introduction

I want to talk about one of the many pretty areas of number theory. This involves the notion of an arithmetic function and related concepts. A few relatively simple concepts will allow us to produce a variety of useful functions and theorems. This provides only a glimpse of the start of the field of analytic number theory, though many of these techniques are used in other places as we’ll also start to see.

(See the end for a summary of identities and results.)

Prelude

As some notation, I’ll write |\mathbb N_+| for the set of positive naturals, and |\mathbb P| for the set of primes. |\mathbb N| will contain |0|. Slightly atypically, I’ll write |[n]| for the set of numbers from |1| to |n| inclusive, i.e. |a \in [n]| if and only if |1 \leq a \leq n|.

I find that the easiest way to see results in number theory is to view a positive natural number as a multiset of primes which is uniquely given by factorization. Coprime numbers are ones where these multisets are disjoint. Multiplication unions the multisets. The greatest common divisor is multiset intersection. |n| divides |m| if and only if |n| corresponds to a sub-multiset of |m|, in which case |m/n| corresponds to the multiset difference. The multiplicity of an element of a multiset is the number of occurrences. For a multiset |P|, |\mathrm{dom}(P)| is the set of elements of the multiset |P|, i.e. those with multiplicity greater than |0|. For a finite multiset |P|, |\vert P\vert| will be the sum of the multiplicities of the distinct elements, i.e. the number of elements (with duplicates) in the multiset.

We can represent a multiset of primes as a function |\mathbb P \to \mathbb N| which maps an element to its multiplicity. A finite multiset would then be such a function that is |0| at all but finitely many primes. Alternatively, we can represent the multiset as a partial function |\mathbb P \rightharpoonup \mathbb N_+|. It will be finite when it is defined for only finitely many primes. Equivalently, when it is a finite subset of |\mathbb P\times\mathbb N_+| (which is also a functional relation).

Unique factorization provides a bijection between finite multisets of primes and positive natural numbers. Given a finite multiset |P|, the corresponding positive natural number is |n_P = \prod_{(p, k) \in P} p^k|.

I will refer to this view often in the following.

Arithmetic Functions

An arithmetic function is just a function defined on the positive naturals. Usually, they’ll land in (not necessarily positive) natural numbers, but that isn’t required.

In most cases, we’ll be interested in the specific subclass of multiplicative arithmetic functions. An arithmetic function, |f|, is multiplicative if |f(1) = 1| and |f(ab) = f(a)f(b)| whenever |a| and |b| are coprime. We also have the notion of a completely multiplicative arithmetic function for which |f(ab) = f(a)f(b)| always. Obviously, completely multiplicative functions are multiplicative. Analogously, we also have a notion of (completely) additive where |f(ab) = f(a) + f(b)|. Warning: In other mathematical contexts, “additive” means |f(a+b)=f(a)+f(b)|. An obvious example of a completely additive function being the logarithm. Exponentiating an additive function will produce a multiplicative function.

For an additive function, |f|, we automatically get |f(1) = 0| since |f(1) = f(1\cdot 1) = f(1) + f(1)|.

Lemma: The product of two multiplicative functions |f| and |g| is multiplicative.
Proof: For |a| and |b| coprime, |f(ab)g(ab) = f(a)f(b)g(a)g(b) = f(a)g(a)f(b)g(b)|. |\square|

A parallel statement holds for completely multiplicative functions.

It’s also clear that a completely multiplicative function is entirely determined by its action on prime numbers. Since |p^n| is coprime to |q^n| whenever |p| and |q| are coprime, we see that a multiplicative function is entirely determined by its action on powers of primes. To this end, I’ll often define multiplicative/additive functions by their action on prime powers and completely multiplicative/additive functions by their action on primes.

Multiplicative functions aren’t closed under composition, but we do have that if |f| is completely multiplicative and |g| is multiplicative, then |f \circ g| is multiplicative when that composite makes sense.

Here are some examples. Not all of these will be used in the sequel.

• The power function |({-})^z| for any |z|, not necessarily an integer, is completely multiplicative.
• Choosing |z=0| in the previous, we see the constantly one function |\bar 1(n) = 1| is completely multiplicative.
• The identity function is clearly completely multiplicative and is also the |z=1| case of the above.
• The Kronecker delta function |\delta(n) = \begin{cases}1, & n = 0 \\ 0, & n \neq 0\end{cases}| is completely multiplicative. Often written |\varepsilon| in this context.
• Define a multiplicative function via |\mu(p^n) = \begin{cases} -1, & n = 1 \\ 0, & n > 1\end{cases}| where |p| is prime. This is the Möbius function. More holistically, |\mu(n)| is |0| if |n| has any square factors, otherwise |\mu(n) = (-1)^k| where |k| is the number of (distinct) prime factors.
• Define a completely multiplicative function via |\lambda(p) = -1|. |\lambda(n) = \pm 1| depending on whether there is an even or odd number of prime factors (including duplicates). This function is known as the Liouville function.
• |\lambda(n) = (-1)^{\Omega(n)}| where |\Omega(n)| is the completely additive function which counts the number of prime factors of |n| including duplicates. |\Omega(n_P) = \vert P\vert|.
• Define a multiplicative function via |\gamma(p^n) = -1|. |\gamma(n) = \pm 1| depending on whether there is an even or odd number of distinct prime factors.
• |\gamma(n) = (-1)^{\omega(n)}| where |\omega(n)| is the additive function which counts the number of distinct prime factors of |n|. See Prime omega function. We also see that |\omega(n_P) = \vert\mathrm{dom}(P)\vert|.
• The completely additive function for |q\in\mathbb P|, |\nu_q(p) = \begin{cases}1,&p=q\\0,&p\neq q\end{cases}| is the p-adic valuation.
• It follows that the |p|-adic absolute value |\vert r\vert_p = p^{-\nu_p(r)}| is completely multiplicative. It can be characterized on naturals by |\vert p\vert_q = \begin{cases}p^{-1},&p=q\\1,&p\neq q\end{cases}|.
• |\gcd({-}, k)| for a fixed |k| is multiplicative. Given any multiplicative function |f|, |f \circ \gcd({-},k)| is multiplicative. This essentially “restricts” |f| to only see the prime powers that divide |k|. Viewing the finite multiset of primes |P| as a function |\mathbb P\to\mathbb N|, |f(\gcd(p^n,n_P)) = \begin{cases}f(p^n),&n\leq P(p)\\f(p^{P(p)}),&n>P(p)\end{cases}|.
• The multiplicative function characterized by |a(p^n) = p(n)| where |p(n)| is the partition function counts the number of abelian groups the given order. That this function is multiplicative is a consequence of the fundamental theorem of finite abelian groups.
• The Jacobi symbol |\left(\frac{a}{n}\right)| where |a\in\mathbb Z| and |n| is an odd positive integer is a completely multiplicative function with either |a| or |n| fixed. When |n| is an odd prime, it reduces to the Legendre symbol. For |p| an odd prime, we have |(\frac{a}{p}) = a^{\frac{p-1}{2}} \pmod p|. This will always be in |\{-1, 0, 1\}| and can be alternately defined as |\left(\frac{a}{p}\right) = \begin{cases}0,&p\mid a\\1,&p\nmid a\text{ and }\exists x.x^2\equiv a\pmod p\\-1,&\not\exists x.x^2\equiv a\pmod p\end{cases}|. Therefore, |\left(\frac{a}{p}\right)=1| (|=0|) when |a| is a (trivial) quadratic residue mod |p|.
• An interesting example which is not multiplicative nor additive is the arithmetic derivative. Let |p\in\mathbb P|. Define |\frac{\partial}{\partial p}(n)| via |\frac{\partial}{\partial p}(p) = 1|, |\frac{\partial}{\partial p}(q) = 0| for |q\neq p| and |q\in\mathbb P|, and |\frac{\partial}{\partial p}(nm) = \frac{\partial}{\partial p}(n)m + n\frac{\partial}{\partial p}(m)|. We then have |D_S = \sum_{p\in S}\frac{\partial}{\partial p}| for non-empty |S\subseteq\mathbb P| which satisfies the same product rule identity. This perspective views a natural number (or, more generally, a rational number) as a monomial in infinitely many variables labeled by prime numbers.
• A Dirichlet character of modulus |m| is, by definition, a completely multiplicative function |\chi| satisfying |\chi(n + m) = \chi(n)| and |\chi(n)| is non-zero if and only if |n| is coprime to |m|. The Jacobi symbol |\left(\frac{({-})}{m}\right)| is a Dirichlet character of modulus |m|. |\bar 1| is the Dirichlet character of modulus |1|.

Dirichlet Series

Given an arithmetic function |f|, we define the Dirichlet series:

\[\mathcal D[f](s) = \sum_{n=1}^\infty \frac{f(n)}{n^s} = \sum_{n=1}^\infty f(n)n^{-s}\]

When |f| is a Dirichlet character, |\chi|, this is referred to as the (Dirichlet) |L|-series of the character, and the analytic continuation is the (Dirichlet) |L|-function and is written |L(s, \chi)|.

We’ll not focus much on when such a series converges. See this section of the above Wikipedia article for more details. Alternatively, we could talk about formal Dirichlet series. We can clearly see that if |s = 0|, then we get the sum |\sum_{n=1}^\infty f(n)| which clearly won’t converge for, say, |f = \bar 1|. We can say that if |f| is asymptotically bounded by |n^k| for some |k|, i.e. |f \in O(n^k)|, then the series will converge absolutely when the real part of |s| is greater than |k+1|. For |\bar 1|, it follows that |\mathcal D[\bar 1](x + iy)| is defined when |x > 1|. We can use analytic continuation to go beyond these limits.

See A Catalog of Interesting Dirichlet Series for a more reference-like listing. Beware differences in notation.

Dirichlet Convolution

Why is this interesting in this context? Let’s consider two arithmetic functions |f| and |g| and multiply their corresponding Dirichlet series. We’ll get:

\[\mathcal D[f](s)\mathcal D[g](s) = \sum_{n=1}^\infty h(n)n^{-s} = \mathcal D[h](s)\]

where now we need to figure out what |h(n)| is. But |h(n)| is going to be the sum of all the terms of the form |f(a)a^{-s}g(b)b^{-s} = f(a)g(b)(ab)^{-s}| where |ab = n|. We can thus write: \[h(n) = \sum_{ab=n} f(a)g(b) = \sum_{d\mid n} f(d)g(n/d)\] We’ll write this more compactly as |h = f \star g| which we’ll call Dirichlet convolution. We have thus shown a convolution theorem of the form \[\mathcal D[f]\mathcal D[g] = \mathcal D[f \star g]\]

The Kronecker delta serves as a unit to this operation which is reflected by |\mathcal D[\delta](s) = 1|.

In the same way we can view a sum of the form |\sum_{a+b=n}f(a)g(b)| that arises in “normal” convolution as a sum along the line |y = n - x|, we can view the sum |\sum_{ab=n}f(a)g(b)| as a sum along a hyperbola of the form |y = n/x|. For all of |\sum_{n=1}^\infty\sum_{k=1}^\infty f(n)g(k)|, |\sum_{n=1}^\infty\sum_{k=1}^n f(k)g(n-k)|, and |\sum_{n=1}^\infty\sum_{k\mid n}f(k)g(n/k)| we’re including |f(a)g(b)| for every |(a,b)\in\mathbb N_+\times\mathbb N_+| in the sum exactly once. The difference is whether we’re grouping the internal sum by rows, diagonals, or hyperbolas. This idea of summing hyperbolas can be expanded to a computational technique for sums of multiplicative functions called the Dirichlet hyperbola method.

Since we will primarily be interested in multiplicative functions, we should check that |f \star g| is a multiplicative function when |f| and |g| are.

Lemma: Assume |a| and |b| are coprime, and |f| and |g| are multiplicative. Then |(f \star g)(ab) = (f \star g)(a)(f \star g)(b)|.

Proof: Since |a| and |b| are coprime, they share no divisors besides |1|. This means every |d| such that |d \mid ab| factors as |d = d_a d_b| where |d_a \mid a| and |d_b \mid b|. More strongly, write |D_n = \{ d \in \mathbb N_+ \mid d \mid n\}|, then for any coprime pair of numbers |i| and |j|, we have |D_{ij} \cong D_i \times D_j| and that every pair |(d_i, d_j) \in D_i \times D_j| are coprime¹. Thus,

\[\begin{flalign} (f \star g)(ab) & = \sum_{d \in D_{ab}} f(d)g((ab)/d) \tag{by definition} \\ & = \sum_{(d_a, d_b) \in D_a \times D_b} f(d_a d_b)g((ab)/(d_a d_b)) \tag{via the bijection} \\ & = \sum_{(d_a, d_b) \in D_a \times D_b} f(d_a)f(d_b)g(a/d_a)g(b/d_b) \tag{f and g are multiplicative} \\ & = \sum_{d_a \in D_a} \sum_{d_b \in D_b} f(d_a)f(d_b)g(a/d_a)g(b/d_b) \tag{sum over a Cartesian product} \\ & = \sum_{d_a \in D_a} f(d_a)g(a/d_a) \sum_{d_b \in D_b} f(d_b)g(b/d_b) \tag{undistributing} \\ & = \sum_{d_a \in D_a} f(d_a)g(a/d_a) (f \star g)(b) \tag{by definition} \\ & = (f \star g)(b) \sum_{d_a \in D_a} f(d_a)g(a/d_a) \tag{undistributing} \\ & = (f \star g)(b) (f \star g)(a) \tag{by definition} \\ & = (f \star g)(a) (f \star g)(b) \tag{commutativity of multiplication} \end{flalign}\] |\square|

It is not the case that the Dirichlet convolution of two completely multiplicative functions is completely multiplicative.

We can already start to do some interesting things with this. First, we see that |\mathcal D[\bar 1] = \zeta|, the Riemann zeta function. Now consider |(\bar 1 \star \bar 1)(n) = \sum_{k \mid n} 1 = d(n)|. |d(n)| is the divisor function which counts the number of divisors of |n|. We see that |\mathcal D[d](s) = \zeta(s)^2|. A simple but useful fact is |\zeta(s - z) = \mathcal D[(-)^z](s)|. This directly generalizes the result for |\mathcal D[\bar 1]| and also implies |\mathcal D[\operatorname{id}](s) = \zeta(s - 1)|.

Generalizing in a different way, we get the family of functions |\sigma_k = ({-})^k \star \bar 1|. |\sigma_k(n) = \sum_{d \mid n} d^k|. From the above, we see |\mathcal D[\sigma_k](s) = \zeta(s - k)\zeta(s)|.

Lemma: Given a completely multiplicative function |f|, we get |f(n)(g \star h)(n) = (fg \star fh)(n)|.
Proof: \[\begin{flalign} (fg \star fh)(n) & = \sum_{d \mid n} f(d)g(d)f(n/d)h(n/d) \\ & = \sum_{d \mid n} f(d)f(n/d)g(d)h(n/d) \\ & = \sum_{d \mid n} f(n)g(d)h(n/d) \\ & = f(n)\sum_{d \mid n} g(d)h(n/d) \\ & = f(n)(g \star h)(n) \end{flalign}\] |\square|

As a simple corollary, for a completely multiplicative |f|, |f \star f = f(\bar 1 \star \bar 1) = fd|.

Euler Product Formula

However, the true power of this is unlocked by the following theorem:

Theorem (Euler product formula): Given a multiplicative function |f| which doesn’t grow too fast, e.g. is |O(n^k)| for some |k > 0|, \[\mathcal D[f](s) = \sum_{n=1}^\infty f(n)n^{-s} = \prod_{p \in \mathbb P}\sum_{n=0}^\infty f(p^n)p^{-ns} = \prod_{p \in \mathbb P}\left(1 + \sum_{n=1}^\infty f(p^n)p^{-ns}\right) \] where the series converges.

Proof: The last equality is simply using the fact that |f(p^0)p^0 = f(1) = 1| because |f| is multiplicative. The idea for the main part is similar to how we derived Dirichlet convolution. When we start to distribute out the infinite product, each term will correspond to the product of selections of a term from each series. When all but finitely many of those selections select the |1| term, we get |\prod_{(p, k) \in P}f(p^k)(p^k)^{-s}| where |P| is some finite multiset of primes induced by those selections. Therefore, |\prod_{(p, k) \in P}f(p^k)(p^k)^{-s} = f(n_P)n_P^{-s}|. Thus, by unique factorization, |f(n)n^{-s}| for every positive natural occurs in the sum produced by distributing the right-hand side exactly once.

In the case where |P| is not a finite multiset, we’ll have \[ \frac{\prod_{(p, k) \in P}f(p^k)}{\left(\prod_{(p, k) \in P}p^k\right)^s}\]

The denominator of this expression goes to infinity when the real part of |s| is greater than |0|. As long as the numerator doesn’t grow faster than the denominator (perhaps after restricting the real part of |s| to be greater than some bound), then this product goes to |0|. Therefore, the only terms that remain are these corresponding to the Dirichlet series on the left-hand side. |\square|

If we assume |f| is completely multiplicative, we can further simplify Euler’s product formula via the usual sum of a geometric series, |\sum_{n=0}^\infty x^n = (1-x)^{-1}|, to:

\[ \sum_{n=1}^\infty f(n)n^{-s} = \prod_{p \in \mathbb P}\sum_{n=0}^\infty (f(p)p^{-s})^n = \prod_{p \in \mathbb P}(1 - f(p)p^{-s})^{-1} \]

Now let’s put this to work. The first thing we can see is |\zeta(s) = \mathcal D[\bar 1](s) = \prod_{p\in\mathbb P}(1 - p^{-s})^{-1}|. But this lets us write |1/\zeta(s) = \prod_{p\in\mathbb P}(1 - p^{-s})|. If we look for a multiplicative function that would produce the right-hand side, we see that it must send a prime |p| to |-1| and |p^n| for |n > 1| to |0|. In other words, it’s the Möbius function |\mu| we defined before. So |\mathcal D[\mu](s) = 1/\zeta(s)|.

Using |\mathcal D[d](s) = \zeta(s)^2|, we see that \[\begin{flalign} \zeta(s)^2 & = \prod_{p\in\mathbb P}\left(\sum_{n=0}^\infty p^{-ns}\right)^{-2} \\ & = \prod_{p\in\mathbb P}\left(\sum_{n=0}^\infty (n+1)p^{-ns}\right)^{-1} \\ & = \prod_{p\in\mathbb P}\left(\sum_{n=0}^\infty d(p^n)p^{-ns}\right)^{-1} \\ & = \mathcal D[d](s) \end{flalign}\] Therefore, |d(p^n) = n + 1|. This intuitively makes sense because the only divisors of |p^n| are |p^k| for |k = 0, \dots, n|, and for |a| and |b| coprime |d(ab) = \vert D_{ab} \vert = \vert D_a \times D_b\vert = \vert D_a\vert\vert D_b\vert = d(a)d(b)|.

Another result leveraging the theorem is given any multiplicative function |f|, we can define a new multiplicative function via |f^{[k]}(p^n) = \begin{cases}f(p^m), & km = n\textrm{ for }m\in\mathbb N \\ 0, & k \nmid n\end{cases}|.

Lemma: The operation just defined has the property that |\mathcal D[f^{[k]}](s) = \mathcal D[f](ks)|.
Proof: \[\begin{flalign} \mathcal D[f^{[k]}](s) & = \prod_{p \in \mathbb P}\sum_{n=0}^\infty f^{[k]}(p^n)p^{-ns} \\ & = \prod_{p \in \mathbb P}\sum_{n=0}^\infty f^{[k]}(p^{kn})p^{-nks} \\ & = \prod_{p \in \mathbb P}\sum_{n=0}^\infty f(p^n)p^{-nks} \\ & = \mathcal D[f](ks) \end{flalign}\] |\square|

Möbius Inversion

We can write a sum over some function, |f|, of the divisors of a given natural |n| as |(f \star \bar 1)(n) = \sum_{d \mid n} f(d)|. Call this |g(n)|. But then we have |\mathcal D[f \star \bar 1] = \mathcal D[f]\mathcal D[\bar 1] = \mathcal D[f]\zeta| and thus |\mathcal D[f] = \mathcal D[f]\zeta/\zeta = \mathcal D[(f \star \bar 1) \star \mu]|. Therefore, if we only have the sums |g(n) = \sum_{d \mid n} f(d)| for some unknown |f|, we can recover |f| via |f(n) = (g \star \mu)(n) = \sum_{d\mid n}g(d)\mu(n/d)|. This is Möbius inversion.

Formally:

\[g(n) = \sum_{d\mid n} f(d) \iff f(n) = \sum_{d \mid n} \mu(d)g(n/d)\]

As a simple example, we clearly have |\zeta(s)/\zeta(s) = 1 = \mathcal D[\delta](s)| so |\bar 1 \star \mu = \delta| or |\sum_{d \mid n}\mu(d) = 0| for |n > 1| and |1| when |n = 1|.

We also get generalized Möbius inversion via |\delta(n) = \delta(n)n^k = (\mu\star\bar 1)(n)n^k = (({-})^k\mu\star({-})^k)(n)|. Which is to say if |g(n) = \sum_{d\mid n}d^k f(n/d)| then |f(n) = \sum_{d\mid n} \mu(d)d^kg(n/d)|.

By considering logarithms, we also get a multiplicative form of (generalized) Möbius inversion: \[g(n) = \prod_{d\mid n}f(n/d)^{d^k} \iff f(n) = \prod_{d\mid n}g(n/d)^{\mu(d)d^k}\]

Theorem: As another guise of Möbius inversion, given any completely multiplicative function |h|, let |g(m) = \sum_{n=1}^\infty f(mh(n))|. Assuming these sums make sense, we can recover |f(k)| via |f(k) = \sum_{m=1}^\infty \mu(m)g(kh(m))|.

Proof: \[\begin{align} \sum_{m=1}^\infty \mu(m)g(kh(m)) & = \sum_{m=1}^\infty \mu(m)\sum_{n=1}^\infty f(kh(m)h(n)) \\ & = \sum_{N=1}^\infty \sum_{N=mn} \mu(m)f(kh(N)) \\ & = \sum_{N=1}^\infty f(kh(N)) \sum_{N=nm} \mu(m) \\ & = \sum_{N=1}^\infty f(kh(N)) (\mu\star\bar 1)(N) \\ & = \sum_{N=1}^\infty f(kh(N)) \delta(N) \\ & = f(k) \end{align}\] |\square|

This will often show up in the form of |r(x^{1/n})| or |r(x^{1/n})/n|, i.e. with |h(n)=n^{-1}| and |f_x(k) = r(x^k)| or |f_x(k) = kr(x^k)|. Typically, we’ll then be computing |f_x(1) = r(x)|.

Lambert Series

As a brief aside, it’s worth mentioning Lambert Series.

Given an arithmetic function |a|, these are series of the form: \[ \sum_{n=1}^\infty a(n) \frac{x^n}{1-x^n} = \sum_{n=1}^\infty a(n) \sum_{k=1}^\infty x^{kn} = \sum_{n=1}^\infty (a \star \bar 1)(n) x^n \]

This leads to: \[\sum_{n=1}^\infty \mu(n) \frac{x^n}{1-x^n} = x\] and: \[\sum_{n=1}^\infty \varphi(n) \frac{x^n}{1-x^n} = \frac{x}{(1-x)^2}\]

Inclusion-Exclusion

The Möbius and |\zeta| functions can be generalized to incidence algebras where this form is from the incidence algebra induced by the divisibility order². A notable and relevant example of a Möbius functions for another, closely related, incidence algebra is when we consider the incidence algebra induced by finite multisets with the inclusion ordering. Let |T| be a finite multiset, we get |\mu(T) = \begin{cases}0,&T\text{ has repeated elements}\\(-1)^{\vert T\vert},&T\text{ is a set}\end{cases}|. Since we can view a natural number as a finite multiset of primes, and we can always relabel the elements of a finite multiset with distinct primes, this is equivalent to the Möbius function we’ve been using.

This leads to a nice and compact way of describing the principle of inclusion-exclusion. Let |A| and |S| be (finite) multisets with |S \subseteq A| and assume we have |f| and |g| defined on the set of sub-multisets of |A|. If \[g(A) = \sum_{S\subseteq A} f(S)\] then \[f(A) = \sum_{S\subseteq A}\mu(A\setminus S)g(S)\] and this is Möbius inversion for this notion of Möbius function. We can thus take a different perspective on Möbius inversion. If |P| is a finite multiset of primes, then \[g(n_P) = \sum_{Q\subseteq P}f(n_Q) \iff f(n_P) = \sum_{Q\subseteq P}\mu(P\setminus Q)g(n_Q)\] recalling that |Q\subseteq P \iff n_Q \mid n_P| and |n_{P\setminus Q} = n_P/n_Q| when |Q\subseteq P|.

We get traditional inclusion-exclusion by noting that |\mu(T)=(-1)^{\vert T\vert}| when |T| is a set, i.e. all elements have multiplicity at most |1|. Let |I| be a finite set and assume we have a family of finite sets, |\{T_i\}_{i\in I}|. Write |T = \bigcup_{i\in I}T_i| and define |\bigcap_{i\in\varnothing}T_i = T|.

Define \[f(J) = \left\vert\bigcap_{i\in I\setminus J}T_i\setminus\bigcup_{i \in J}T_i\right\vert\] for |J\subseteq I|. In particular, |f(I) = 0|. |f(J)| is then the number of elements shared by all |T_i| for |i\notin J| and no |T_j| for |j\in J|. Every |x \in \bigcup_{i\in I}T_i| is thus associated to exactly one such subset of |I|, namely |\{j\in I\mid x\notin T_j\}|. Formally, |x \in \bigcap_{i\in I\setminus J}T_i\setminus\bigcup_{i \in J}T_i \iff J = \{j\in I\mid x\notin T_j\}| so each |\bigcap_{i\in I\setminus J}T_i\setminus\bigcup_{i \in J}T_i| is disjoint and \[g(J) = \sum_{S\subseteq J}f(S) = \left\vert\bigcup_{S\subseteq J}\left(\bigcap_{i\in I\setminus S}T_i\setminus\bigcup_{i \in S}T_i\right)\right\vert = \left\vert\bigcap_{i\in I\setminus J}T_i\right\vert \] for |J \subseteq I|. In particular, |g(I) = \vert\bigcup_{i\in I}T_i\vert|.

By the Möbius inversion formula for finite sets, we thus have: \[f(J) = \sum_{S\subseteq J}(-1)^{\vert J\vert - \vert S\vert}g(S)\] which for |J = I| gives: \[ 0 = \sum_{J\subseteq I}(-1)^{\vert I\vert - \vert J\vert}\left\vert\bigcap_{i\in I\setminus J}T_i\right\vert = \left\vert\bigcup_{i\in I}T_i\right\vert + \sum_{J\subsetneq I}(-1)^{\vert I\vert - \vert J\vert}\left\vert\bigcap_{i\in I\setminus J}T_i\right\vert \] which is equivalent to the more usual form: \[\left\vert\bigcup_{i\in I}T_i\right\vert = \sum_{J\subsetneq I}(-1)^{\vert I\vert - \vert J\vert - 1}\left\vert\bigcap_{i\in I\setminus J}T_i\right\vert = \sum_{\varnothing\neq J\subseteq I}(-1)^{\vert J\vert + 1}\left\vert\bigcap_{i\in J}T_i\right\vert \]

|\varphi|

An obvious thing to explore is to apply Möbius inversion to various arithmetic functions. A fairly natural first start is applying Möbius inversion to the identity function. From the above results, we know that this unknown function |\varphi| will satisfy |\mathcal D[\varphi](s) = \zeta(s-1)/\zeta(s) = \mathcal D[\operatorname{id}\star\mu](s)|. We also immediately have the property that |n = \sum_{d \mid n}\varphi(d)|. Using Euler’s product formula we have: \[\begin{flalign} \zeta(s-1)/\zeta(s) & = \prod_{p \in \mathbb P} \frac{1 - p^{-s}}{1 - p^{-s+1}} \\ & = \prod_{p \in \mathbb P} \frac{1 - p^{-s}}{1 - pp^{-s}} \\ & = \prod_{p \in \mathbb P} (1 - p^{-s})\sum_{n=0}^\infty p^n p^{-ns} \\ & = \prod_{p \in \mathbb P} \left(\sum_{n=0}^\infty p^n p^{-ns}\right) - \left(\sum_{n=0}^\infty p^n p^{-s} p^{-ns}\right) \\ & = \prod_{p \in \mathbb P} \left(\sum_{n=0}^\infty p^n p^{-ns}\right) - \left(\sum_{n=0}^\infty p^n p^{-(n + 1)s}\right) \\ & = \prod_{p \in \mathbb P} \left(1 + \sum_{n=1}^\infty p^n p^{-ns}\right) - \left(\sum_{n=1}^\infty p^{n-1} p^{-ns}\right) \\ & = \prod_{p \in \mathbb P} \left(1 + \sum_{n=1}^\infty (p^n - p^{n-1}) p^{-ns}\right) \\ & = \prod_{p \in \mathbb P} \left(1 + \sum_{n=1}^\infty \varphi(p^n) p^{-ns}\right) \\ & = \mathcal D[\varphi](s) \end{flalign}\]

So |\varphi| is the multiplicative function defined by |\varphi(p^n) = p^n - p^{n-1}|. For |p^n|, we can see that this counts the number of positive integers less than or equal to |p^n| which are coprime to |p^n|. There are |p^n| positive integers less than or equal to |p^n|, and every |p|th one is a multiple of |p| so |p^n/p = p^{n-1}| are not coprime to |p^n|. All the remainder are coprime to |p^n| since they don’t have |p| in their prime factorizations and |p^n| only has |p| in its. We need to verify that this interpretation is multiplicative. To be clear, we know that |\varphi| is multiplicative and that this interpretation works for |p^n|. The question is whether |\varphi(n)| for general |n| meets the above description, i.e. whether the number of coprime numbers less than |n| is multiplicative.

Theorem: The number of coprime numbers less than |n| is multiplicative and is equal to |\varphi(n)|.

Proof: |\varphi = \mu\star\operatorname{id}|. We have:

\[\begin{flalign} \varphi(n_P) & = \sum_{d\mid n_P}\mu(d)\frac{n_P}{d} \\ & = \sum_{Q\subseteq P}\mu(Q)\frac{n_P}{n_Q} \\ & = \sum_{Q\subseteq \mathrm{dom}(P)}(-1)^{\vert Q\vert}\frac{n_P}{n_Q} \end{flalign}\]

We can see an inclusion-exclusion pattern. Specifically, let |C_k = \{ c \in [k] \mid \gcd(c, k) = 1\}| be the numbers less than or equal to |k| and coprime to |k|. Let |S_{k,m} = \{ c \in [k] \mid m \mid c\}|. We have |S_{k,a} \cap S_{k,b} = S_{k,\operatorname{lcm}(a,b)}|. Also, when |c \mid k|, then |\vert S_{k,c}\vert = k/c|. |C_{n_P} = [n_P] \setminus \bigcup_{p \in \mathrm{dom}(P)} S_{n_P,p}| because every number not coprime to |n_P| shares some prime factor with it. Applying inclusion-exclusion to the union yields \[\begin{align} \vert C_{n_P}\vert & = n_P - \sum_{\varnothing\neq Q\subseteq\mathrm{dom}(P)}(-1)^{\vert Q\vert+1}\left\vert \bigcap_{p\in Q}S_{n_P,p}\right\vert \\ & = n_P + \sum_{\varnothing\neq Q\subseteq\mathrm{dom}(P)}(-1)^{\vert Q\vert}\frac{n_P}{\prod_{p\in Q}p} \\ & = \sum_{Q\subseteq\mathrm{dom}(P)}(-1)^{\vert Q\vert}\frac{n_P}{n_Q} \end{align}\] |\square|

Many of you will already have recognized that this is Euler’s totient function.

Combinatorial Species

The book Combinatorial Species and Tree-Like Structures has many examples where Dirichlet convolutions and Möbius inversion come up. A combinatorial species is a functor |\operatorname{Core}(\mathbf{FinSet})\to\mathbf{FinSet}|. Any permutation on a finite set can be decomposed into a collection of cyclic permutations. Let |U| be a finite set of cardinality |n| and |\pi : U \cong U| a permutation of |U|. For any |u\in U|, there is a smallest |k\in\mathbb N_+| such that |\pi^k(u) = u| where |\pi^{k+1} = \pi \circ \pi^k| and |\pi^0 = \operatorname{id}|. The |k| elements |\mathcal O(u)=\{\pi^{i-1}(u)\mid i\in[k]\}| make up a cycle of length |k|, and |\pi| restricted to |U\setminus O(u)| is a permutation on this smaller set. We can just inductively pull out another cycle until we run out of elements. Write |\pi_k| for the number of cycles of length |k| in the permutation |\pi|. We clearly have |n = \sum_{k=1}^\infty k\pi_k| as every cycle has |k| elements in it.

Write |\operatorname{fix}\pi| for the number of fixed points of |\pi|, i.e. the cardinality of the set |\{u\in U\mid \pi(u) = u\}|. Clearly, every element that is fixed by |\pi^k| needs to be in a cycle whose length divides |k|. This leads to the equation:

\[ \operatorname{fix}\pi^k = \sum_{d\mid k} d\pi_d = ((d \mapsto d\pi_d) \star \bar 1)(k)\]

Since |F(\pi^k) = F(\pi)^k| for a combinatorial species |F|, Möbius inversion, as explicitly stated in Proposition 2.2.3 of Combinatorial Species and Tree-Like Structures, leads to:

\[k(F(\pi))_k = \sum_{d\mid k}\mu\left(\frac{k}{d}\right)\operatorname{fix}F(\pi^d) = (\mu\star(d\mapsto \operatorname{fix}F(\pi^d)))(k) \]

If we Dirichlet convolve both sides of this with |\operatorname{id}|, replacing |F(\pi)| with |\beta| as it doesn’t matter that this permutation comes from an action of a species, we get:

\[\sum_{d\mid m} d\beta_d(m/d) = m\sum_{d\mid m} \beta_d = (\varphi\star(d\mapsto \operatorname{fix}\beta^d))(m)\]

This is just using |\varphi = \operatorname{id}\star\mu|. If we choose |m| such that |\beta^m = \operatorname{id}|, then we get |\sum_{d\mid m} \beta_d = \sum_{k=1}^\infty \beta_k| because |\beta_k| will be |0| for all the |k| which don’t divide |m|. This makes the previous equation into equation 2.2 (34) in the book.

Since we know |n = \sum_{k=1}^\infty k\pi_k| for any permutation |\pi|, we also get: \[\vert F([n])\vert = \sum_{k=1}^\infty\sum_{d\mid k}\mu\left(\frac{k}{d}\right)\operatorname{fix}F(\pi^d) = \sum_{k=1}^\infty(\mu\star(d\mapsto\operatorname{fix}F(\pi^d)))(k)\]

These equations give us a way to compute some of these divisor sums by looking at the number fixed points and cycles of the action of species and vice versa. For example, 2.3 (49) is a series of Dirichlet convolutions connected to weighted species.

Example 12 from this book presents a nice and perhaps surprising identity. The core of it can be written as: \[\sum_{k=1}^\infty\ln(1-ax^k) = \sum_{k=1}^\infty\rho_k(a)\ln(1-x^k)\] where |\rho_k(a) = k^{-1}\sum_{d\mid k}\varphi(k/d)a^d|. We can rewrite this definition as the characterization |k\rho_k(a) = (\varphi\star a^{({-})})(k)|. Recalling that |\varphi = \mu \star \operatorname{id}| and |\ln(1-x) = -\sum_{n=1}^\infty x^n/n|, we get the following derivation:

Theorem: \[\sum_{k=1}^\infty\ln(1-ax^k) = \sum_{k=1}^\infty\rho_k(a)\ln(1-x^k)\] where |\rho_k(a) = k^{-1}\sum_{d\mid k}\varphi(k/d)a^d|.

Proof: \[\begin{flalign} \sum_{k=1}^\infty\ln(1-ax^k) & = -\sum_{k=1}^\infty\sum_{n=1}^\infty \frac{a^n x^{nk}}{n} \\ & = -\sum_{n=1}^\infty\sum_{k=1}^\infty \frac{a^n x^{nk}}{n} \\ & = -\sum_{N=1}^\infty\sum_{k\mid N} \frac{a^{N/k} x^N}{N/k} \tag{N=nk} \\ & = -\sum_{N=1}^\infty\frac{x^N}{N}\sum_{k\mid N} ka^{N/k} \\ & = -\sum_{N=1}^\infty\frac{x^N}{N}(\operatorname{id}\star a^{({-})})(N) \\ & = -\sum_{N=1}^\infty\frac{x^N}{N}(\delta\star\operatorname{id}\star a^{({-})})(N) \tag{the trick} \\ & = -\sum_{N=1}^\infty\frac{x^N}{N}(\bar 1\star\mu\star\operatorname{id}\star a^{({-})})(N) \\ & = -\sum_{N=1}^\infty\frac{x^N}{N}(\bar 1\star\varphi\star a^{({-})})(N) \\ & = -\sum_{N=1}^\infty\frac{x^N}{N}\sum_{k\mid N}(\varphi\star a^{({-})})(k) \\ & = -\sum_{N=1}^\infty\frac{x^N}{N}\sum_{k\mid N}k\rho_k(a) \\ & = -\sum_{n=1}^\infty\frac{x^{nk}}{n}\sum_{k=1}^\infty\rho_k(a) \tag{N=nk again} \\ & = \sum_{k=1}^\infty\rho_k(a) \ln(1-x^k) \end{flalign}\] |\square|

Derivative of Dirichlet series

We can easily compute the derivative of a Dirichlet series (assuming sufficiently strong convergence so we can push the differentiation into the sum):

\[\begin{flalign} \mathcal D[f]’(s) & = \frac{d}{ds}\sum_{n=1}^\infty f(n)n^{-s} \\ & = \sum_{n=1}^\infty f(n)\frac{d}{ds}n^{-s} \\ & = \sum_{n=1}^\infty f(n)\frac{d}{ds}e^{-s\ln n} \\ & = \sum_{n=1}^\infty -f(n)\ln n e^{-s\ln n} \\ & = -\sum_{n=1}^\infty f(n)\ln n n^{-s} \\ & = -\mathcal D[f\ln](s) \end{flalign}\]

This leads to the identity |\frac{d}{ds}\ln\mathcal D[f](s) = \mathcal D[f]’ (s)/\mathcal D[f](s) = -\mathcal D[f\ln \star \mu](s)|. For example, we have |-\zeta’(s)/\zeta(s) = \mathcal D[\ln \star \mu](s)|. Using the Euler product formula, we have |\ln\zeta(s) = -\sum_{p\in\mathbb P}\ln(1-p^{-s})|. Differentiating this gives \[\begin{flalign} \frac{d}{ds}\ln\zeta(s) & = -\sum_{p\in\mathbb P} p^{-s}\ln p/(1 - p^{-s}) \\ & = -\sum_{p\in\mathbb P} \sum_{k=1}^\infty \ln p (p^k)^{-s} \\ & = -\sum_{n=1}^\infty \Lambda(n) n^{-s} \\ & = -\mathcal D[\Lambda](s) \end{flalign}\] where |\Lambda(n) = \begin{cases}\ln p,&p\in\mathbb P\land\exists k\in\mathbb N_+.n=p^k \\ 0, & \text{otherwise}\end{cases}|. |\Lambda|, which is not a multiplicative nor an additive function, is known as the von Mangoldt function. Just to write it explicitly, the above implies |\Lambda = \ln \star \mu|, i.e. |\Lambda| is the Möbius inversion of |\ln|. This can be generalized for arbitrary completely multiplicative functions besides |\bar 1| to get |\mathcal D[f]’/\mathcal D[f] = \mathcal D[f\Lambda]|.

We now have multiple perspectives on |\Lambda| which is a kind of “indicator function” for prime powers.

Dirichlet Inverse

Let’s say we’re given an arithmetic function |f|, and we want to find an arithmetic function |g| such that |f \star g = \delta| which we’ll call the Dirichlet inverse of |f|. We immediately get |(f \star g)(1) = f(1)g(1) = 1 = \delta(1)|. So, supposing |f(1)\neq 1|, we can define |g(1) = 1/f(1)|. We then get a recurrence relation for all the remaining values of |g| via: \[0 = (f \star g)(n) = f(1)g(n) + \sum_{d \mid n, d\neq 1} f(d)g(n/d)\] for |n > 1|. Solving for |g(n)|, we have: \[g(n) = -f(1)^{-1}\sum_{d\mid n,d\neq 1}f(d)g(n/d)\] where the right-hand side only requires |g(k)| for |k < n|. If |f| is multiplicative, then |f(1) = 1| and the inverse of |f| exists.

If |f| is completely multiplicative, its Dirichlet inverse is |\mu f|. This follows easily from |f \star \mu f = (\bar 1 \star \mu)f = \delta f = \delta|. As an example, |({-})^z| is completely multiplicative so its inverse is |({-})^z\mu|. Since the inverse of a Dirichlet convolution is the convolution of the inverses, we get |\varphi^{-1}(n) = \sum_{d\mid n}d\mu(d)|. Not to be confused with |\varphi(n) = (\operatorname{id}\star\mu)(n) = \sum_{d\mid n} d\mu(n/d)|.

Less trivially, the inverse of a multiplicative function is also a multiplicative function. We can prove it by complete induction on |\mathbb N_+| using the formula for |g| from above.

Theorem: If |f\star g = \delta|, then |g| is multiplicative when |f| is.

Proof: Let |n = ab| where |a| and |b| are coprime. If |a| (or, symmetrically, |b|) is equal to |1|, then since |g(1) = 1/f(1) = 1|, we have |g(1n) = g(1)g(n) = g(n)|. Now assume neither |a| nor |b| are |1| and, as the induction hypothesis, assume that |g| is multiplicative on all numbers less than |n|. We have: \[\begin{flalign} g(ab) & = -\sum_{d\mid ab,d\neq 1}f(d)g(ab/d) \\ & = -\sum_{d_a \mid a}\sum_{d_b \mid b,d_a d_b \neq 1}f(d_ad_b)g(ab/(d_ad_b)) \\ & = -\sum_{d_a \mid a}\sum_{d_b \mid b,d_a d_b \neq 1}f(d_a)f(d_b)g(a/d_a)g(b/d_b)) \\ & = -\sum_{d_b \mid b,d_b \neq 1}f(d_b)g(a)g(b/d_b)) - \sum_{d_a \mid a,d_a \neq 1}\sum_{d_b \mid b}f(d_a)f(d_b)g(a/d_a)g(b/d_b)) \\ & = -g(a)\sum_{d \mid b,d \neq 1}f(d)g(b/d)) - \sum_{d_a \mid a,d_a \neq 1}f(d_a)g(a/d_a)\sum_{d_b \mid b}f(d_b)g(b/d_b)) \\ & = g(a)g(b) - \sum_{d_a \mid a,d_a \neq 1}f(d_a)g(a/d_a) (f \star g)(b) \\ & = g(a)g(b) - \delta(b)\sum_{d_a \mid a,d_a \neq 1}f(d_a)g(a/d_a) \\ & = g(a)g(b) \end{flalign}\] |\square|

Assuming |f| has a Dirichlet inverse, we also have: \[\mathcal D[f^{-1}](s) = \mathcal D[f](s)^{-1}\] immediately from the convolution theorem.

More Examples

Given a multiplicative function |f|:

\[\begin{align} \mathcal D[f(\gcd({-},n_P))](s) & = \zeta(s)\prod_{(p,k)\in P}(1 - p^{-s})\left(\sum_{n=0}^\infty f(p^{\min(k,n)})p^{-ns}\right) \\ & = \zeta(s)\prod_{(p,k)\in P}(1 - p^{-s})\left(\frac{f(p^k)p^{-(k+1)s}}{1 - p^{-s}} + \sum_{n=0}^k f(p^n)p^{-ns}\right) \end{align}\]

As an example, |\eta(s) = (1 - 2^{1-s})\zeta(s) = \mathcal D[f](s)| where |f(n) = \begin{cases}-1,&n=2\\1,&n\neq 2\end{cases}|.

Alternatively, |f(n) = \mu(\gcd(n, 2))| and we can apply the above formula to see: \[\begin{flalign} \mathcal D[\mu(\gcd({-},2))] & = \zeta(s)(1-2^{-s})\left(\frac{\mu(2)2^{-2s}}{1 - 2^{-s}} + \sum_{n=0}^1 \mu(2^n)2^{-ns}\right) \\ & = \zeta(s)(1-2^{-s})\left(\frac{-2^{-2s}}{1 - 2^{-s}} + 1 - 2^{-s}\right) \\ & = \zeta(s)(-2^{-2s} + (1 - 2^{-s})^2) \\ & = \zeta(s)(1 - 2^{1-s}) \end{flalign}\]

|\lambda| and |\gamma|

Recalling, |\lambda| is completely multiplicative and is characterized by |\lambda(p) = -1|.

We can show that |\mathcal D[\lambda](s) = \zeta(2s)/\zeta(s)| which is equivalent to saying |\bar 1^{(2)} \star \mu = \lambda| or |\lambda\star\bar 1 = \bar 1^{(2)}|.

\[\begin{flalign} \zeta(2s)/\zeta(s) & = \prod_{p\in\mathbb P} \frac{1-p^{-s}}{1-(p^{-s})^2} \\ & = \prod_{p\in\mathbb P} \frac{1-p^{-s}}{(1-p^{-s})(1+p^{-s})} \\ & = \prod_{p\in\mathbb P} (1 + p^{-s})^{-1} \\ & = \prod_{p\in\mathbb P} (1 - \lambda(p)p^{-s})^{-1} \\ & = \mathcal D[\lambda](s) \end{flalign}\]

We have |\lambda\mu = \vert\mu\vert = \mu\mu| is the inverse of |\lambda| so |\mathcal D[\vert\mu\vert](s) = \zeta(s)/\zeta(2s)|.

Recalling, |\gamma| is multiplicative and is characterized by |\gamma(p^n) = -1|.

\[\begin{flalign} \mathcal D[\gamma](s) & = \prod_{p \in \mathbb P}\left(1 + \sum_{n=1}^\infty \gamma(p^n)p^{-ns}\right) \\ & = \prod_{p \in \mathbb P}\left(1 - \sum_{n=1}^\infty p^{-ns}\right) \\ & = \prod_{p \in \mathbb P}\left(1 - \left(\sum_{n=0}^\infty p^{-ns} - 1\right)\right) \\ & = \prod_{p \in \mathbb P}\frac{2(1 - p^{-s}) - 1}{1 - p^{-s}} \\ & = \prod_{p \in \mathbb P}\frac{1 - 2p^{-s}}{1 - p^{-s}} \end{flalign}\]

This implies that |(\gamma\star\mu)(p^n) = \begin{cases}-2, & n=1 \\ 0, & n > 1 \end{cases}|.

Indicator Functions

Let |1_{\mathbb P}| be the indicator function for the primes. We have |\omega = 1_{\mathbb P}\star\bar 1| or |1_{\mathbb P} = \omega\star\mu|. Directly, |\mathcal D[1_{\mathbb P}](s) = \sum_{p\in\mathbb P}p^{-s}| so we have |\mathcal D[\omega](s)/\zeta(s) = \sum_{p\in\mathbb P} p^{-s}|.

Lemma: |\mathcal D[1_{\mathbb P}](s)=\sum_{n=1}^\infty \frac{\mu(n)}{n}\ln\zeta(ns)|
Proof: We proceed as follows: \[\begin{align} \sum_{n=1}^\infty \frac{\mu(n)}{n}\ln\zeta(ns) & = \sum_{n=1}^\infty \frac{\mu(n)}{n}\ln\left(\prod_{p\in\mathbb P}(1 - p^{-ns})^{-1}\right) \\ & = -\sum_{n=1}^\infty \frac{\mu(n)}{n}\sum_{p\in\mathbb P}\ln(1 - p^{-ns}) \\ & = \sum_{p\in\mathbb P}\sum_{n=1}^\infty \frac{\mu(n)}{n}\sum_{k=1}^\infty p^{-kns}/k \\ & = \sum_{p\in\mathbb P}\sum_{N=1}^\infty \sum_{N=kn} \frac{\mu(n)}{N}p^{-Ns} \\ & = \sum_{p\in\mathbb P}\sum_{N=1}^\infty \frac{p^{-Ns}}{N}\sum_{N=kn}\mu(n) \\ & = \sum_{p\in\mathbb P}\sum_{N=1}^\infty \frac{p^{-Ns}}{N}(\mu\star\bar 1)(N) \\ & = \sum_{p\in\mathbb P}\sum_{N=1}^\infty \frac{p^{-Ns}}{N}\delta(N) \\ & = \sum_{p\in\mathbb P} p^{-s} \\ & = \mathcal D[1_{\mathbb P}](s) \end{align}\] |\square|

Let |1_{\mathcal P}| be the indicator function for prime powers. |\Omega = 1_{\mathcal P}\star\bar 1| or |1_{\mathcal P} = \Omega\star\mu|. |\mathcal D[1_{\mathcal P}](s) = \sum_{p\in\mathbb P}(1 - p^{-s})^{-1}| so we have |\mathcal D[\Omega](s)/\zeta(s) = \sum_{p\in\mathbb P}(1 - p^{-s})^{-1}|.

Lemma: |\mathcal D[1_{\mathcal P}](s)=\sum_{n=1}^\infty \frac{\varphi(n)}{n}\ln\zeta(ns)|
Proof: This is quite similar to the previous proof. \[\begin{align} \sum_{n=1}^\infty \frac{\varphi(n)}{n}\ln\zeta(ns) & = \sum_{p\in\mathbb P}\sum_{N=1}^\infty \frac{p^{-Ns}}{N}\sum_{N=kn}\varphi(n) \\ & = \sum_{p\in\mathbb P}\sum_{N=1}^\infty \frac{p^{-Ns}}{N}(\varphi\star\bar 1)(N) \\ & = \sum_{p\in\mathbb P}\sum_{N=1}^\infty \frac{p^{-Ns}}{N} N \\ & = \sum_{p\in\mathbb P}\sum_{N=1}^\infty p^{-Ns} \\ & = \mathcal D[1_{\mathcal P}](s) \end{align}\] |\square|

Summatory Functions

One thing we’ve occasionally been taking for granted is that the operator |\mathcal D| is injective. That is, |\mathcal D[f] = \mathcal D[g]| if and only if |f = g|. To show this, we’ll use the fact that we can (usually) invert the Mellin transform which can be viewed roughly as a version of |\mathcal D| that operates on continuous functions.

Before talking about the Mellin transform, we’ll talk about summatory functions as this will ease our later discussion.

We will turn a sum into a continuous function via a zero-order hold, i.e. we will take the floor of the input. Thus |\sum_{n\leq x} f(n)| is constant on any interval of the form |[k,k+1)|. It then (potentially) has jump discontinuities at integer values. The beginning of the sum is at |n=1| so for all |x<1|, the sum up to |x| is |0|. We will need a slight tweak to better deal with these discontinuities. This will be indicated by a prime on the summation sign.

For non-integer values of |x|, we have: \[\sum_{n \leq x}’ f(n) = \sum_{n \leq x} f(n)\]

For |m| an integer, we have: \[ \sum_{n \leq m}’ f(n) = \frac{1}{2}\left(\sum_{n<m} f(n) + \sum_{n \leq m} f(n)\right) = \sum_{n\leq m} f(n) - f(m)/2 \]

This kind of thing should be familiar to those who’ve worked with things like Laplace transforms of discontinuous functions. (Not for no reason…)

One reason for introducing these summation functions is they are a little easier to work with. Arguably, we want something like |\frac{d}{dx}\sum_{n\leq x}f(n) = \sum_{n=1}^\infty f(n)\delta(n-x)|, but that means we end up with a bunch of distribution nonsense and even more improper integrals. The summation function may be discontinuous, but it at least has a finite value everywhere. Of course, another reason for introducing these functions is that they often are values we’re interested in.

Several important functions are these continuous “sums” of arithmetic functions of this form:

• Mertens function: |M(x) = \sum_{n\leq x}’ \mu(n)|
• Chebyshev function: |\vartheta(x) = \sum_{p\leq x, p\in\mathbb P}’ \ln p = \sum_{n\leq x} 1_{\mathbb P}(n)\ln n|
• Second Chebyshev function: |\psi(x) = \sum_{n\leq x}’ \Lambda(n) = \sum_{n=1}^\infty \vartheta(x^{1/n})|
• The prime-counting function: |\pi(x) = \sum_{n\leq x}’ 1_{\mathbb P}|
• Riemann’s prime-power counting function: |\Pi_0(x) = \sum_{n\leq x} \frac{\Lambda(n)}{\ln n} = \sum_{n=1}^\infty \sum_{p^n\leq x,p\in\mathbb P}’ n^{-1} = \sum_{n=1}^\infty\pi(x^{1/n})n^{-1}|
• |D(x) = \sum_{n\leq x}d(n)|

These are interesting in how they related to the prime-counting function.

Let’s consider the arithmetic function |\Lambda/\ln| whose Dirichlet series is |\ln\zeta|.

We have the summation function |\sum_{n\leq x}’ \Lambda(n)/\ln(n)|, but |\Lambda(n)| is |0| except when |n=p^k| for some |p\in\mathbb P| and |k\in\mathbb N_+|. Therefore, we have \[\begin{align} \sum_{n\leq x}’ \frac{\Lambda(n)}{\ln(n)} & = \sum_{k=1}^\infty\sum_{p^k\leq x, p\in\mathbb P}’ \frac{\Lambda(p^k)}{\ln(p^k)} \\ & = \sum_{k=1}^\infty\sum_{p^k\leq x, p\in\mathbb P}’ \frac{\ln(p)}{k\ln(p)} \\ & = \sum_{k=1}^\infty\sum_{p^k\leq x, p\in\mathbb P}’ \frac{1}{k} \\ & = \sum_{k=1}^\infty \frac{1}{k} \sum_{p^k\leq x, p\in\mathbb P}’ 1 \\ & = \sum_{k=1}^\infty \frac{1}{k} \sum_{p\leq x^{1/k}, p\in\mathbb P}’ 1 \\ & = \sum_{k=1}^\infty \frac{\pi(x^{1/k})}{k} \\ \end{align}\]

|\ln\zeta(s) = s\mathcal M[\Pi_0](-s)=\mathcal D[\Lambda/\ln](s)| where |\mathcal M| is the Mellin transform, and the connection to Dirichlet series is described in the following section.

Mellin Transform

The definition of the Mellin transform and its inverse are:

\[\mathcal M[f](s) = \int_0^\infty x^s\frac{f(x)}{x}dx\] \[\mathcal M^{-1}[\varphi](x) = \frac{1}{2\pi i}\int_{c-i\infty}^{c+i\infty} x^{-s}\varphi(s)ds\]

The contour integral is intended to mean the vertical line with real part |c| traversed from negative to positive imaginary values. Modulo the opposite sign of |s| and the extra factor of |x|, this is quite similar to a continuous version of a Dirichlet series.

The Mellin transform is closely related to the two-sided Laplace transform.

\[\mathcal D[f](s) = s\mathcal M\left[x\mapsto \sum_{n\leq x}’ f(n)\right](-s)\]

Using Mellin transform properties, particularly the one for transforming the derivative, we can write the following.

\[\begin{align} \mathcal D[f](s) = s\mathcal M\left[x\mapsto \sum_{n\leq x}’ f(n)\right](-s) & \iff \mathcal D[f](1-s) = -(s-1)\mathcal M\left[x\mapsto \sum_{n\leq x}’ f(n)\right](s-1) \\ & \iff \mathcal D[f](1-s) = \mathcal M\left[x\mapsto \frac{d}{dx}\sum_{n\leq x}’ f(n)\right](s) \\ & \iff \mathcal D[f](1-s) = \int_0^\infty x^{s-1}\frac{d}{dx}\sum_{n\leq x}’ f(n)dx \\ & \iff \mathcal D[f](1-s) = \int_0^\infty x^{s-1}\sum_{n=1}^\infty f(n)\delta(x-n)dx \\ & \iff \mathcal D[f](1-s) = \sum_{n=1}^\infty f(n)n^{s-1} \\ & \iff \mathcal D[f](s) = \sum_{n=1}^\infty f(n)n^{-s} \end{align}\]

This leads to Perron’s formula

\[\begin{align} \sum_{n\leq x}’ f(n) & = \mathcal M^{-1}[s\mapsto -\mathcal D[f](-s)/s](x) \\ & = \frac{1}{2\pi i}\int_{-c-i\infty}^{-c+i\infty}\frac{\mathcal D[f](-s)}{-s} x^{-s} ds \\ & = -\frac{1}{2\pi i}\int_{c+i\infty}^{c-i\infty}\frac{\mathcal D[f](s)}{s} x^s ds \\ & = \frac{1}{2\pi i}\int_{c-i\infty}^{c+i\infty}\frac{\mathcal D[f](s)}{s} x^s ds \end{align}\]

for which we need to take the Cauchy principal value to get something defined. (See also Abel summation.)

There are side conditions on the convergence of |\mathcal D[f]| for these formulas to be justified. See the links.

Many of the operations we’ve described on Dirichlet series follow from Mellin transform properties. For example, we have |\mathcal M[f]’(s) = \mathcal M[f\ln](s)| generally.

Summary

Properties

Dirichlet Convolution

Dirichlet convolution is |(f\star g)(n) = \sum_{d\mid n} f(d)g(n/d) = \sum_{mk=n} f(m)g(k)|.

Dirichlet convolution forms a commutative ring with it as the multiplication, |\delta| as the multiplicative unit and the usual additive structure. This is to say that Dirichlet convolution is commutative, associative, unital, and bilinear.

For |f| completely multiplicative, |f(g\star h) = fg \star fh|.

Dirichlet Inverse

For any |f| such that |f(1)\neq 0|, there is a |g| such that |f\star g = \delta|. In particular, the set of multiplicative functions forms a subgroup of this multiplicative group, i.e. the Dirichlet convolution of multiplicative functions is multiplicative.

If |f(1) \neq 0|, then |f \star g = \delta| where |g| is defined by the following recurrence:

\[\begin{flalign} g(1) & = 1/f(1) \\ g(n) & = -f(1)^{-1}\sum_{d\mid n,d\neq 1}f(d)g(n/d) \end{flalign}\]

For a completely multiplicative |f|, its Dirichlet inverse is |\mu f|.

Convolution Theorem

\[\mathcal D[f](s)\mathcal D[g](s) = \mathcal D[f\star g](s)\]

Möbius Inversion

\[\delta = \bar 1 \star \mu\]

This means from a divisor sum |g(n)\sum_{d\mid n}f(d) = (f\star\bar 1)(n)| for each |n|, we can recover |f| via |g\star\mu = f\star\bar 1\star\mu = f|. Which is to say |f(n)=\sum_{d\mid n}g(d)\mu(n/d)|.

This can be generalized via |({-})^k\mu\star({-})^k = \delta|. In sums, this means when |g(n)=\sum_{d\mid n}d^k f(n/d)|, then |f(n)=\sum_{d\mid n}\mu(d)d^k g(n/d)|.

Let |h| be a completely multiplicative function. Given |g(m) = \sum_{n=1}^\infty f(mh(n))|, then |f(n) = \sum_{m=1}^\infty \mu(m)g(nh(m))|.

Using the Möbius function for finite multisets and their inclusion ordering, we can recast Möbius inversion of naturals as Möbius inversion of finite multisets (of primes) a la: \[n_P = \sum_{Q\subseteq P}\mu(P\setminus Q)n_Q = \sum_{Q\subseteq P}\mu(n_P/n_Q)n_Q = \sum_{d\mid n_P}\mu(n_P/d)d \]

As a nice result, we have: \[\sum_{n=1}^\infty\ln(1-ax^n) = \sum_{n=1}^\infty\rho_n(a)\ln(1-x^n)\] where |n\rho_n(a) = (\varphi \star a^{({-})})(n)|.

Dirichlet Series

\[\mathcal D[f](s) = \sum_{n=1}^\infty f(n)n^{-s}\]

\[\mathcal D[n\mapsto f(n)n^k](s) = \mathcal D[f](s - k)\]

\[\mathcal D[f^{-1}](s) = \mathcal D[f](s)^{-1}\] where the inverse on the left is the Dirichlet inverse.

\[\mathcal D[f]’(s) = -\mathcal D[f\ln](s)\]

For a completely multiplicative |f|, \[\mathcal D[f]’(s)/\mathcal D[f](s) = -\mathcal D[f\Lambda](s)\] and: \[\ln\mathcal D[f](s) = \mathcal D[f\Lambda/\ln](s)\]

Dirichlet series as a Mellin transform:

\[\mathcal D[f](s) = s\mathcal M\left[x\mapsto \sum_{n\leq x}’ f(n)\right](-s)\]

The corresponding inverse Mellin transform statement is called Perron’s Formula:

\[\sum_{n\leq x}’ f(n) = \frac{1}{2\pi i}\int_{c-i\infty}^{c+i\infty}\frac{\mathcal D[f](s)}{s} x^s ds\]

Euler Product Formula

Assuming |f| is multiplicative, we have:

\[\mathcal D[f](s) = \prod_{p \in \mathbb P}\sum_{n=0}^\infty f(p^n)p^{-ns} = \prod_{p \in \mathbb P}\left(1 + \sum_{n=1}^\infty f(p^n)p^{-ns}\right) \]

When |f| is completely multiplicative, this can be simplified to:

\[\mathcal D[f](s) = \prod_{p \in \mathbb P}(1 - f(p)p^{-s})^{-1} \]

Lambert Series

Given an arithmetic function |a|, these are series of the form: \[ \sum_{n=1}^\infty a(n) \frac{x^n}{1-x^n} = \sum_{n=1}^\infty (a \star \bar 1)(n) x^n \]

\[\sum_{n=1}^\infty \mu(n) \frac{x^n}{1-x^n} = x\]

\[\sum_{n=1}^\infty \varphi(n) \frac{x^n}{1-x^n} = \frac{x}{(1-x)^2}\]

Arithmetic function definitions

|f(p^n)=\cdots| implies a multiplicative/additive function, while |f(p)=\cdots| implies a completely multiplicative/additive function.

|p^z| for |z\in\mathbb C| is completely multiplicative. This includes the identity function (|z=1|) and |\bar 1| (|z=0|). For any multiplicative |f|, |f\circ \gcd({-},k)| is multiplicative.

|\ln| is completely additive.

Important but neither additive nor multiplicative are the indicator functions for primes |1_{\mathbb P}| and prime powers |1_{\mathcal P}|.

The following functions are (completely) multiplicative unless otherwise specified.

\[\begin{flalign} \delta(p) & = 0 \tag{Kronecker delta} \\ \bar 1(p) & = 1 = p^0 \\ \mu(p^n) & = \begin{cases}-1, & n = 1 \\ 0, & n > 1\end{cases} \tag{Möbius function} \\ \Omega(p) & = 1 \tag{additive} \\ \lambda(p) & = -1 = (-1)^{\Omega(p)} \tag{Liouville function} \\ \omega(p^n) & = 1 \tag{additive} \\ \gamma(p^n) & = -1 = (-1)^{\omega(p^n)} \\ a(p^n) & = p(n) \tag{p(n) is the partition function} \\ \varphi(p^n) & = p^n - p^{n-1} = p^n(1 - 1/p) = J_1(p^n) \tag{Euler totient function} \\ \sigma_k(p^n) & = \sum_{m=0}^n p^{km} = \sum_{d\mid p^n} d^k = \frac{p^{k(n+1)}-1}{p^k - 1} \tag{last only works for k>0} \\ d(p^n) & = n + 1 = \sigma_0 \\ f^{[k]}(p^n) & = \begin{cases}f(p^m),& km=n\\0,& k\nmid n\end{cases} \tag{f multiplicative} \\ \Lambda(n) & = \begin{cases}\ln p,&p\in\mathbb P\land\exists k\in\mathbb N_+.n=p^k \\ 0, & \text{otherwise}\end{cases} \tag{not multiplicative} \\ J_k(p^n) & = p^{kn} - p^{k(n-1)} = p^{kn}(1 - p^{-k}) \tag{Jordan totient function} \\ \psi_k(p^n) & = p^{kn} + p^{k(n-1)} = p^{kn}(1 + p^{-k}) = J_{2k}(p^n)/J_k(p^n) \tag{Dedekind psi function} \\ \end{flalign}\]

Dirichlet convolutions

\[\begin{flalign} \delta & = \bar 1 \star \mu \\ \varphi & = \operatorname{id}\star\mu \\ \sigma_z & = ({-})^z \star \bar 1 = \psi_z \star \bar 1^{(2)} \\ \sigma_1 & = \varphi \star d \\ d & = \sigma_0 = \bar 1 \star \bar 1 \\ f \star f & = fd \tag{f completely multiplicative} \\ f\Lambda & = f\ln \star f\mu = f\ln \star f^{-1} \tag{f completely multiplicative, Dirichlet inverse} \\ \lambda & = \bar 1^{(2)} \star \mu \\ \vert\mu\vert & = \lambda^{-1} = \mu\lambda \tag{Dirichlet inverse} \\ 2^\omega & = \vert\mu\vert \star \bar 1 \\ \psi_z & = ({-})^z \star \vert\mu\vert \\ \operatorname{fix} \pi^{(-)} & = \bar 1 \star (k \mapsto k\pi_k) \tag{for a permutation} \\ ({-})^k & = J_k \star \bar 1 \end{flalign}\]

More Dirichlet convolution identities are here, though many are trivial consequences of the earlier properties.

Dirichlet series

\[\begin{array}{l|ll} f(n) & \mathcal D[f](s) & \\ \hline \delta(n) & 1 & \\ \bar 1(n) & \zeta(s) & \\ n & \zeta(s-1) & \\ n^z & \zeta(s-z) & \\ \sigma_z(n) & \zeta(s-z)\zeta(s) & \\ \mu(n) & \zeta(s)^{-1} & \\ \vert\mu(n)\vert & \zeta(s)/\zeta(2s) & \\ \varphi(n) & \zeta(s-1)/\zeta(s) & \\ d(n) & \zeta(s)^2 & \\ \mu(\gcd(n, 2)) & \eta(s) = (1-2^{1-s})\zeta(s) & \\ \lambda(n) & \zeta(2s)/\zeta(s) \\ \gamma(n) & \prod_{p \in \mathbb P}\frac{1-2p^{-s}}{1-p^{-s}} & \\ f^{[k]}(n) & \mathcal D[f](ks) & \\ f(n)\ln n & -\mathcal D[f]’ (s) & f\text{ completely multiplicative}\\ \Lambda(n) & -\zeta’(s)/\zeta(s) & \\ \Lambda(n)/\ln(n) & \ln\zeta(s) & \\ 1_{\mathbb P}(n) & \sum_{n=1}^\infty \frac{\mu(n)}{n}\ln\zeta(ns) & \\ 1_{\mathcal P}(n) & \sum_{n=1}^\infty \frac{\varphi(n)}{n}\ln\zeta(ns) & \\ \psi_k(n) & \zeta(s)\zeta(s - k)/\zeta(2s) & \\ J_k(n) & \zeta(s - k)/\zeta(s) & \end{array}\]

---

1. Viewing natural numbers as multisets, |D_n| is the set of all sub-multisets of |n|. The isomorphism described is then simply the fact that given any sub-multiset of the union of two disjoint multisets, we can sort the elements into their original multisets producing two sub-multisets of the disjoint multisets.↩︎

2. Incidence algebras are a decategorification of the notion of a category algebra.↩︎

August 22, 2025 11:25 PM

You could have invented CuTe hierarchical layout (but maybe not the rest of it?)

CuTe is a C++ library that aims to make dealing with complicated indexing easier. A key part of how it does this is by defining a Layout type, which specifies how to map from logical coordinates to physical locations (CuTe likes to say layouts are "functions from integers to integers.") In fact, CuTe layouts are a generalization of PyTorch strides, which say you always do this mapping by multiplying each coordinate with its respective stride and summing them together, e.g., i0 * s0 + i1 * s1 + .... Although NVIDIA's docs don't spell it out, the CuTe's generalization here is actually very natural, and in this blog post I'd like to explain how you could have invented it (on a good day).

First, a brief recap about strides. PyTorch views allow us to reinterpret the physical layout of a tensor in different ways, changing how we map logical coordinates into physical locations. For example, consider this 2-D tensor:

>>> torch.arange(4).view(2, 2)
tensor([[0, 1],
        [2, 3]])
>>> torch.arange(4).view(2, 2).stride()
(2, 1)

The physical memory reads 0, 1, 2, 3, and if I want to know what the value at coordinate (0, 1) is (row 0, col 1), I compute 0 * 2 + 1 * 1, which tells me I should read out the value at index 1 in physical memory. If I change the strides, I can change the order I read out the physical locations. For example, if I transpose I have:

>>> torch.arange(4).view(2, 2).T
tensor([[0, 2],
        [1, 3]])
>>> torch.arange(4).view(2, 2).T.stride()
(1, 2)

The physical memory hasn't changed, but now when we read out coordinate (0, 1), we compute 0 * 1 + 1 * 2, which tells me I should read the value at index 2 (which is indeed what I see at this coordinate!)

PyTorch also allows us to "flatten" dimensions of a tensor, treating them as a 1D tensor. Intuitively, a 2-D tensor flattened into a 1-D one involves just concatenating all the rows together into one line:

>>> torch.arange(4).view(2, 2).view(-1)
tensor([0, 1, 2, 3])

We should be able to do this for the transpose too, getting tensor([0, 2, 1, 3]), but instead, this is what you get:

>>> torch.arange(4).view(2, 2).T.view(-1)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
RuntimeError: view size is not compatible with input tensor's size and stride (at least one dimension spans across two contiguous subspaces). Use .reshape(...) instead.

The dreaded "use reshape instead" error! The error is unavoidable under PyTorch striding: there is no stride we can select that will cause us to read the elements in this order (0, 2, 1, 3); after all, i0 * s0 is a pretty simple equation, we can't simultaneously have 1 * s0 == 2 and 2 * s0 == 1.

Upon learning this, an understandable reaction is to just shrug, assume that this is impossible to fix, and move on with your life. But today, you are especially annoyed by this problem, because you were only trying to flatten N batch dimensions into a single batch dimension so that you could pass it through a function that only works with one batch dimension, with the plan of unflattening it when you're done. It doesn't matter that this particular layout is inexpressible with strides; you aren't going to rely on the layout in any nontrivial way, you just care that you can flatten and then unflatten back to the original layout.

Imagine we're dealing with a tensor of size (2, 2, 2) where the strides for dim 0 and dim 1 were transposed as (2, 4, 1). It should be OK to flatten this into a tensor (4, 2) and then unflatten it back to (2, 2, 2). Intuitively, I'd like to "remember" what the original sizes and strides are, so that I can go back to them. Here's an idea: let's just store the original size/stride as a nested entry in our size tuple. So instead of the size (4, 2), we have ((2, 2), 2); and now analogously the stride can simply be ((2, 4), 1). When I write (2, 2) as the "size" of a dimension, I really just mean the product 4, but there is some internal structure that affects how I should index its inside, namely, the strides (2, 4). If I ask for the row at index 2, I first have to translate this 1D coordinate into a 2D coordinate (1, 0), and then apply the strides to it like before.

Well, it turns out, this is exactly how CuTe layouts work! In CuTe, sizes/strides are hierarchical: a size is actually a tree of ints, where the hierarchy denotes internal structure of a dimension that you can address linearly (in fact, everything by default can be addressed in a 1-D linear way, even if its an N-D object.) The documentation of Layout does say this... but I actually suffered a lot extracting out the high level intuition of this blog post, because CuTe uses co-lexicographic ordering when linearizing (it iterates over coordinates (0,0), (1,0), (2,0), etc. rather than in the more normal lexicographic order (0,0), (0,1), (0,2)). This leads to some truly deranged example code where they print a 2D matrix in conventional lexicographic ordering, and then turn around and say, "But wait, if I have the layout take care of translating the 1D coordinate into an ND coordinate, it is colexicographic!!":

> print2D(s2xh4)
  0    2    1    3
  4    6    5    7
# sure, why not?

> print1D(s2xh4)
  0    4    2    6    1    5    3    7
# wtf???

In any case, if you want to engage with the documentation, s2xh4 is the important example to pay attention to for understanding the nested semantics. However, note the example is smeared across like five sections and also you need to know about the co-lexicographic thing to understand why the examples print the way they do.

by Edward Z. Yang at August 22, 2025 06:48 AM

Decidable equality for indexed data types, take 2

Decidable equality for indexed data types, take 2

Posted on August 22, 2025
Tagged agda, equality, path, dependent, indexed, agda

In a post from a year ago, I explored how to prove decidable equality in Agda of a particular indexed data type. Recently, I discovered a different way to accomplish the same thing, without resorting to embedded sigma types.

This post is literate Agda; you can download it here if you want to play along. I tested everything here with Agda version 2.6.4.3 and version 2.0 of the standard library. (I assume it would also work with more recent versions, but haven’t tested it.)

Background

This section is repeated from my previous post, which I assume no one remembers.

First, some imports and a module declaration. Note that the entire development is parameterized by some abstract set B of base types, which must have decidable equality.

open import Data.Product using (Σ ; _×_ ; _,_ ; -,_ ; proj₁ ; proj₂)
open import Data.Product.Properties using (≡-dec)
open import Function using (_∘_)
open import Relation.Binary using (DecidableEquality)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
open import Relation.Nullary.Decidable using (yes; no; Dec)

module OneLevelTypesIndexed2 (B : Set) (≟B : DecidableEquality B) where

We’ll work with a simple type system containing base types, function types, and some distinguished type constructor □. So far, this is just to give some context; it is not the final version of the code we will end up with, so we stick it in a local module so it won’t end up in the top-level namespace.

module Unindexed where
  data Ty : Set where
    base : B → Ty
    _⇒_ : Ty → Ty → Ty
    □_ : Ty → Ty

For example, if \(X\) and \(Y\) are base types, then we could write down a type like \(\square ((\square \square X \to Y) \to \square Y)\):

  infixr 2 _⇒_
  infix 30 □_

  postulate
    BX BY : B

  X : Ty
  X = base BX
  Y : Ty
  Y = base BY

  example : Ty
  example = □ ((□ □ X ⇒ Y) ⇒ □ Y)

However, for reasons that would take us too far afield in this blog post, I don’t want to allow immediately nested boxes, like \(\square \square X\). We can still have multiple boxes in a type, and even boxes nested inside of other boxes, as long as there is at least one arrow in between. In other words, I only want to rule out boxes immediately applied to another type with an outermost box. So we don’t want to allow the example type given above (since it contains \(\square \square X\)), but, for example, \(\square ((\square X \to Y) \to \square Y)\) would be OK.

Two encodings

In my previous blog post, I ended up with the following encoding of types indexed by a Boxity, which records the number of top-level boxes. Since the boxity of the arguments to an arrow type do not matter, we make them sigma types that package up a boxity with a type having that boxity. I was then able to define decidable equality for ΣTy and Ty by mutual recursion.

data Boxity : Set where
  ₀ : Boxity
  ₁ : Boxity

variable b b₁ b₂ b₃ b₄ : Boxity

module WithSigma where
  ΣTy : Set
  data Ty : Boxity → Set

  ΣTy = Σ Boxity Ty

  data Ty where
    □_ : Ty ₀ → Ty ₁
    base : B → Ty ₀
    _⇒_ : ΣTy → ΣTy → Ty ₀

The problem is that working with this definition of Ty is really annoying! Every time we construct or pattern-match on an arrow type, we have to package up each argument type into a dependent pair with its Boxity; this introduces syntactic clutter, and in many cases we know exactly what the Boxity has to be, so it’s not even informative. The version we really want looks more like this:

data Ty : Boxity → Set where
  base : B → Ty ₀
  _⇒_ : {b₁ b₂ : Boxity} → Ty b₁ → Ty b₂ → Ty ₀
  □_ : Ty ₀ → Ty ₁

infixr 2 _⇒_
infix 30 □_

In this version, the boxities of the arguments to the arrow constructor are just implicit parameters of the arrow constructor itself. Previously, I was unable to get decidable equality to go through for this version… but just the other day, I finally realized how to make it work!

Path-dependent equality

The key trick that makes everything work is to define a path-dependent equality type. I learned this from Martín Escardó. The idea is that we can express equality between two indexed things with different indices, as long as we also have an equality between the indices.

_≡⟦_⟧_ : {A : Set} {B : A → Set} {a₀ a₁ : A} → B a₀ → a₀ ≡ a₁ → B a₁ → Set
b₀ ≡⟦ refl ⟧ b₁   =   b₀ ≡ b₁

That’s exactly what we need here: the ability to express equality between Ty values, which may be indexed by different boxities—as long as we know that the boxities are equal.

Decidable equality for Ty

We can now use this to directly encode decidable equality for Ty. First, we can easily define decidable equality for Boxity.

Boxity-≟ : DecidableEquality Boxity
Boxity-≟ ₀ ₀ = yes refl
Boxity-≟ ₀ ₁ = no λ ()
Boxity-≟ ₁ ₀ = no λ ()
Boxity-≟ ₁ ₁ = yes refl

Here is the type of the decision procedure: given two Ty values which may have different boxities, we decide whether or not we can produce a witness to their equality. Such a witness consists of a pair of (1) a proof that the boxities are equal, and (2) a proof that the types are equal, depending on (1).We would really like to write this as Σ (b₁ ≡ b₂) λ p → σ ≡⟦ p ⟧ τ, but for some reason Agda requires us to fill in some extra implicit arguments before it is happy that everything is unambiguous, requiring some ugly syntax.

Ty-≟′ : (σ : Ty b₁) → (τ : Ty b₂) → Dec (Σ (b₁ ≡ b₂) λ p → _≡⟦_⟧_ {_} {Ty} σ p τ)

Before showing the definition of Ty-≟′, let’s see that we can use it to easily define both a boxity-homogeneous version of decidable equality for Ty, as well as decidable equality for Σ Boxity Ty:

Ty-≟ : DecidableEquality (Ty b)
Ty-≟ {b} σ τ with Ty-≟′ σ τ
... | no σ≢τ = no (λ σ≡τ → σ≢τ ( refl , σ≡τ))
... | yes (refl , σ≡τ) = yes σ≡τ

ΣTy-≟ : DecidableEquality (Σ Boxity Ty)
ΣTy-≟ (_ , σ) (_ , τ) with Ty-≟′ σ τ
... | no σ≢τ = no λ { refl → σ≢τ (refl , refl) }
... | yes (refl , refl) = yes refl

A lot of pattern matching on refl and everything falls out quite easily.

And now the definition of Ty-≟′. It looks complicated, but it is actually not very difficult. The most interesting case is when comparing two arrow types for equality: we must first compare the boxities of the arguments, then consider the arguments themselves once we know the boxities are equal.

Ty-≟′ (□ σ) (□ τ) with Ty-≟′ σ τ
... | yes (refl , refl) = yes (refl , refl)
... | no σ≢τ = no λ { (refl , refl) → σ≢τ (refl , refl) }
Ty-≟′ (base S) (base T) with ≟B S T
... | yes refl = yes (refl , refl)
... | no S≢T = no λ { (refl , refl) → S≢T refl }
Ty-≟′ (_⇒_ {b₁} {b₂} σ₁ σ₂) (_⇒_ {b₃} {b₄} τ₁ τ₂) with Boxity-≟ b₁ b₃ | Boxity-≟ b₂ b₄ | Ty-≟′ σ₁ τ₁ | Ty-≟′ σ₂ τ₂
... | no b₁≢b₃ | _ | _ | _ = no λ { (refl , refl) → b₁≢b₃ refl }
... | yes _ | no b₂≢b₄ | _ | _ = no λ { (refl , refl) → b₂≢b₄ refl }
... | yes _ | yes _ | no σ₁≢τ₁ | _ = no λ { (refl , refl) → σ₁≢τ₁ (refl , refl) }
... | yes _ | yes _ | yes _ | no σ₂≢τ₂ = no λ { (refl , refl) → σ₂≢τ₂ (refl , refl) }
... | yes _ | yes _ | yes (refl , refl) | yes (refl , refl) = yes (refl , refl)
Ty-≟′ (□ _) (base _) = no λ ()
Ty-≟′ (□ _) (_ ⇒ _) = no λ ()
Ty-≟′ (base _) (□ _) = no λ ()
Ty-≟′ (base _) (_ ⇒ _) = no λ { (refl , ()) }
Ty-≟′ (_ ⇒ _) (□ _) = no λ ()
Ty-≟′ (_ ⇒ _) (base _) = no λ { (refl , ()) }

<noscript>Javascript needs to be activated to view comments.</noscript>

by Brent Yorgey at August 22, 2025 12:00 AM