Binomial queues as a nested type

Warning: this is probably only of interest to functional programmers.

Maciej Kotowicz recently asked on the Haskell Cafe mailing list about implementing binomial queues (also known as binomial heaps) using fancy type machinery so that the type-checker can enforce the shape invariants of the data structure. This reminded me of a discussion I had with some colleagues in the summer of 1998 about using nested types to enforce these kinds of invariants. A little digging around in mail archives yielded this email, presented here with some light formatting and a few fixed typos.

I've been playing with binomial queues as a nested type, and I think you'll find the end result interesting.

REVIEW

Let me first quickly review the usual implementation of binomial queues. Recall that a binomial tree has the shape

data Tree a = Node a [Tree a]

A binomial tree of rank k has k children, of ranks k-1 .. 0 (stored in the list in decreasing order of rank). Note that we can combine two heap-ordered binomial trees of rank k to get a heap-ordered binomial tree of rank (k+1) as follows:

combine a@(Node x xs) b@(Node y ys)
   | x <= y    = Node x (b : xs)
   | otherwise = Node y (a : ys)

Now a binomial queue is a list of heap-ordered binomial trees of increasing height (but not necessarily of consecutive ranks). We'll represent the ranks of those trees that are present by their position in the tree. Thus, some ranks will be empty. This could be implemented as

type Binom a = [Maybe (Tree a)]

or somewhat more efficiently as

data Binom a = Nil
             | Zero (Binom a)
             | One (Tree a) (Binom a)

or better still by unboxing the Tree in the One constructor

data Binom a = Nil
             | Zero (Binom a)
             | One a [Tree a] (Binom a)

I won't go over all the operations -- they are amply covered elsewhere. I'll just describe two functions. The first, add, takes a tree and a list (where the tree has the same rank as the first position in the list), and returns a new list. It works basically like the increment function on binary numbers.

add :: Ord a => a -> [Tree a] -> Binom a -> Binom a
add x xs Nil = One x xs Nil
add x xs (Zero h) = One x xs h
add x xs (One y ys h)
  | x <= y    = Zero (add x (Node y ys : xs) h)
  | otherwise = Zero (add y (Node x xs : ys) h)

The merge function is similar and works basically like the addition function on binary numbers.

Finally, the getMin function returns the minimum element of a queue paired with the queue without that element. The helper function getMin_ returns a triple of the minimum element in some suffix of the queue, the list of children associated with that minimum element, and the suffix without that element.

getMin_ :: Ord a => Binom a -> (a, [Tree a], Binom a)
getMin_ (Zero h) = case getMin_ h of
                     (y,ys,h') -> (y,ys,Zero h')
getMin_ (One x xs Nil) = (x,xs,Nil)
getMin_ (One x xs h) = case getMin_ h of
                         (y,ys,h') | x <= y    -> (x,xs,Zero h)
                                   | otherwise -> (y,ys,One x xs h')

getMin :: Ord a => Binom a -> (a, Binom a)
getMin h = let (x,xs,h') = getMin_ h
           in (x,merge (list2binom xs Nil) h')

list2binom [] h = h
list2binom (Node x xs : ys) h = list2binom ys (One x xs h)

Note that when getMin receives a list of children, it converts them to a valid binomial queue by reversing the list (and changing each pair of a Node constructor and a (:) constructor to a One constructor).

NESTED REPRESENTATION -- FIRST ATTEMPT

By following the same approach we have been using to design nested datatypes, we get the following representation of binomial queues.

data Binom_ a b = Nil
                | Zero (Binom_ a (Trees a b))
                | One a b (Binom_ a (Trees a b))

type Trees a b = (a, b, b)

type Binom a = Binom_ a ()

Here the list of children

  (Node x3 xs3 : Node x2 xs2 : Node x1 xs1 : Node x0 xs0 : [])

is being represented by the nested triples

  (xs3,xs3', (x2,xs2', (x1,xs1', (x0,xs0', ()))))

(where xsN' is the appropriate conversion of xsN).

All the functions are perfectly straightforward, except for getMin and getMin_ which must incrementally build up the reversing function to convert

  (xs3,xs3', (x2,xs2', (x1,xs1', (x0,xs0', ()))))

to

  One x0 xs0' (One x1 xs1' (One x2 xs2' (One x3 xs3' Nil)))

As a result of building up this reverse function incrementally, this implementation ends up being roughly 10% slower than the original.

INTERLUDE ON REVERSING LISTS

Suppose we want to support the following ADT. We want sequences with three operations:

empty :: ReversableSeq a
cons  :: a -> ReversableSeq a -> ReversableSeq a
rev   :: ReversableSeq a -> [a]

with the obvious semantics. cons must take O(1) time, but rev may take O(n) time. A list is a reasonable implementation with

type ReversableSeq a = [a]
empty = []
cons = (:)
rev = reverse

but, if you think about it, there's a fair amount of interpretive overhead in the pattern matching that reverse performs at every step. Way back in 1985, John Hughes came up with a representation that avoids this overhead:

type ReversableSeq a = [a] -> [a]
empty = id
cons x xs = xs . (x:)
rev xs = xs []

The result of cons 1 (cons 2 (cons 3 empty)) is

id . (3:) . (2:) . (1:)

which, when applied to [] by the rev function, yields [3,2,1]. One way to think of this representation is as lists with "holes" at the ends. The cons operation fills in this hole with an element and another hole, and the rev operation fills in the hole with []. (This is quite similar to difference lists in logic programming...)

Applying this trick to the regular representation of binomial queues yields

data Binom a = Nil
             | Zero (Binom a)
             | One a (Binom a -> Binom a) (Binom a)

which turns out to be about 10% faster than the original representation.

NESTED REPRESENTATION -- SECOND ATTEMPT

Ok, let's try to make a nested datatype out of this. Conceptually, the nesting should keep track of our position in the queue so that we know what rank the current tree has and can't possibly mix up trees of different ranks. We hypothesize some Base type for the beginning of the list, and some type transformer Succ that modifies the type as we move down the queue.

type Base = ???
type Succ b = ???  -- this might need to be Succ a b

type Binom a = Binom_ a Base

data Binom_ a b = Nil
                | Zero (Binom_ a (Succ b))
                | One a (Binom_ a ??? -> Binom_ a ???) (Binom_ a (Succ b))

Now, what should the missing types in the One constructor be? Well, the function (Binom_ a ??? -> Binom_ a ???) represents the children of the current node. If this node is of rank k, then these children are of ranks 0 .. k-1. The function (Binom_ a ??? -> Binom_ a ???) takes a queue starting at rank k and adds the children to the front of it, yielding a queue starting at rank 0. So the ???'s can be filled in as

                | One a (Binom_ a b -> Binom_ a Base) (Binom_ a (Succ b))

or just

                | One a (Binom_ a b -> Binom a) (Binom_ a (Succ b))

Now, what should the types Base and Succ be? It doesn't matter because we never construct data of those types, we simply use the types to discriminate between positions in the queue. So we can define Base and Succ as

type Base = Void
newtype Succ b = S Void

I think this is a very interesting type for several reasons:

• It includes an arrow type, which we haven't seen much.
• The RHS of the datatype definition (in fact, just the One constructor) has occurrences of Binom_ at no fewer than three different types

  Binom_ a b
  Binom_ a Base
  Binom_ a (Succ b)
  

  I've seen two before, but not three.
• It includes types which are never used, but are merely there to capture certain invariants (in this case, that trees of different ranks should never be confused). [2009 Comment: Today, these are called phantom types.] In some ways this might make this type less interesting, but an interesting consequence is that the code satisifes a certain "type erasure" property: if you erase the types from all the functions, you get code for the optimized regular representation.

Because of this "type erasure" property, you might expect it to be just as fast as the optimized regular representation, but in fact it is roughly 10% slower -- or roughly as fast as the original regular representation. This is because the extra types hinder a certain optimization that the programmer might make (and which I did make in the optimized regular representation).

Recall the type of the getMin_ function from the original regular representation, and the way it was used by getMin.

getMin_ :: Ord a => Binom a -> (a, [Tree a], Binom a)

getMin :: Ord a => Binom a -> (a, Binom a)
getMin h = let (x,xs,h') = getMin_ h
           in (x,merge (list2binom xs Nil) h')

For the optimized regular representation, this becomes

getMin_ :: Ord a => Binom a -> (a, Binom a -> Binom a, Binom a)

getMin :: Ord a => Binom a -> (a, Binom a)
getMin h = let (x,xs,h') = getMin_ h
           in (x,merge (xs Nil) h')

Now, consider the optimized nested representation. We can't just write

getMin_ :: Ord a => Binom_ a b -> (a, Binom_ a b -> Binom a, Binom_ a b)

because we don't know the rank of the tree that the second component of the triple came from. (Note that if we had existential types, we could write

getMin_ :: Ord a => Binom_ a b -> 
                    (a, exists c. Binom_ a c -> Binom a, Binom_ a b)

getMin :: Ord a => Binom a -> (a, Binom a)
getMin h = let (x,xs,h') = getMin_ h
           in (x,merge (xs Nil) h')

Some implementations do in fact support existential types, but in limited ways that would carry efficiency costs of their own...)

Instead of returning the children and then applying them to Nil at the end, we apply the children to Nil first, and then return the result, yielding the type

  
getMin_ :: Ord a => Binom_ a b -> (a, Binom a, Binom_ a b)

getMin :: Ord a => Binom a -> (a, Binom a)
getMin h = let (x,xs,h') = getMin_ h
           in (x,merge xs h')

This depends on laziness to evaluate only the children of the final minimum, and not all the children of the temporary minimums along the way. However, this does mean that we build a lot more thunks of the form (xs Nil) along the way. And building these thunks is apparently quite expensive.

2009 Addendum Ralf Hinze considers a similar representation in Section 6 of Numerical Representations as Higher-Order Nested Datatypes. Today, you would probably use fancier type machinery like dependent types or maybe GADTs, but it's still amazing how far you can get with only nested types.

Score one for induction!

One of my favorite textbooks on algorithms—in spite of the fact that it's twenty years old—is Udi Manber's Introduction to Algorithms: A Creative Approach. However, I have never been tempted to actually use it in class. You see, the book's greatest strength is also its greatest weakness.

Most textbooks on algorithms show you a lot of polished algorithms, but provide little or no insight on how to go about designing such algorithms. Manber's book does a very good job providing such insight, by making an analogy with inductive proofs. If you have any skill with induction, then you can use Manber's approach to help you design algorithms. (Of course, this should come as no surprise since writing an inductive proof and writing a recursive function are essentially the same activity.)

I'm sure you see the flaw here—most students are even less comfortable with induction than they are with recursion. It's like trying to help somebody learn to drive a car by making an analogy with riding a unicycle. For a certain segment of the audience, that analogy might be just what they need, but for the most of the audience, the analogy will only produce puzzled looks.

I was recently helping a student who was struggling to get a handle on recursion. He was making the common beginner mistake of trying to think about what happens during the recursive call instead of trusting that the recursive call works (sometimes called the recursive leap of faith). By sheer coincidence, I had happened to notice the day before that this student had done very well in our discrete math course the previous year. Time to give it a try...

“You know when you're writing a proof by induction and at some point you use the inductive hypothesis? That's just like a recursive call. You don't worry about what happens inside the inductive hypothesis, you just say ‘Assume that it works for N-1...’ It's the same with recursion. You just assume that the recursive call works.”

That comparison actually seemed to help. Maybe Manber was onto something after all!

Less than vs Greater than

From math, we know that X < Y is the same as Y > X. But in programming, they're not the same.

Oh, I'm not talking about situations where X and Y have side effects that interact badly. Instead, I'm talking about situations where one may be more error prone than the other.

Although the two expressions are mathematically equivalent, they're not linguistically equivalent. One focuses attention on something being smaller, and the other focuses attention on something being bigger. For example, it is a relatively common mistake to go the wrong way when searching a binary search tree. However, almost every time I run into this error, the student has also written the comparisons backward from the direction I think of as “natural”.

Consider the following function for determining whether a given key x appears in a binary search tree t:

  function member(x,t) is
     if t = null then return false
     if t.key = x then return true
     if t.key < x then return member(x,t.left)
     if t.key > x then return member(x,t.right)

The fact that I've written this using recursion instead of iteration is irrelevant. What matters is that the third case goes left when it should go right, and vice versa for the fourth case. But looking more carefully at that third case

     if t.key < x then return member(x,t.left)

I'm not particularly surprised by the error. The comparison t.key < x focuses attention on something being smaller, and the left side of the tree is where the smaller keys go. By asking whether x is smaller than t.key, rather than whether t.key is smaller than x, I think we're much less likely to fall into this trap.

Hey, you got your loop in my recursion!

I've written before about trying to diagnose students' broken or ineffective mental models from the mistakes they make. Here's a mistake that I see frequently from students who are not yet comfortable with recursion.

Say you wanted to write a function to calculate the sum of a list using a loop. Many students could easily write something like

   function sum(list) is
      variable total := 0
      while list /= null do
         total := total + list.item
         list := list.next
      return total

But ask them to write the sum function using recursion, and you might get something like

   function sum(list) is
      variable total := 0
      if list = null then
         return total
      else
         total := total + list.item
         return sum(list.next)

Of course, this code always returns 0. It's pretty clear that the writer had the iterative algorithm in mind, and doesn't understand that each recursive call to sum creates a new instance of the total variable.

When I watch such a student writing code like this, he often declares the variable immediately, before even beginning to think about what the recursive decomposition is going to look like, an almost spinal reflex conditioned by several semesters of writing loops. I can explain recursion until I'm hoarse and draw pictures until my hand cramps up, but I can't compete with the will-o'-the-wisp allure of that variable. Once it's there, it will almost inevitably lead the student to his doom in the bogs of iterative thinking.

One trick to help such a student is to break the cycle where it begins, by getting rid of that variable. Tell him to write the function without using any local or global variables. Or, if he really thinks he needs a variable, to declare it as a constant instead. Of course, there are times when a variable is perfectly appropriate inside a recursive function, but such examples can often be avoided until the student has a better grasp of recursion.

In search of epiphany

I watched the movie Proof last night. I highly recommend it. It's not often that mathematicians get so much screen time.

The nature of mathematical creativity plays a large role in the movie. One comment was especially intriguing. (Minor spoiler ahead.) In describing the process of solving a particularly difficult problem, one character says, “It was like...connecting dots. Some nights I...I could connect three or four of them. And some nights they'd be really far apart. I'd have no idea how to get to the next one, if there was the next one.”

This description rings both true and false for me. The true part is I'd have no idea how to get to the next one, if there was the next one. This nicely summarizes what it's like to work on a hard problem. You don't know what to do next, and you're not sure that a solution even exists.

But the connecting dots part doesn't feel right. It makes the process sound linear, when the reality is anything but. In my experience, the really hard problems—the ones that require the most creativity—are most often solved by epiphany, by having the whole solution burst into your head, seemingly in an instant. That's when the connecting dots part happens, but it all happens at once, not a few a time.

Of course, the catch is that epiphany can't be forced. I'm reminded of the old joke about the lottery. A man prays fervently every night, “Please, Lord, let me win the lottery tomorrow.” After twenty years, a heavenly voice responds, “Would you buy a ticket already!”

No, you can't just sit around waiting for an epiphany to happen. Epiphanies are hard work! TANSTAAFL. So, how do you go about searching for epiphany? Every epiphany I've ever had has been the result of a two-pronged effort.

The first prong is building up sweat equity. I thoroughly explore the space around the problem, playing with the problem from many different angles. Of course, I'm actively trying to solve the problem during this time, because I might get lucky and stumble across a solution. But I don't worry too much if I don't seem to be getting anywhere. This part of the process is not so much about connecting the dots as about building lots and lots (and lots) of potential connections.

The second prong is staying alert. That's easy to say, but really hard to do over long periods of time. Eventually, I hope, some stray thought or some environmental trigger will start a cascade, where some subset of those potential connections will become actual connections, creating a path to the solution. Sometimes this happens when you're relaxed and your mind is drifting, such as in the shower or while driving. I remember once in grad school trying all afternoon to track down a bug. That night my wife and I went over to a friend's house for dinner. Everybody was shocked when, in the middle of beef stroganoff, I suddenly shouted out, “That's it!”

Other times the epiphany can happen while you're actively working on something else. For example, the key insight behind TradeMaximizer came while I was trying to put together a homework for my Algorithms class. I had been working off and on for weeks trying to find cycles in the trade graph. But I had set that aside and was coming up with homework problems, when I stumbled across a stray comment that talked about converting a directed graph into a bipartite graph. That sentence was enough to set off the chain reaction of connections and, within seconds, TradeMaximizer was born.

Probably the most famous story about scientific epiphany is that of Archimedes' bath. Funny story: Shortly after announcing TradeMaximizer to the math trade community on BoardGameGeek, I received a peevish email from another BoardGameGeek user who thought he also had a solution. He described how he had come to BoardGameGeek, eager to share his discovery, only to find my announcement first. He complained “Argh! Way to shout ‘Eureka!’ while Archimedes is drying himself off!” (The other solution turned out to be bogus.)

Games for Programmers: Black Vienna

The next in an irregular series of board game recommendations for programmers. Of course, you don't have to be a programmer to enjoy these games, but if you are a programmer, then I think there's a pretty good chance that you'll like them.

O frabjous day!

My favorite deduction game, Black Vienna, has long been out of print, but now you can give it a try online, thanks to the efforts of Greg Aleknevicus. Go check out Black Vienna Online. It's free and easy to use. The user interface isn't going to win any awards, but it gets the job done. I'm thrilled that this game can now reach a wider audience.

Most deduction games are for two players, but Black Vienna handles three to six players. Your goal is to figure out the members of the infamous “Black Vienna” gang. There are 27 suspect cards, labeled A-Z and Ö. At the beginning of the game, three of these cards are chosen randomly and set aside. Those are the members of the gang.

The remaining 24 suspect cards are dealt out evenly to the players. (With 5 players, one of the players gets only 4 cards.) These are the cards of suspects for whom you can provide alibis.

On your turn you conduct an investigation. There is a pool of available investigation cards, each showing three suspects. You choose one of the available investigation cards and place it in front of another player. That player marks the card with plastic chips, according to how many of the suspects are in her hand. For example, if I have the cards BGMTXY and somebody plays the BQT card on me, I would mark it with two chips (for the B and the T). Other players would then know that I had two of the three suspects, but not necessarily which ones.

The turn then passes to the player who was just investigated.

One nice thing about Black Vienna as a game is that every player is involved on every turn. Even if you are not actively part of the investigation, you still need to update your information with the results of the investigation, and follow any chains of deductions to their conclusions.

Example Deductions

Some deductions are obvious. For example, if I played two chips on the BQT card, and you have the Q card in your hand, then you know that I have the B and the T. Other deductions are less obvious. Here's an actual example from a recent game. Call the other players Caitlin, Monica, Drew, and Dom.

Monica played one chip on GPX, but I had the X, so I knew that she had either G or P (but not both). Similarly, she also played one chip on DHR, but I knew Dom had the R, so Monica had either D or H. Finally, she played two chips on LNV.

Drew played one chip on DVY and zero chips on FÖY, so he had either D or V. Between Drew and Monica, they had at least 4 of the 5 cards DHLNV and at least 5 of the 7 cards DGHLNPV (possibly more if Drew had any of GHLNP).

Meanwhile, I knew all but two of Caitlin's cards. The only possibilities for those last two cards were DGHLNPV. Monica and Drew together had at least 5 of those 7 cards, so Monica, Drew, and Caitlin together must have all 7.

This tells me that none of these 7 cards are in the gang, and none of these 7 cards are in Dom's hand. It also tells me that Drew does not have any of GHLNP.

Finally, I can be more specific about Caitlin's cards. One of her two cards is G or P, and the other is one of DHLNV.

Online Play

The online implementation is asynchronous. You do not need to be logged in at the same time as other players. Instead, the system emails you whenever a turn is taken with the results of the investigation. When it is your turn, you can log on and take your turn at your leisure. This means that a 45-minute face-to-face game can take days or even weeks when played online, but it also means that you can play the game with odd minutes here and there, instead of having to carve out a solid chunk of time. An additional benefit is that it is easy to play with friends in different time zones. For example, I frequently play with friends on the other side of the country.

However, the greatest benefit of the online implementation is that it does away with the greatest weakness of face-to-face play—player errors. Not errors in deductions, which would be your own fault and would only affect you, but errors in answering investigations. If a player carelessly puts out, say, one chip when he should have put out two chips, it ruins the game for everyone. Even if the player notices the error a few turns later and tries to correct it, it's far too late. By then, the other players have already updated their notes with deductions made from the faulty answer, and typically have no way of backing out of those deductions.

If you want to give Black Vienna a try, see the detailed rules of the game and the instructions for the online interface.

Addendum: I've played in several three-player games recently. It's ok with that number, but I think it's significantly better with four or five players. (I haven't tried six yet.) With three players, the deductions are less interesting, and there is a greater chance for one player to get lucky.

Breadth-First Numbering: An Algorithm in Pictures

I've always enjoyed the mathematical tradition of “proofs without words”, so I wanted to see if something similar could be done with an algorithm. Of course, an algorithm is typically more complicated than a mathematical identity, so it's not surprising that an algorithm typically can't be captured in a single picture. Instead, I've found the idea of a commutative diagram to be a useful pictorial shorthand, where the short way around the diagram gives a high-level view of the operation, and the long way around gives more detail. Here is an attempt to describe my breadth-first numbering algorithm from ICFP 2000 using this idea.

Wanted

Rules

Example