Paper Content:
Page 1:
Binomial Tabulation: A Short Story
HSIANG-SHANG KO and SHIN-CHENG MU, Academia Sinica, Taiwan
JEREMY GIBBONS, University of Oxford, UK
We reconstruct some of the development in Richard Bird’s [2008] paper Zippy Tabulations of Recursive Functions ,
using dependent types and string diagrams rather than mere simple types. This paper serves as an intuitive
introduction to and demonstration of these concepts for the curious functional programmer, who ideally
already has some exposure to dependent types and category theory, is not put off by basic concepts like
indexed types and functors, and wants to see a more practical example.
The paper is presented in the form of a short story, narrated from the perspective of a functional programmer
trying to follow the development in Bird’s paper. The first section recaps the original simply typed presentation.
The second section explores a series of refinements that can be made using dependent types. The third section
uses string diagrams to simplify arguments involving functors and naturality. The short story ends there, but
the paper concludes with a discussion and reflection in the afterword.
1 FUNCTIONS
‘What on earth is this function doing?’
I stare at the late Richard Bird’s [2008] paper Zippy Tabulations of Recursive Functions , frowning.
cd :: B a -> B (L a)
cd (Bin (Tip y) (Tip z)) = Tip [y,z]
cd (Bin (Tip y) u ) = Tip (y : ys) where Tip ys = cd u
cd (Bin t (Tip z)) = Bin (cd t) (mapB (: [z]) t)
cd (Bin t u ) = Bin (cd t) (zipBWith (:) t (cd u))
I know Bis this Haskell data type of binary trees:
data B a = Tip a | Bin (B a) (B a)
Presumably mapB andzipBWith are the usual map and zip functions for these trees, and Lis the
standard list type. But how did Richard come up with such an incomprehensible function definition?
He didn’t bother to explain it in his paper. It might have helped if he had provided some examples.
1.1 Top-Down and Bottom-Up Algorithms
From the explanations that arein the paper, I suppose I can guess roughly what cdshould do.
Richard was studying the relationship between top-down and bottom-up algorithms that solve
problems specified recursively on some input data structure. When the input is a nonempty list, a
generic top-down algorithm is defined by
td :: (a -> s) -> (L s -> s) -> L a -> s
td f g [x] = f x
td f g xs = g (map (td f g) (dc xs))
The input of tdis a nonempty list of a’s, and the output is a solution of type sfor the input list.
Singleton lists form the base case, for which the given function fcomputes a solution directly. If an
input list xsis not singleton, it is decomposed into shorter lists by some dc :: L a -> L (L a) .
Then tdrecursively computes a subsolution for each shorter list. Finally, gcombines the subsolutions
Authors’ addresses: Hsiang-Shang Ko, joshko@iis.sinica.edu.tw; Shin-Cheng Mu, scm@iis.sinica.edu.tw, Academia Sinica,
Institute of Information Science, 128 Academia Road, Taipei, Taiwan, 115201; Jeremy Gibbons, jeremy.gibbons@cs.ox.ac.uk,
University of Oxford, Department of Computer Science, Wolfson Building, Parks Road, Oxford, UK, OX1 3QD.arXiv:2503.04001v1 [cs.PL] 6 Mar 2025
Page 2:
2 Hsiang-Shang Ko, Shin-Cheng Mu, and Jeremy Gibbons
td"abcd"td"abc"td"abd"td"acd"td"bcd"td"ab"td"ac"td"bc"td"ab"td"ad"td"bd"td"ac"td"ad"td"cd"td"bc"td"bd"td"cd"td"a"td"b"td"a"td"c"td"b"td"c"td"a"td"b"td"a"td"d"td"b"td"d"td"a"td"c"td"a"td"d"td"c"td"d"td"b"td"c"td"b"td"d"td"c"td"d"
Fig. 1. Computing td "abcd" top-down.
into a solution for xs. In fact, in order to cover a wider range of algorithms, Richard’s definition is
more abstract and general. But I’m working with this simplified version as an easier starting point.
In the last example of the paper, dccomputes all the immediate sublists of a given list — all the
lists with exactly one element missing:
dc :: L a -> L (L a)
dc [x,y] = [[x],[y]]
dc (xs ++ [x]) = [xs] ++ [ys ++ [x] | ys <- dc xs]
(Richard assumed that a list could be matched with a snoc pattern xs ++ [x] .) For example,
computing a solution for "abcd" requires subsolutions for "abc" ,"abd" ,"acd" , and "bcd" (Figure 1).
In turn, computing a solution for "abc" requires subsolutions for "ab" ,"ac" , and "bc" , and so on.
When the problem decomposition reaches length- 2sublists — that’s a bit of a mouthful, so let me
just say ‘ 2-sublists’ for short — it becomes evident that this dcleads to overlapping subproblems ,
andtddeals with that very inefficiently. For example, a solution for "ab" is required for solving
the problem for "abc" and"abd" , and tdcomputes that solution twice. And it gets worse further
down: a solution for each 1-sublist is computed 6times!
It’s better to proceed bottom-up instead, working upwards through a lattice of sublists (Figure 2),
level by level. Level 1consists of solutions for the 1-sublists. Then solutions for the (𝑘+1)-sublists
in level𝑘+1are computed from subsolutions in level 𝑘. Finally, the top level consists of a single
solution, for the input list. More specifically, if the levels were represented as lists, level 2would be
[td "ab", td "ac", td "bc", td "ad" ...]
One way to construct level 3from level 2would be using a function cd':: L a -> L (L a)
that copies and rearranges the elements such that the subsolutions for the immediate sublists of
the same list are brought together:
[[td "ab", td "ac", td "bc"], [td "ab", td "ad", td "bd"] ...]
Then applying map g to this list of lists would produce level 3:
[td "abc", td "abd", td "acd", td "bcd" ...]
If such a function cd'could be constructed, a bottom-up algorithm computing the same solution
astdwould be given by
bu':: (a -> s) -> (L s -> s) -> L a -> s
bu'f g = head . loop . map f
where loop [y] = [y]
loop ys = loop (map g (cd 'ys))
Level 1is obtained by applying fto each element of the input list. Then the loop function keeps
applying map g . cd 'to get the next level. It stops at a level with a single element, which is a
Page 3:
Binomial Tabulation: A Short Story 3
td "abcd"td "abc"td "abd"td "acd"td "bcd"td "ab"td "ac"td "bc"td "ad"td "bd"td "cd"td "a"td "b"td "c"td "d"level 1level 2level 3level 4level 0td ""
Fig. 2. Computing td "abcd" bottom-up.
solution for the entire input list. Like td, this bu'is a simplified version. To cope with more general
problems, Richard had to store something more complex in each level, but I don’t think I need that.
1.2 Rearranging Binary Trees
That’s what I understand about cdso far. But Richard must have realised at some point that it’s
difficult to define the cdrearrangement using lists, and decided to represent each level using the
Bdata type. So cd :: B a -> B (L a) , and the actual bottom-up algorithm buis defined by
bu :: (a -> s) -> (L s -> s) -> L a -> s
bu f g = unTip . loop . cvt . map f
where loop (Tip x) = Tip x
loop xs = loop (mapB g (cd xs))
where unTip extracts the element of a Tiptree, and cvtconverts a list to a tree:
unTip :: B a -> a cvt :: L a -> B a
unTip (Tip x) = x cvt [x] = Tip x
cvt (xs ++ [x]) = Bin (cvt xs) (Tip x)
I wonder if I have to use Binstead of lists in cd. If I’m given level 1 of the lattice (Figure 2) as a
4-list, I know they are solutions for the four 1-sublists, and surely there’s no problem rearranging
them for level 2. . . ?
Oh wait, I don’t actually know. All I get is a 4-list. This 4-list could be level 1, but it could well be
level 3. And I don’t get any information from the elements — the element type is parametrically
quantified. So there isn’t enough context for me to decide whether I should produce a 6-list (level 2)
or a 1-list (level 4).
Presumably, Richard’s trees gave him more context. I try to trace Richard’s cdto find out how it
works. Given input "abcd" , the function cvt . map f yields a tree slanted to the left as level 1:
Bin (Bin (Bin (Tip (td "a")) (Tip (td "b"))) (Tip (td "c"))) (Tip (td "d"))
Following Richard’s convention, I draw a Tip x asx, and Bin t u as a dot with tto its left and
ubelow (Figure 3). Applying mapB g . cd to this, I get level 2. For a closer look, I apply only cd
to level 2. Indeed, with its clever mapping and zipping, cdmanages to bring together precisely the
right elements, and produces a ‘level 21/2’. Then I reach level 3by applying mapB g . There’s indeed
more context for distinguishing levels 1and 3: their tree representations have the same size but
different shapes.
The intuition about having enough context seems useful. I was puzzled by why Richard started
from singleton lists instead of the empty list. The intuition helps to explain that too. Level 0would
be a singleton list/tree, and I wouldn’t know the number of values level 1should contain. That
Page 4:
4 Hsiang-Shang Ko, Shin-Cheng Mu, and Jeremy Gibbons
1
cdtd"a"td"b"td"c"td"d"td"ab"td"ac"td"ad"td"bc"td"bd"td"cd"td"abc"td"abd"td"acd"td"bcd"td"ab", td"ac", td"bc"td"ab", td"ad", td"bd"td"ac", td"ad", td"cd"td"bc", td"bd", td"cd"mapB g . cdmapB glevel 1level 2level 2½level 3
13614234
Fig. 3. How mapB g . cd constructs a new level.
number is the length of the input list, and cddoesn’t get that information. So there isn’t enough
context for going from level 0to level 1, regardless of how levels are represented.
1.3 Rearranging Binomial Trees
That still doesn’t give me much insight into why cdworks though. Presumably, cddoes something
useful only for the trees built by cvt . map f andcditself. What are the constraints on these
trees, and how does cdexploit them?
Richard did give a hint: the sizes [1,2,3,4],[1,3,6], and[1,4]of subtrees along their left spines
(the red numbers in Figure 3) are the diagonals of Pascal’s triangle — the trees are related to binomial
coefficients ! The binomial coefficient 𝐶n
kis the number of ways of choosing 𝑘elements from an
𝑛-list. Indeed, each level 𝑘in the lattice (Figure 2) contains values about 𝑘-sublists. For example,
level 2has𝐶4
2=6values, and there are 6ways of choosing 2elements from a 4-list.
Aha! I can even see a pattern related to the choices in the tree representation of level 2(Figure 3):
the right subtree is about all the 2-sublists that end with 'd', and the left subtree about the other
2-sublists not containing 'd'. To choose 2elements from "abcd" , I can include the rightmost
element 'd'or not. If 'd'is included, there are 𝐶3
1ways of choosing 1element from "abc" to go
with 'd'. If'd'is not included, there are 𝐶3
2ways of choosing 2elements from "abc" . And the
total number of 2-sublists is𝐶3
2+𝐶3
1=𝐶4
2. All the Binnodes fit this pattern. I guess the trees are
supposed to satisfy a binomial shape constraint (and the name of the Bdata type could refer to
‘binomial’ as much as to ‘binary’).
That’s about as many clues as I can get from Richard’s paper for now. Given these clues, how do
I prove that cdindeed does the job — bringing values about related immediate sublists together? In
fact, how do I even write that down as a formal specification? And how does that help me to prove
that tdequals bu?
I’m worried that there will be many complex proofs waiting ahead for me.
2 TYPES
2.1 Shapes in Types
The binomial shape constraint seems to be the easiest next target, because there’s a standard
solution: capturing the tree shape in its type. Shape-indexed data types are so common now that
I’m tempted to say they should count as simple types. They’re common even in Haskell. I prefer a
proper dependently typed language though, so I open my favourite editor, and switch to Agda.
The classic example of shape-indexing is, of course, length-indexed lists (or ‘vectors’):
Page 5:
Binomial Tabulation: A Short Story 5
data Vec :N→Set→Setwhere
[] : Vec zero a
:::a→Vecn a→Vec(sucn)a
(I enjoy writing Agda types these days because I no longer have to quantify over each and every
variable, such as aandnin the type of cons — Agda supports implicit ‘generalisation of declared
variables’ now.) The constructors used in a list of type Vecn aare completely determined by the
length index n. The data type definition could even be understood as if it were performing pattern
matching on the index: if the index is zero, then the list has to be nil; otherwise the index is a suc,
and the list has to start with a cons. (Chapman et al .[2010] did develop a theory where data types
can be defined by pattern matching on indices in this way.)
In the same vein, I write down a shape-indexed version of Richard’s Bdata type (Section 1.3):
data B:N→N→Set→Setwhere
tipz:a →Bn zero a
tips:a →B(suck)(suck)a
bin :Bn(suck)a→Bn k a→B(sucn)(suck)a
The size of a tree of type Bn k a with𝑘≤𝑛is precisely the binomial coefficient 𝐶n
k. Naturally,
there are no inhabitants when 𝑘>𝑛. Like Vec, the indices 𝑛,𝑘determine the constructors. If kis
zero, then the tree is a tipzwith one element ( 𝐶n
0=1). Ifnissuck, then the tree is a tipsalso with
one element ( 𝐶1+k
1+k=1). Otherwise the tree is a bin, and the sizes 𝐶n
1+kand𝐶n
kof the two subtrees
add up to the expected size 𝐶1+n
1+kof the whole tree. The trees are now truly binomial rather than
just binary, formalising Richard’s hint about sizes. I’ll write Bn
kforBn k, by analogy with 𝐶n
k.
And now I can give a more informative type to cd(Section 1):
cd:1≤k→k<n→Bn
ka→Bn
1+k(Vec(1+k)a)
It takes as input the data for level 𝑘out of𝑛levels in the sublist lattice (Figure 2), with 1≤𝑘<𝑛;
these are the solutions for each of the 𝐶n
k𝑘-sublists of the original 𝑛-list. And it returns as output
the components for level 1+k; there are𝐶n
1+kof these, each a(1+k)-list (to be fed into gwhen
used in bu). There are two (greyed out) ‘side conditions’ 1≤kandk<n, which I don’t want to
bother with when I’m thinking at a higher level. I’m going to check these conditions mentally and
then ignore everything related to these conditions — I’ll call cdas if it were a function without the
first two arguments, and skip over cases that are impossible due to the conditions. Agda ensures
that I don’t forget about all the ignored stuff in the final code though.
I continue to transcribe the definition of cdinteractively in Agda.
cd:1≤k→k<n→Bn
ka→Bn
1+k(Vec(1+k)a)
cd(bin(tipsy) ( tipzz) )=tips(y::z::[])
cd(bin(tipsy)u@(bin))=tips(y::unTipB(cdu))
cd(bint@(bin) ( tipzz) )=bin(cdt)(mapB(::(z::[]))t)
cd(bint@(bin)u@(bin))=bin(cdt)(zipBWith ::t(cdu))
In the first case, bin(tipsy)(tipzz), Agda conveniently figures out for me whether a Tipin
the pattern should be a tipsortipz. I expect Agda to fill in the right constructor for the goal
type B2
2(Vec 2a)too, but Agda complains that it cannot decide between tipsandbin. Indeed,
B2
2(Vec 2a)matches the result type of both tipsandbin. But binis actually impossible because its
left subtree would have type B1+k
2+ka, and this type is uninhabited. So the indices of Bstill determine
the constructor, though not as directly as in the case of Vec.
Page 6:
6 Hsiang-Shang Ko, Shin-Cheng Mu, and Jeremy Gibbons
I go through the cases bin(tipsy)uandbint(tipzz)without difficulties, after supplying the
definitions of unTipB:Bn
na→aandmapB:(a→b)→ Bn
ka→Bn
kb. In the final bint ucase,
the result should be a bin, and the left subtree cdtis accepted by Agda. Slightly anxiously, I start
constructing the right subtree. Agda tells me that t:B1+n
2+kaandu:B1+n
1+ka. When I ask what type
cduhas, Agda responds with B1+n
2+k(Vec(2+k)a). That’s the same shape as t, sotandcducan be
safely zipped together using a shape-preserving zipBWith :(a→b→c)→ Bn
ka→Bn
kb→Bn
kc.
I’ve gone through the whole definition! So, as I guessed, the binomial shape constraint holds
throughout cd. What’s nice is that I didn’t need to do much. The type checker took care of most of
the proof, using the indices to keep track of the tree shapes throughout the transcription.
2.2 Properties in Types
So much for the shape. But how do I know that the contents are correct — that cdis correctly
rearranging the values?
The input to cdis a tree of values associated with 𝑘-sublists (for some 1≤𝑘<𝑛), and these
values are rearranged in relation to (1+k)-sublists. These values can have any type a, which is
parametrically quantified in the type of cd. The parametric quantification ensures that cdcannot
do different things to different a’s (because there’s no way to do a case analysis on a). So if I can
specify what cdshould do for a specific choice of a, then cdwill have to do the same thing for
alla’s. Well, I suppose a natural choice is k-sublists themselves. I’ll define Richard’s trees (Figure 3)
but just put k-sublists in them, and then specify that cdshould transform level kto level𝑘1/2.
In Haskell, I suppose Richard might have defined the tree of k-sublists of a list xsaschoose k xs ,
where the function choose is defined by
choose :: Int -> L a -> B (L a)
choose 0 _ = Tip []
choose (k+1) xs | length xs == k+1 = Tip xs
choose (k+1) (xs ++ [x]) = Bin (choose (k+1) xs)
(mapB (++[x]) (choose k xs))
The pattern-matching structure of choose is the same as how Bn
kanalyses its indices (Section 2.1),
except that here I’m working with a list rather than just its length. The function generalises
Richard’s dcthat computes the immediate sublists (Section 1.1): dc xs can be redefined as
flatten (choose (length xs - 1) xs) , where
flatten :: B a -> L a
flatten (Tip x) = [x]
flatten (Bin t u) = flatten t ++ flatten u
Then Richard could have specified cdby
cd (choose k xs) =mapB (flatten . choose k) (choose (k+1) xs) (∗)
Informally: given all the k-sublists of an n-listxs,cdshould rearrange and duplicate them into the
appropriate positions for the (k+1) -sublists, where in the position for a particular (k+1) -sublist,
the result should be the list of all its immediate sublists as computed by flatten . choose k .
I could finish what Richard might have done in his paper by deriving the definition of cdfrom
the specification (∗). Maybe I could switch to Bn
kthroughout to make the shapes clear. But there’s
going to be a large amount of tedious equational reasoning. . . I’m not thrilled by the prospect.
∗ ∗ ∗
Page 7:
Binomial Tabulation: A Short Story 7
My editor is still running Agda and showing the shape-indexed version of cd, with Bn
kin its
type (Section 2.1). The whole point of programming with inductive families [Dybjer 1994] such as
Bn
kis to ‘say more and prove less’: encode more properties in the indices, so that those properties
are automatically taken care of as programs construct and deconstruct indexed data, requiring
fewer manual proofs. Instead of just the shapes, maybe it’s possible to extend Bn
kand encode the
entire specification (∗) ofcdin its type?
What the specification ( ∗) says is basically that cdshould transform a tree produced by choose
into another one also produced by choose and then processed using a mapB . I suppose I could force
a tree to be the result of mapB h (choose k xs) for some h(which is the common form of the
input and output trees of cd) by adding handxsas indices to Bn
k, and imposing equality constraints
on the tree elements:
data B′:(n k :N)(b:Set)→( Veck a→b)→ Vecn a→Setwhere
tipz:(y:b)(e:y≡h[]) → B′n zero b h x𝑠
tips:(y:b)(e:y≡h x𝑠) → B′(suck)(suck)b h x𝑠
bin :B′n(suck)b h x𝑠→B′n k b(h·(x::))x𝑠→B′(sucn)(suck)b h(x::x𝑠)
It’s a rather complex extension of Bn
k, but I think I’ll be fine if I stick to the same programming
methodology: perform ‘pattern matching’ on the indices, and specify what should be in the tree in
each case. In the first case, choose returns Tip [] , so the tree should be a tipz, and its element y
should be accompanied by a proof ethat yequals h[], so that tipzy e‘is’mapB h (Tip []) . The
second case is similar. In the third case, the first thing I do is switch from Richard’s snoc pattern
xs ++ [x] to a cons index x::x𝑠— this just ‘reverses’ the list and shouldn’t break anything,
as long as the snoc in mapB (++[x]) is also switched to a cons to match. The first inductive
call of choose easily translates into the type of the left subtree. The right subtree should be the
result of map h (map (x:) (choose k xs)) . Luckily, the two maps can be fused into a single
map (h . (x:)) . So the type of the second subtree uses the index h·(x::)instead of h.
Even though I sort of derived B′from a specification and know it should work, I still feel an urge
to see with my own eyes that B′does work as intended. So I write a tree with ‘holes’ (missing parts
of a program) at the element positions, and let Agda tell me what types the holes should have:
testB′:{b:Set}{h:Vec 2Char→b}→ B′4
2b h"abcd"
testB′=bin(bin(tips{b}0{?0≡h"cd" }1)
(bin(tips{b}2{?2≡h"bd" }3)(tipz{b}4{?4≡h"bc" }5)))
(bin(bin(tips{b}6{?6≡h"ad" }7)(tipz{b}8{?8≡h"ac" }9))
(tipz{b}10{?10≡h"ab" }11))
The goal types of the even-numbered holes are all b, and the odd-numbered holes require proofs
that the even-numbered holes are equal to h z𝑠for all the 2-sublists z𝑠of"abcd" . It works!
∗ ∗ ∗
B′doesn’t look bad, but I can’t help raising an eyebrow. With yet more effort, I suppose I could
refine the type of cdto use B′and encode the full specification ( ∗). But the refined cdwould need
to manipulate the equality proofs in those trees, and maybe eventually I’d still be doing essentially
the same tedious equational reasoning that I wanted to avoid.
Another problem is that the upgraded cdwould only work on trees of sublists, whereas the
original cdin Haskell works on trees of anytype of values. Indeed, the specification ( ∗) talks about
the behaviour of cdon trees of sublists only. By encoding the specification in the type, I’d actually
restrict cdto trees of sublists. That doesn’t sound too useful.
Page 8:
8 Hsiang-Shang Ko, Shin-Cheng Mu, and Jeremy Gibbons
Still, I can’t take my eyes off the definition of B′. The way it absorbs the definition of choose
looks right. If only the elements weren’t restricted to pairs of the form y:bande:y≡h z𝑠. . .
A lightbulb lights up above my head.
data BT:(n k :N)→( Veck a→Set)→ Vecn a→Setwhere
tipz:p[] →BTn zero p x𝑠
tips:p x𝑠 →BT(suck)(suck)p x𝑠
bin :BTn(suck)p x𝑠→BTn k(p·(x::))x𝑠→BT(sucn)(suck)p(x::x𝑠)
Just generalise the element type! More specifically, generalise that to a type family p:Veck a→Set
indexed by k-sublists. Then Bn
kabecomes a special case by specialising ptoconst a(and supplying
anyn-list as the last index), and similarly B′n
kb h x𝑠by specialising pto𝜆z𝑠→Σ[y∈b]y≡h z𝑠!
I wasn’t expecting this generalisation. After taking a moment to calm down, I look more closely
at this new, unifying data type. The index pinBTreplaces hinB′, and is similarly applied to all
the sublists of a particular length. What’s different is that pis applied to a sublist to get the whole
element type in a tip. So, in general, all the elements in a tree of type BTn
kp x𝑠have distinct types,
which are p y𝑠for all the k-sublists y𝑠of the n-listx𝑠. To see an example:
testBT :{p:Vec 2Char→Set}→ BT4
2p"abcd"
testBT =bin(bin(tips{p"cd" }0)(bin(tips{p"bd" }1)(tipz{p"bc" }2)))
(bin(bin(tips{p"ad" }3)(tipz{p"ac" }4))(tipz{p"ab" }5))
It’s simpler to think of a tree of type BTn
kp x𝑠as a table with all the k-sublists of x𝑠as the keys. For
each key y𝑠, there’s an entry of type p y𝑠. (So the ‘T’ in BTstands for both ‘tree’ and ‘table’.)
This BTdefinition is really intriguing. . . Most likely, there is a way to derive BTfrom choose , and
that’ll work for a whole class of functions. The type of BTn
k:(p:Veck a→Set)→ Vecn a→Set
looks just like a continuation-passing version of some Vecn a{Veck a, which would be the type
of a version of choose that nondeterministically returns a k-sublist of an n-list. And the index p
works like a continuation too. Take the (expanded) type of binfor example:
bin :BTn(suck)(𝜆y𝑠→p y𝑠) x𝑠
→BTn k(𝜆z𝑠→p(x::z𝑠))x𝑠→BT(sucn)(suck)p(x::x𝑠)
I can read it as ‘to compute a (1+k)-sublist of x::x𝑠and pass it to continuation p, either compute
a(1+k)-sublist y𝑠ofx𝑠and pass y𝑠topdirectly, or compute a k-sublist z𝑠ofx𝑠and pass x::z𝑠
top’. All the results from pare then collected in a tree as the indices of the element types. A simpler
and familiar example (which can be found in the Agda standard library) is
data All:(a→Set)→ Vecn a→Setwhere
[] : Allp[]
:::p x→Allp x𝑠→Allp(x::x𝑠)
This should be derivable from the function that nondeterministically returns an element of a list.
I’m onto something general — maybe it’s interesting enough for a research paper!
2.3 Specifications as Types
That paper will have to wait though. I’ve still got a problem to solve: how do I use BTto specify cd?
What’s special about BTis that the element types are indexed by sublists, so I know from the type
of an element which sublist it is associated with. That is, I can now directly say ‘values associated
with sublists’ and rearrange these values, rather than indirectly specify the rearrangement in terms
of sublists and then extend to other types of values through parametricity. BTn
kp x𝑠is the type
of a tree of p-typed values associated with the k-sublists of x𝑠, and that’s precisely the intended
Page 9:
Binomial Tabulation: A Short Story 9
meaning of cd’s input. What about the output? It should tabulate the (1+k)-sublists of x𝑠, so the
type should be BTn
1+kq x𝑠for some q:Vec(1+k)a→Set. For each sublist y𝑠:Vec(1+k)a,
I want a list of p-typed values associated with the immediate sublists of y𝑠, which are k-sublists.
Or, instead of a list, I can just use a tree of type BT1+k
kp y𝑠. Therefore the whole type is
retabulate :k<n→BTn
kp x𝑠→BTn
1+k(BT1+k
kp)x𝑠
which is parametric in p(so, like the Haskell version of cd, the elements can have any types). I think
it’s time to rename cdto something more meaningful, and decide to use ‘ retabulate ’ because I’m
moving values in a table into appropriate positions in a new (nested) table with a new tabulation
scheme. And a side condition k<nis needed to guarantee that the output shape BTn
1+kis valid.
The type of retabulate looks like a sensible refinement of the type of cd, except that I’m letting
retabulate return a tree of trees, rather than a tree of lists. Could that change be too drastic?
Hm.. .actually, no — the shape of BT1+k
kis always a (nonempty) list! If kiszero, aBT1
0-tree has to
be a tipz. Otherwise, a BT2+k
1+k-tree has to take the form bin(tipsy)t. This expression is in fact a
cons-like operation:
::BT :p x𝑠→BT1+k
k(p·(x::))x𝑠→BT2+k
1+kp(x::x𝑠)
y::BTt=bin(tipsy)t
To construct a table indexed by all the immediate sublists of x::x𝑠, I need an entry for x𝑠, the
immediate sublist without x, and a table of entries for all the other immediate sublists, which are
x::w𝑠for all the immediate sublists w𝑠ofx𝑠.
I go on to define retabulate . Its type is much more informative than that of cd. Rather than
transcribing cd, can I use the type of retabulate to guide me through the implementation? I type the
left-hand side into the editor, leave the right-hand side as a hole, and perform some case splitting
on the input tree:
retabulate(tipz) ={ }0
retabulate(tips) ={ }1
retabulate(bin(tips))={ }2
retabulate(bin(bin) ( tipz) )={ }3
retabulate(bin(bin) ( tips) )={ }4
retabulate(bint@(bin)u@(bin))={BT2+n
3+k(BT3+k
2+kp(x::x1::x𝑠))}5
The cases for tipsandbin(tips)can be eliminated immediately since the side condition
k<nis violated. I go straight to the last and the most difficult case, bint u, where tanduare both
constructed by bin. Their types are
t:BT1+n
2+kp(x1::x𝑠)
u:BT1+n
1+k(p·(x::))(x1::x𝑠)
Neither of them have the right shape to be used immediately, so in { }5I try starting with a bin:
retabulate(bint@(bin)u@(bin))=bin{BT1+n
3+k(BT3+k
2+kp)(x1::x𝑠)}6
{BT1+n
2+k(BT3+k
2+kp·(x::))(x1::x𝑠)}7
{ }6is directly fulfilled by the induction hypothesis retabulate t! That’s a good sign.
What can I put in { }7? Prompted by the success with { }6, I try the induction hypothesis for u:
retabulate u:BT1+n
2+k(BT2+k
1+k(p·(x::)))( x1::x𝑠)
Hm. Its type has the same outer shape BT1+n
2+k(x1::x𝑠)that I want in the goal type, but the
element types don’t match. . .
Page 10:
10 Hsiang-Shang Ko, Shin-Cheng Mu, and Jeremy Gibbons
To fill out { }7I really have to pay more attention to what the types say. I stare at the types,
and, slowly, they start to make sense.
•The outer shape BT1+n
2+k(x1::x𝑠)tells me that I’m dealing with tables indexed by the (2+k)-
sublists z𝑠ofx1::x𝑠.
•For each z𝑠, I need to construct a table of p-typed entries indexed by all the immediate sublists
ofx::z𝑠, because that’s what the element types BT3+k
2+kp·(x::)in the goal type mean.
•What do I have in retabulate u? I have a table of entries indexed by x::w𝑠for all the immediate
sublists w𝑠ofz𝑠inretabulate u— that’s what the element types BT2+k
1+k(p·(x::))mean.
•What’s the relationship between these sublists x::w𝑠and the table I need to construct, which is
indexed by the immediate sublists of x::z𝑠? Oh, right, the sublists x::w𝑠are the immediate
sublists of x::z𝑠with the first element x! So I’ve already got most of the entries I need.
•I’m still missing an entry for the immediate sublist of x::z𝑠without x, which is z𝑠. Do I have
that? I search through the context. The type of tdraws my attention: it has the familiar outer
shape BT1+n
2+k(x1::x𝑠). What entries are in t? Its type tells me that there’s an entry for each
(2+k)-sublist z𝑠ofx1::x𝑠. That’s precisely what I’m missing!
So, for each z𝑠, I can construct a table indexed by all the immediate sublists of x::z𝑠by combining an
entry for z𝑠(the immediate sublist without x) from twith a table of entries for the other immediate
sublists with xfrom retabulate u. An entry and a table of entries — aren’t they exactly the arguments
of::BT? Indeed, I can fulfil { }7by combining all the corresponding entries in tandretabulate u
(that share the same index z𝑠) using ::BT, that is, zipBTWith ::BTt(retabulate u)!
The rest of the cases are much easier, and I come up with a definition of retabulate ,
retabulate :k<n→BTn
kp x𝑠→BTn
1+k(BT1+k
kp)x𝑠
retabulate{x𝑠= ::[]}(tipzy) =tips(tipzy)
retabulate{x𝑠= ::::}(tipzy) =bin(retabulate(tipzy))(tipz(tipzy))
retabulate(bin(tipsy)u)=tips(y::BTu)
retabulate(bint@(bin) ( tipzz) )=bin(retabulate t)(mapBT(::BT(tipzz))t)
retabulate(bint@(bin)u@(bin))=bin(retabulate t)
(zipBTWith ::BTt(retabulate u))
where the map and zip functions are the expected ones:
mapBT :(∀{y𝑠}→ p y𝑠→q y𝑠)→∀{ x𝑠}→ BTn
kp x𝑠→BTn
kq x𝑠
zipBTWith :(∀{y𝑠}→ p y𝑠→q y𝑠→r y𝑠)
→ ∀{ x𝑠}→ BTn
kp x𝑠→BTn
kq x𝑠→BTn
kr x𝑠
Amazingly, the more informative type of retabulate did help me to develop its definition. As
I filled in the holes, I didn’t feel I had much of a choice — in a good way, because that reflected
the precision of the type. Furthermore, I discovered a new presentation that varies slightly from
Richard’s cd! The first two cases of cdare subsumed by the third case, bin(tipsy)u, ofretabulate .
The second case of cdrecursively traverses the given tree to convert it to a list, which is not needed
inretabulate , because it yields a tree of trees. Therefore the first two cases of cdcan be unified into
one. I forgot to include the side condition 1≤kinretabulate , but that leads to two new tipzcases
instead of preventing me from completing the definition. Whereas cdhas to start from level 1of
the sublist lattice (Figure 2), this pair of cases of retabulate is capable of producing a level- 1table
(with as many elements as x𝑠) from a level- 0table, which is a tipz. This is due to x𝑠now being
available as an index, providing the missing context for retabulate .
In fact, looking at the type more closely, I suspect that the extensional behaviour of retabulate is
completely determined by the type (so the type works as a nice and tight specification): the shape
Page 11:
Binomial Tabulation: A Short Story 11
of the output table is completely determined by the indices; moreover, all the input elements have
distinct types in general, so each element in the output table has to be the only input element with
the required type — there is no choice to make. Formally, the proof will most likely be based on
parametricity (and might be similar to Voigtländer’s [2009]). That’ll probably be a fun exercise. . . but
I’ll leave that for another day.
2.4 Precision of Types
Right now I’m more eager to understand why the bottom-up algorithm buequals the top-down
td(Sections 1.1 and 1.2). Will dependent types continue to be helpful? I should try and find out by
transcribing the two algorithms into Agda too.
The first thing to do is make the type of the two algorithms as precise as the type of retabulate .
I start from the combining function g. Its type L s -> s has been making me shudder involuntarily
whenever I see it: it says so little about what gshould do. The intention — that gshould compute
the solution for a list from those of its immediate sublists — is nowhere to be seen.
But now I have the right vocabulary to state the intention precisely in Agda. I can use BTto
quantify over all sublists of a particular length. And to say ‘a solution for a list’ (instead of just ‘a
solution’) I should switch from a type to a type family
s:∀{k}→ Veck a→Set
such that s y𝑠is the type of solutions for y𝑠. So
✘g:∀{k}→{ y𝑠:Vec(2+k)a}→ BT2+k
1+ks y𝑠→s y𝑠
I look at the type with a satisfied smile — now that’s what I call a nice and informative type! It says
concisely and precisely what gshould do: compute a solution for any y𝑠:Vec(2+k)afrom a
table of solutions for all the length- (1+k)(that is, immediate) sublists of y𝑠.
The smile quickly turns into a frown though. I still don’t feel comfortable with BT2+k
1+k. The indices
are apparently not the most general ones — why not BT1+k
k?
I delete ( ✘) the type of gand start pondering. I wrote BT2+k
1+kin that type because that was what
Richard wanted to say. Richard used singleton lists as the base cases instead of the empty list, so
gwas applied to solutions for sublists of length at least 1, hence the subscript 1+k. But the most
general type
g:∀{k}→{ y𝑠:Vec(1+k)a}→ BT1+k
ks y𝑠→s y𝑠
looks just fine. In particular, when kis0, the type says that gshould compute a solution for a
singleton list from a solution for the empty list (the only immediate sublist of a singleton list),
which seems reasonable. . .
. . . And indeed it is reasonable!
When I discovered the extra tipzcases of retabulate (Section 2.3), I saw that it may be possible
to start from level 0 of the sublist lattice (Figure 2) after all. Now it’s confirmed. Instead of starting
with solutions for singleton lists, I can start with a given solution for the empty list
✘e:s[]
at level 0, and work upwards using g. There’s no problem going from level 0 to level 1, because
there’s now additional context in the indices so that gknows for which singleton list a solution
should be computed. Making types precise has helped me to find a more natural and general form
of recursive computation over immediate sublists!
Page 12:
12 Hsiang-Shang Ko, Shin-Cheng Mu, and Jeremy Gibbons
And it’s not just any recursive computation — it’s now an alternative induction principle for lists.
The base case eis still about the empty list, and the inductive case gassumes that the induction
hypothesis holds for all the immediate sublists. (I guess I’ve been instinctively drawn towards
induction principles, in common with most dependently typed programmers.)
✘ImmediateSublistInduction :Set 1
ImmediateSublistInduction =
{a:Set}(s:∀{k}→ Veck a→Set)
(e:s[])
(g:∀{k}→{ y𝑠:Vec(1+k)a}→ BT1+k
ks y𝑠→s y𝑠)
{n:N} (x𝑠:Vecn a)→ s x𝑠
∗ ∗ ∗
ImmediateSublistInduction looks very nice, but I’m still worried: will it be possible to transcribe
tdandbufor this type easily, that is, without ugly stuff like type conversions ( subst ,rewrite , etc)?
Sadly, there may never be any theory that tells me quickly whether or not a type admits pretty
programs. The only way to find out is to try writing some. I start transcribing td(Section 1.1).
The only component for which I still don’t have a dependently typed version is dc, which I’ve
generalised to choose (Section 2.3). Now I can give it a precise type:
choose :(n k :N)→ k≤↑n→(x𝑠:Vecn a)→ BTn
kExactly x𝑠
The key ingredient is the BTn
kin the result type, which tabulates all the k-sublists as the indices of
the element types. I just need to plug in this data type
data Exactly :a→Setwhere
exactly :(x:a)→ Exactly x
to say that the elements in the resulting table should be exactly the tabulated indices. In contrast to
the Haskell version, I need to make the Agda version of choose total by saying explicitly that the
length nof the list x𝑠is at least k, so that there are enough elements to choose from. Somewhat
notoriously, there are many versions of natural number inequality. To align with the inductive
structure of choose , I pick the data type m≤↑nwhere mremains fixed throughout the definition
and serves as an ‘origin’, and an inhabitant of m≤↑nis the distance (which is essentially a natural
number) that nis away from the origin m:
data≤↑:N→N→Setwhere
zero : m≤↑m
suc :m≤↑n→m≤↑sucn
Given the precise type, transcribing choose is pretty much straightforward:
choose :(n k :N)→ k≤↑n→(x𝑠:Vecn a)→ BTn
kExactly x𝑠
choose zero =tipz(exactly [])
choose(suck)(suck)zero x𝑠 =tips(exactly x𝑠)
choose(sucn)(suck)(sucd)(x::x𝑠)=
bin(choose n(suck)d x𝑠)(mapBT(mapExactly(x::))(choose n k(incr d)x𝑠))
--mapExactly :(f:a→b)→{ x:a}→ Exactly x→Exactly(f x)
The function performs an induction on k, like the Haskell version. The second and third cases are
an inner induction on the distance that nis away from suck. In the second case the distance is
zero, meaning that nis (at the origin) suck, sox𝑠has the right length and can be directly returned.
Page 13:
Binomial Tabulation: A Short Story 13
Otherwise the distance is sucdin the third case, where the first inductive call is on d, and the
second inductive call is on kwhile the distance is unchanged, but the type suck≤↑sucnneeds to
be adjusted to k≤↑n(by invoking incr :sucm≤↑n→m≤↑nond).
∗ ∗ ∗
I step back and take another look at choose . There’s one thing that bothers me: Exactly xis a type
that has a unique inhabitant, so I could’ve used the unit type ⊤as the element types instead, and
I’d still give the same amount of information, which is none! That doesn’t make a lot of sense —
I thought I was computing all the k-sublists and returning them in a table, but somehow those
sublists didn’t really matter, and I could just return a blank table of type BTn
k(const⊤)x𝑠. . . ?
Hold on, it’s actually making sense. . .
It’s because all the information is already in the table structure of BT. Indeed, I can write
mapBT(𝜆{{y𝑠}tt→exactly y𝑠}):BTn
k(const⊤)x𝑠→BTn
kExactly x𝑠
to recover a table of Exactly s from just a blank table by replacing every tt(the unique inhabitant
of⊤) with the index y𝑠there. What choose does is not really compute the sublists — BThas already
‘computed’ them. Instead, choose merely affirms that there is a table indexed by all the k-sublists
of an n-list whenever k≤↑n. The elements in the table don’t matter, and might as well be tt.
So, instead of choose , I can use
✘blank :(n k :N)→ k≤↑n→{ x𝑠:Vecn a}→ BTn
k(const⊤)x𝑠
blank zero =tipztt
blank(suck)(suck)zero =tipstt
blank(sucn)(suck)(sucd){ ::}=bin(blank n(suck)d)(blank n k(incr d))
to construct a blank table indexed by all the immediate sublists in the inductive case of td, where
I’ll then compute and fill in solutions for all the immediate sublists by invoking tdinductively, and
finally invoke gto combine all those solutions. And the base case simply returns e.
✘td:ImmediateSublistInduction
tds e g{zero}[]=e
tds e g{sucn}x𝑠=g(mapBT(𝜆{{y𝑠}tt→tds e g{n}y𝑠})(blank1+n
n(suc zero)))
I look aghast at the monster I’ve created. Sure, the definition type-checks, but oh my. . . it’s terribly
ugly. The problems are cosmetic though, and should be easy to fix. (1) The induction is on n, which
shouldn’t have been an implicit argument. (2) In the base case, I have to match x𝑠with []to make
it type-correct to return e, but that could’ve been avoided if I set e:{x𝑠:Vec 0a}→ s x𝑠. (3) In
the inductive case, x𝑠doesn’t need to be explicit because it’s passed around only implicitly in the
indices on the right-hand side. (4) I can get rid of the 𝜆around the inductive call to tdif I make y𝑠
implicit and add a dummy ⊤argument. In fact, if I add a dummy ⊤argument to eandblank as
well, I can make the definition point-free like in Richard’s paper — a temptation I cannot resist. So I
revise the induction principle,
ImmediateSublistInduction :Set 1
ImmediateSublistInduction =
{a:Set}(s:∀{k}→ Veck a→Set)
(e:{y𝑠:Vec 0a}→⊤→ s y𝑠)
(g:∀{k}→{ y𝑠:Vec(1+k)a}→ BT1+k
ks y𝑠→s y𝑠)
(n:N){x𝑠:Vecn a}→⊤→ s x𝑠
Page 14:
14 Hsiang-Shang Ko, Shin-Cheng Mu, and Jeremy Gibbons
add the dummy⊤argument to blank (also ignoring the inequality argument from now on),
blank :(n k :N)→ k≤↑n→{ x𝑠:Vecn a}→⊤→ BTn
k(const⊤)x𝑠
and get my point-free td:
td:ImmediateSublistInduction
tds e g zero =e
tds e g(sucn)=g·mapBT(tds e g n)·blank1+n
n
The revised ImmediateSublistInduction may not be too user-friendly, but that can be amended
later (when there’s actually a user).
∗ ∗ ∗
And it’d be wonderful if the revised ImmediateSublistInduction worked for butoo! I proceed to
transcribe bu(Section 1.2):
bu:ImmediateSublistInduction
bus e g n =unTip·loop 0{0↓≤n}0·mapBTe·blankn
0
where loop :(k:N)→ k↓≤n→BTn
ks x𝑠→BTn
ns x𝑠
loop nzero =id
loop k(sucd)=loop(1+k)d·mapBTg·retabulate
I construct the initial table by reusing blank to create a blank level- 0table and using mapBTe
to fill in the initial solution for the empty list. Then the loop function increases the level to nby
repeatedly retabulating a level- ktable as a level-(1+k)table and filling in solutions for all the
length-(1+k)sublists using mapBTg. Finally, a solution for the whole input list is extracted from
the level- ntable using
unTip :BTn
np x𝑠→p x𝑠
unTip(tipsp)=p
unTip{x𝑠=[]}(tipzp)=p
Thebincase is impossible and ignored. (Hm, retabulate andunTip smell comonadic, and maybe
the indices constitute a grading [Gaboardi et al. 2016]. . . but I can’t get distracted now.)
The argument/counter kofloop should satisfy the invariant k↓≤n. Again, this version of natural
number inequality is chosen to align with the inductive structure of loop. The data type m↓≤nis
dual to≤↑in the sense that this time it is nthat is fixed throughout the definition, and mmoves
away from n:
data↓≤ :N→N→Setwhere
zero : n↓≤n
suc :sucm↓≤n→m↓≤n
Then loop simply performs induction on the distance k↓≤n; the counter kgoes up as the
distance decreases in inductive calls, and eventually reaches nwhen the distance becomes zero.
The remaining {0↓≤n}0is actually nontrivial, but the Agda standard library covers that.
2.5 Equality from Types
Okay, I’ve made the type of both tdandbuprecise. How does this help me prove tdequals bu?
The definitions still look rather different except for their type. . .
. . . And the type is an induction principle.
Is it possible to have extensionally different implementations of an induction principle?
Page 15:
Binomial Tabulation: A Short Story 15
Let me think about the induction principle of natural numbers.
N-Induction :Set 1
N-Induction =(p:N→Set)(pz:pzero)(ps:∀{m}→ p m→p(sucm))
(n:N)→ p n
ind :N-Induction
indp pz ps zero =pz
indp pz ps(sucn)=ps(indp pz ps n)
The motive pis parametrically quantified, so a proof of p nhas to be napplications of pstopz.
There are intensionally different ways to construct that ( indversus a tail-recursive implementation,
for example), but extensionally they’re all the same.
Of course, parametricity is needed to prove that formally. I look up Bernardy et al .’s [2012]
translation, which (after a bit of simplification) gives the following statement:
N-Induction-unary-parametricity :N-Induction→Set 1
N-Induction-unary-parametricity f=
{p:N→Set} ( q:∀{m}→ p m→Set)
{pz:pzero} ( qz:q pz)
{ps:∀{m}→ p m→p(sucm)}(qs:∀{m}{x:p m}→ q x→q(ps x))
{n:N}→ q(f p pz ps n)
Unary parametricity can be thought of as adding an invariant ( q) to a parametrically quantified
type or type family; this invariant is assumed to hold for any first-order input ( qz) and be preserved
by any higher-order input ( qs), and is guaranteed to hold for the output. Now choose the invariant
that any proof of p mis equal to the one produced by indp pz ps m , and that’s it:
N-Induction-uniqueness-from-parametricity :
(f:N-Induction)→N-Induction-unary-parametricity f
→(p:N→Set)(pz:pzero)(ps:∀{m}→ p m→p(sucm))(n:N)
→f p pz ps n≡indp pz ps n
N-Induction-uniqueness-from-parametricity f param p pz ps n =
param(𝜆{m}x→x≡indp pz ps m)refl(cong ps)
--refl :{x:a}→ x≡x;cong :(f:a→b)→{ x y :a}→ x≡y→f x≡f y
The same argument works for ImmediateSublistInduction — any function of the type satisfying
unary parametricity is pointwise equal to td. I finish the Agda proofs for both induction principles
in a dreamlike state.
Yeah, I have a proof that tdequals bu.
Well, strictly speaking I don’t have one yet. (Vanilla) Agda doesn’t have internal parametric-
ity [Van Muylder et al .2024], so I’d need to prove the parametricity of bu, painfully. But there
shouldn’t be any surprise.
Somehow I feel empty though. I was expecting a more traditional proof based on equational
reasoning. This kind of proof may require more work, but allows me to compare what tdandbu
dointensionally . That’s an aspect overlooked from the parametricity perspective. Despite having
a proof now, I think I’m going to have to delve into the definitions of tdandbuanyway, to get a
clearer picture of their relationship.
Page 16:
16 Hsiang-Shang Ko, Shin-Cheng Mu, and Jeremy Gibbons
3 DIAGRAMS
Another hint Richard left was ‘naturality’, a category-theoretic notion which he used a lot in his
paper. In functional programming, naturality usually stems from parametric polymorphism: all
parametric functions, such as cdandunTip , satisfy naturality. I’ve got some parametric functions
too, such as retabulate andunTip . Their dependent function types with all the indices are more
advanced than Richard’s types though, and the simply typed form of naturality Richard used no
longer makes sense. But one nice thing about category theory is its adaptability — all I need to
figure out is which category I’m in, and then I’ll be able to work out what naturality means for my
functions systematically within the world of category theory.
And, if the key is naturality, now I have an additional tool that Richard didn’t: string diagrams. I’ve
seen how dramatically string diagrams simplify proofs using naturality, so it’s probably worthwhile
to take a look at the two algorithms from a string-diagrammatic perspective.
But before I get to string diagrams, I need to work through some basic category theory. . .
3.1 From Categories to String Diagrams
Functional programmers are familiar with types and functions, and know when functions can
be composed sequentially — when adjacent functions meet at the same type. And it’s possible
to compose an empty sequence of functions, in which case the result is the identity function.
Categories are settings in which the same intuition about sequential composition works. Instead
of types and functions, the categorical programmer can switch to work with some objects and
morphisms specified by a category, where each morphism is labelled with a source object and a
target object (like the source and target types of a function), and morphisms can be composed
sequentially when adjacent morphisms meet at the same object. And, like identity functions, there
are identity morphisms too. Working in a new setting that’s identified as a category is a blessing for
the functional programmer: it means that the programmer can still rely on some of their intuitions
about types and functions to navigate in the new setting. More importantly, some notions that
prove to be useful in functional programming (such as naturality) can be defined generically on
categories and systematically transported to other settings.
A clue about the kind of category I’m in is that I’m tempted to say ‘ retabulate transforms a tree of
p’s to a tree of trees of p’s’. When a simply typed functional programmer says ‘a tree of something’,
that ‘something’ is a type, that is, an object in the familiar category of types and functions. But here
pis not a type. It’s a type family. So I’ve landed in a different kind of category where the objects
are type families.
There are quite a few versions of ‘categories of families’. I go through the types of the components
used in the algorithms (Section 2.4) to find a common form, and it seems that the simplest version
suffices: given an index type a:Set, a category of families Fam ahas objects of type
Fam :Set→Set 1
Fam a=a→Set
and morphisms of type
⇒ :Fam a→Fam a→Set
p⇒q=∀{x}→ p x→q x
That is, a morphism from ptoqis a family of functions between corresponding types (with the
same index) in pandq. Everything in the definition is parametrised by the index type a, so actually
I’m working in not just one but many related categories of families, with different index types.
These categories are still inherently types and functions, so it’s no surprise that their sequential
composition works in the way familiar to the functional programmer.
Page 17:
Binomial Tabulation: A Short Story 17
With the definition of Fam , now I can rewrite the parametric function types of retabulate and
unTip to look more like the ones in Haskell:
retabulate :BTn
kp⇒BTn
1+k(BT1+k
kp)
unTip :BTn
np⇒p
I can fit blankn
kinto Fam(Vecn a)by lifting its⊤argument to a type family const⊤(that is, an
object of the category):
blankn
k:const⊤⇒BTn
k(const⊤)
The base and inductive cases of ImmediateSublistInduction fit into these Fam categories too: given
a:Setands:∀{k}→ Fam(Veck a), I can write
g:BT1+k
ks⇒s
e:const⊤⇒s{0}
(It’s important to say explicitly that the target of eiss{0}:Fam(Vec 0a)to make it clear that
egives a solution for the empty list.)
∗ ∗ ∗
I haven’t done much really. It’s just a bit of abstraction that hides part of the indices, and might
even be described as cosmetic. What’s important is that, by fitting my programs into the Fam
categories, I can start talking about them in categorical language. In particular, I want to talk about
naturality. That means I should look for functors andnatural transformations in my programs.
A parametric data type such as BTn
kis categorically the object part of a functor , which maps
objects in a category to objects in a possibly different category. In the case of BTn
k, the functor goes
from Fam(Veck a)toFam(Vecn a)— indeed I can rewrite the type of BTn
kas
BTn
k:Fam(Veck a)→ Fam(Vecn a)
TheBT-typed trees are made up of the constructors of BTand hold elements of types p. A categorical
insight is that the constructors constitute an independent layer of data added by the functor outside
the elements. The independence of this functor layer is described formally by the definitions of
functors and natural transformations.
One aspect of this independence is that the functor layer can stay the same and impervious to
whatever is happening at the inner layer. Categorically, ‘whatever is happening’ means an arbitrary
morphism. In the case of BT, the inner layer (the elements) may be changed by some arbitrary
morphism of type p⇒q, and that can always be lifted to a morphism of type BTn
kp⇒BTn
kq
that doesn’t change the functor layer (the tree constructors). This lifting is the morphism part of a
functor, and is the ‘map’ function that comes with any (normal) parametric data type. I’ve already
had a map function for BT, and indeed its type can be rewritten as
mapBT:(p⇒q)→( BTn
kp⇒BTn
kq)
In a sense, a lifted morphism such as mapBTfis essentially just fsince mapBTfdoes nothing
to the functor layer. So when fis a composition, that composition shows up at the level of lifted
morphisms too. Formally, this is stated as a functoriality equation:
mapBT(f′·f)=mapBTf′·mapBTf
(Also mapBTid=idin the degenerate case of composing no morphisms.)
The functor layer may also be changed by natural transformations independently of whatever is
happening at the inner layer. In Fam categories, a natural transformation has type ∀{p}→ F p⇒
G pfor some functors FandG, and transforms an F-layer to a G-layer without changing the inner
Page 18:
18 Hsiang-Shang Ko, Shin-Cheng Mu, and Jeremy Gibbons
layer p, whatever pis. For example, retabulate transforms the functor layer BTn
kto acomposition of
functors BTn
1+k·BT1+k
k(which can be regarded as two functor layers) without changing p. Indeed,
retabulate transforms only the tree constructors and doesn’t change the elements to something else.
Moreover, this transformation of the functor layer does not interfere with whatever is happening
at the inner layer. Again ‘whatever is happening’ amounts to a quantification over all morphisms:
for any f:p⇒qhappening at the inner layer, if retabulate is happening at the functor layer
too, it doesn’t make a difference whether forretabulate happens first, because they happen at
independent layers. Formally, this is stated as a naturality equation (where fneeds to be lifted
appropriately):
retabulate ·mapBTf=mapBT(mapBTf)·retabulate
∗ ∗ ∗
With functor composition, in general there can be many functor layers in an object (like the target
ofretabulate ), and all these layers can be transformed independently by natural transformations.
The best way of managing this structure is to use string diagrams . In string diagrams, functors
are drawn as wires, and natural transformations are drawn as dots with input functors/wires
attached below and output functors/wires above. (I learned string diagrams mainly from Coecke
and Kissinger [2017], so my string diagrams have inputs below and outputs on top.) The natural
transformations I’ve got are retabulate andunTip , and I can draw their types as
BTn
1+kBT1+k
k
BTn
kBTn
nretabulate unTip
String diagrams focus on the functor layers and represent them explicitly as a bunch of wires —
functor composition is represented as juxtaposition of wires, and the identity functor is omitted
(it is drawn as no wires). As a string diagram, retabulate has one input wire labelled BTn
kand two
output wires BTn
1+kandBT1+k
k, since it transforms a BTn
klayer to two layers BTn
1+k·BT1+k
k. The
diagram of unTip goes from one wire to none, since unTip transforms BTn
nto the identity functor.
Indeed, what unTip does is get rid of the tipzortipsconstructor.
G
FH
𝛼𝛽Whereas functor composition is arranged horizontally, sequential composition of
natural transformations goes vertically. Given transformations 𝛼:∀{p}→ F p⇒G p
and𝛽:∀{p}→ G p⇒H p, their sequential composition 𝛽·𝛼:∀{p}→ F p⇒H p
is drawn in a string diagram as 𝛼and𝛽juxtaposed vertically and sharing the middle wire
with label G(obscuring a section of the wire).
The power of string diagrams becomes evident when things happen in both the horizon-
tal and vertical dimensions. For example, suppose there are two layers FandF′, where the
outer layer Fshould be transformed by 𝛼and the inner layer F′by𝛼′:∀{p}→ F′p⇒
G′p. There are two ways of doing this: either mapG𝛼′·𝛼, where the outer layer Fis
transformed to Gfirst, or𝛼·mapF𝛼′, where the inner layer F′is transformed to G′first. The two
ways are equal by naturality of 𝛼, but the equality can be seen more directly with string diagrams:
𝛼𝛼′𝛼
𝛼′
FG
FG
=
F′G′
F′G′
Page 19:
Binomial Tabulation: A Short Story 19
tds e g 3=g·
mapBT(g·
mapBT(g·
mapBTe·
blank1
0)·
blank2
1)·
blank3
2
⊤⊤ BT3
2⊤ BT2
1⊤ BT1
0
blank1
0
blank2
1
blank3
2ssss
ggg
e
Fig. 4. A special case of the top-down algorithm as a string diagram.
Themap means skipping over the outer/left functor and transforming the inner/right functor; so in
the diagrams, 𝛼′is applied to the inner/right wire. (I’ve added dashed lines to emphasise that both
diagrams are constructed as the sequential composition of two transformations.) By placing layers
of functors in a separate dimension, it’s much easier to see which layers are being transformed, and
determine whether two sequentially composed transformations are in fact applied independently,
so that their order of application can be swapped. This is abstracted as a diagrammatic reasoning
principle: dots in a diagram can be moved upwards or downwards, possibly changing their vertical
positions relative to other dots (while stretching or shrinking the wires, which can be thought of as
elastic strings), and the (extensional) meaning of the diagram will remain the same.
∗ ∗ ∗
I want to draw tdandbuas string diagrams. However, some of their components, namely blank ,e,
andg, are not natural transformations. Technically, only natural transformations can go into string
diagrams. But I’m still tempted to draw those components intuitively as
BT1+k
kss
g e
⊤s
⊤⊤ BTn
k
blankn
k
After a bit of thought, I come up with some technical justification. Any morphism f:p⇒qcan be
lifted to have the type ∀{r}→( const p)r⇒(const q)r, and become a natural transformation
Page 20:
20 Hsiang-Shang Ko, Shin-Cheng Mu, and Jeremy Gibbons
tds e g 3
={- definition -}
g·mapBT(g·mapBT(g·mapBTe·blank1
0)·blank2
1)·blank3
2
={- functoriality -}
g·mapBT(g·mapBT(g·mapBTe)·mapBTblank1
0·blank2
1)·blank3
2
={- functoriality -}
g·mapBT(g·mapBT(g·mapBTe))·
mapBT(mapBTblank1
0·blank2
1)·blank3
2
Fig. 5. Rewriting td s e g 3into two phases using functoriality.
from const ptoconst q. It’s fine to leave the lifting implicit and just write pandqfor wire labels,
since it’s usually clear that pandqare not functors and need to be lifted. For example, sis a type
family, which is an object in a Fam category, and needs to be lifted to const sto be a functor. For ⊤
there’s one more step: ⊤abbreviates the type family const⊤, which is an object in a Fam category,
and needs to be further lifted to const(const⊤)to be a functor. It’s kind of technical, but in the
end these diagrams are okay.
3.2 Diagrammatic Reasoning
All the abstract nonsense took me some time. But I still don’t know whether string diagrams will
actually help me to understand the two algorithms (Section 2.4). It’s time to find out.
I’m not confident enough to work with the full recursive definitions straight away, so I take the
special case tds e g 3of the top-down algorithm and unfold it into a deeply nested expression
g·mapBT(...)·blank3
2(as on the left of Figure 4). The rightmost component blank3
2has type
const⊤⇒BT3
2(const⊤), which — after eliding the const s, as I’ve just decided to do — is drawn
as the bottom Y-junction in the string diagram (as on the right of Figure 4), transforming the input
⊤-wire at the bottom into two wires BT3
2and⊤. Then the mapBTmeans that the left wire BT3
2is
skipped over and unchanged. The right ⊤-wire continues to be transformed by blank2
1and so on,
and eventually becomes an s-wire. Finally, I apply gto the BT3
2-wire I skipped over and the s-wire
to produce the output s-wire at the top.
I step back and compare the expression and the diagram (Figure 4). All the mapBTs are gone in
the diagram, because I can directly apply a transformation to the intended layers/wires, rather
than count awkwardly how many outer layers I have to skip, using mapBTone layer at a time.
Functoriality is also transparent in the diagram, so it’s slightly easier to see that tdhas two phases
(which I have separated by a dashed line): the first phase constructs deeply nested blank tables, and
the second phase fills and demolishes the tables inside out.
Functoriality is already somewhat transparent in the traditional expression though, thanks to
the infix notation of function composition. So I suppose I don’t absolutely need the string diagram
to see that tdhas two phases, although the required rewriting (Figure 5) is not as perspicuous as
just seeing the two phases in the diagram. Moreover, there’s nothing I can meaningfully move in
the diagram — all the transformations here are lifted after all.
Hm. Maybe I’ll have more luck with the bottom-up algorithm, which has ‘real’ natural trans-
formations? I go on to expand bus e g 3. The loop in the expression unfolds into a sequence of
functions, alternating between retabulate andmapBTg.
‘A sequence. . . ’ I mutter. I shouldn’t have expected anything else from unfolding a loop. But the
sequential structure is so different from the deeply nested structure of td.
Page 21:
Binomial Tabulation: A Short Story 21
bus e g 3=unTip·
mapBTg·
retabulate·
mapBTg·
retabulate·
mapBTg·
retabulate·
mapBTe·
blank3
0
⊤⊤ BT3
0BT1
0BT3
1BT2
1BT3
2
retabulate
retabulate
blank3
0ssss
ggg
BT3
2BT3
3
retabulateunTip
e
Fig. 6. A special case of the bottom-up algorithm as a string diagram.
And then, something unexpected yet familiar appears in the transcribed diagram (Figure 6).
There are also two phases for table construction and demolition, and the gs and ein the demolition
phase are exactly the same as in td!
The string diagram is truly helpful this time. Now I see, as Richard hinted, that I could rewrite
the traditional expression using the naturality of unTip andretabulate to push gand eto the
left of the sequence and separate the two phases (Figure 7). But in the string diagram, all those
rewritings amount to nothing more than gradually pulling the two phases apart, eventually making
the dashed line horizontal. In fact I don’t even bother to pull, because on this diagram I can already
see simultaneously both the sequence (the dots appearing one by one vertically) and the result of
rewriting the sequence using naturality.
∗ ∗ ∗
So, modulo naturality, the two algorithms have the same table demolition phase but different
table construction phases. If I can prove that their table construction phases are equal, then I’ll
have another proof that the two algorithms are equal, in addition to the parametricity-based
proof (Section 2.5). For td, the construction phase is a right-leaning tree on the diagram, whereas
forbuit’s a left-leaning tree. Maybe what I need is an equation about blank andretabulate that
can help me to rotate a tree. . . ?
cd (choose k xs) =mapB (flatten . choose k) (choose (k+1) xs)
The equation (∗) flashes through my mind. Of course it has to be this equation — I used it as a
specification for cd, the Haskell progenitor of retabulate . How else would I introduce retabulate
Page 22:
22 Hsiang-Shang Ko, Shin-Cheng Mu, and Jeremy Gibbons
bus e g 3
={- definition -}
unTip·mapBTg·retabulate·mapBTg·retabulate·mapBTg·retabulate·mapBTe·blank3
0
={- naturality of unTip -}
g·
unTip·retabulate·mapBTg·retabulate·mapBTg·retabulate·mapBTe·blank3
0
={- naturality of retabulate -}
g·
unTip·mapBT(mapBTg)·retabulate·retabulate·mapBTg·retabulate·mapBTe·blank3
0
={- naturality of unTip again -}
g·mapBTg·
unTip·retabulate·retabulate·mapBTg·retabulate·mapBTe·blank3
0
={- similarly -}
g·mapBTg·mapBT(mapBTg)·mapBT(mapBT(mapBTe))·
unTip·retabulate·retabulate·retabulate·blank3
0
={- functoriality -}
g·mapBT(g·mapBT(g·mapBTe))·
unTip·retabulate·retabulate·retabulate·blank3
0
Fig. 7. Rewriting bu s e g 3into two phases using naturality.
into the picture? But first let me update this for my dependently typed string diagrams:
= BT𝑛
𝑘
⊤⊤BT1+𝑘
𝑘BT𝑛
1+𝑘
retabulate
blank𝑛
𝑘BT𝑛
1+𝑘
⊤⊤
blank𝑛
1+𝑘blank1+𝑘
𝑘BT1+𝑘
𝑘⊤
(∗∗)
That’s a tree rotation all right! So I should do an induction that uses this equation to rotate the
right-leaning tree in tdand obtain the left-leaning tree in bu(Figure 8). And then I’ll need to prove
the equation, meaning that I’ll need to go through the definitions of retabulate andblank ...Oh
hell, that’s a lot of work.
But wait a minute — do I really need to go through all this?
The three functors at the top of the diagrams ( ∗∗) catch my attention. In Agda, they expand to
the type BTn
1+k(BT1+k
k(const⊤))x𝑠. An inhabitant of this type is a table of blank tables, so there is
no choice of table entries; and moreover the structures of all the tables are completely determined
by the indices...the type has a unique inhabitant! So the equation is actually trivial to prove: the
two sides are forced by the type to construct the same table. And I don’t need to look into the
definitions of retabulate andblank at all!
Relieved, I start to work on the proof. The precise notion I need here is (mere) propositions [The
Univalent Foundations Program 2013, Chapter 3]:
Page 23:
Binomial Tabulation: A Short Story 23
⊤⊤ BT3
2⊤ BT2
1⊤ BT1
0
blank1
0
blank2
1
blank3
2BT3
2
⊤ BT3
1⊤ BT1
0
blank1
0
blank3
1retabulateBT2
1
⊤ ⊤⊤ BT3
0BT1
0BT3
1BT2
1BT3
2
retabulate
retabulate
blank3
0= =
Fig. 8. Rewriting the table construction phase of tds e g 3to that of bus e g 3using the rotation equation (∗∗).
isProp :Set→Set
isProp a={x y :a}→ x≡y
The type BTn
kp x𝑠is propositional if the element types pare propositional — this is easy to prove
by a straightforward double induction:
BT-isProp :(∀{y𝑠}→ isProp(p y𝑠))→ isProp(BTn
kp x𝑠)
And then the equation ( ∗∗) can be proved trivially by invoking BT-isProp twice:
rotation :retabulate(blankn
ktt)≡mapBTblank1+k
k(blankn
1+ktt)
rotation =BT-isProp(BT-isProp refl)
The side conditions of retabulate andblank (omitted above) are all universally quantified. Usually
they make proofs more complex, but not in this case because the proof doesn’t look into any of the
function definitions. As long as the type is blank nested tables, the two sides of an equation can be
arbitrarily complicated, and I can still prove them equal just by using BT-isProp .
Wait, blank nested tables — aren’t those what the construction phases of both algorithms produce?
I face-palm. It was a waste of time proving the rotation equation. The construction phases of
both algorithms produce blank nested tables of the same type — BT3
2(BT2
1(BT1
0(const⊤))) x𝑠in
the concrete examples I tried (Figures 4 and 6). So I can directly prove them equal using BT-isProp
three times. There’s no need to do any rotation.
Oh well, rotation is still interesting because it helps to explain how the two algorithms are related
intensionally: they produce the same layers of tables but in opposite orders, and rotation helps
to show how one order can be rewritten into the other (Figure 8). It’s just that a rotation -based
proof would be quite tedious, and I don’t want to go through with that. A proof based on BT-isProp
should be much simpler. Conceptually I’ve figured it all out: both algorithms have two phases
modulo naturality; their table demolition phases are exactly the same, and their table construction
phases are equal due to the BT-isProp reasoning. But the general proof is still going to take some
work. If I want to stick to string diagrams, I’ll need to transcribe the algorithms into inductively
defined diagrams. Moreover, the BT-isProp reasoning is formally an induction (on the length of
the input list), which needs to be worked out. And actually, compared with a diagrammatic but
informal proof, I prefer a full Agda formalisation. That means I’ll need to spell out a lot of detail,
including functoriality and naturality rewriting (Figures 5 and 7). Whining, I finish the entire proof
in Agda. But as usual, in the end there’s a dopamine hit from seeing everything checked.
∗ ∗ ∗
Page 24:
24 Hsiang-Shang Ko, Shin-Cheng Mu, and Jeremy Gibbons
Still, I can’t help feeling that I’ve neglected a fundamental aspect of the problem: why the bottom-
up algorithm is more efficient. After making all the effort adopting dependent types and string
diagrams, do these state-of-the-art languages help me say something about efficiency too?
String diagrams make it easier for me to see that the table construction phases of both algorithms
produce the same layers of tables but in opposite orders. Only the order used by the bottom-
up algorithm allows table construction and demolition to be interleaved, and consequently the
algorithm needs no more than two layers of tables at any time. That’s the crucial difference between
the two algorithms. Now I need to figure out what the difference means algorithmically.
More specifically, why is it good to keep twolayers of tables and not more?
When there are multiple layers of tables of type BTn
kwith k<n, meaning that the input list is split
into proper sublists multiple times, all the final sublists will appear (as indices in the element types)
in the entire nested table multiple times — that is, overlapping subproblems will appear. Therefore,
when I use gto fill in a nested table, I’m invoking gto compute duplicate solutions for overlapping
subproblems, which is what I want to avoid. More precisely, ‘using gto fill in a nested table’ means
applying gunder at least two layers, for example mapBT(mapBTg):BT3
2(BT2
1(BT1
0s))⇒
BT3
2(BT2
1s), where the result is at least two layers of tables, so there need to be at least three layers
of tables (to which mapBT(mapBTg)is applied) for duplicate solutions of overlapping subproblems
to be recomputed. The bottom-up algorithm never gets to three layers of tables, and therefore
avoids recomputing solutions for overlapping subproblems.
That reasoning doesn’t sound too bad, although it’s clear that there’s much more to be done.
The whole argument is still too informal and lacks detail. It’s easy to poke holes in the reasoning —
for example, if the input list has duplicate elements, then the bottom-up algorithm won’t be able to
entirely avoid recomputing solutions of overlapping subproblems. To fix this, the algorithm will need
a redesign. And of course it’s tempting to explore more problem-decomposing strategies beyond
immediate sublists. Eventually I may arrive at something general about dynamic programming,
which was what Richard wanted to work out in his paper.
All those are for another day, however. I’ve had enough fun today. Mostly, what I did was
transcribe Richard’s programs into new languages, but that helped me to reason in new ways, using
more convenient tools to make sense of the programs.
I wish Richard was still around so that I could show all these to him. He would’ve liked the new
languages and the new ways of reasoning.
∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗
AFTERWORD
This work is presented as a kind of ‘Socratic monologue’, recording the thought processes of a
functional programmer as they solve a programming mystery. We were inspired by the science
fiction novel Project Hail Mary by Andy Weir, where the narrative masterfully weaves together
intuitive presentations of scientific knowledge and the protagonist’s application of that knowledge
to solve the problems he is facing. We envisaged to do something similar in this paper, although it
ends up being not as leisurely and entertaining as Weir’s novel, because we need to cover more
technical detail, and there is very little action in our story apart from sitting in front of a computer
and racking one’s brains. However, compared to the traditional rational reconstruction of a finished
piece of work, we believe that this format helps both the writer and the reader to focus on currently
available clues and how to make progress based on those clues by recreating the experience of
solving a mystery. In fact, our telling largely follows our actual development (tracing what cddoes
in Section 1.2, generalising BandB′toBTin Section 2.2, revising ImmediateSublistInduction in
Page 25:
Binomial Tabulation: A Short Story 25
Section 2.4, realising that the BT-isProp argument works more generally after proving rotation in
Section 3.2, etc) — that is, this paper is ‘based on a true story’.
The format also works well with various decisions regarding what to include in the paper, and
what to omit. We put emphasis on intuitive explanations, and give formal definitions, theorems,
and proofs only when necessary: we usually rely on intuitive reasoning to tackle a problem at first,
and do not hurry to write things down formally. The ancillary Agda code provides the omitted
formal detail though. We have striven to keep the paper fairly self-contained: the reader should
be able to get a sense of the main ideas just from the intuitive explanations. But we do not intend
this paper to be a tutorial on dependently typed programming in Agda or on category theory —
the paper is best thought of as a companion to such tutorials or textbooks, giving a larger but not
overly complicated example, and applying the abstract tools to that example. To make the paper
more accessible, we have also resisted the temptation to generalise or to answer every question: for
example, we do not generalise ImmediateSublistInduction for dynamic programming more broadly
(as Bird [2008] attempted to do); we leave the question of whether the type of retabulate uniquely
determines the extensional behaviour of its inhabitants as a conjecture (Section 2.3); and we avoid
digressions into topics such as how data types like BTcan be derived systematically (Section 2.2)
and whether BTis a graded comonad (Section 2.4).
This work gives a dependently typed treatment of the sublists problem. The problem has been
studied in other settings. It was one of the examples used by Bird and Hinze [2003] when studying
a technique of function memoisation using trees of shared nodes, which they called nexuses . Bird
[2008] went on to study top-down and bottom-up algorithms, where the sublists problem was the
final example. To cover all the examples in the paper, Bird’s generic bottom-up algorithm also
employed a form of nexus, but it is not needed for the sublists problem and thus omitted in our
work. Mu [2024] derived cdfrom the specification ( ∗) and proved the equality between tdandbu
using traditional equational reasoning. Neither Bird and Hinze [2003] nor Bird [2008] discussed
applications of the sublists problem, but Mu [2024] observed that reduction to it is a standard
technique in the algorithms community. None of these papers used dependent types (except that
Mu [2024, Section 4.3] mentioned the shape-indexed Bandcdin Section 2.1).
The general message we want to deliver is that we can discover, explain, and prove things
by writing them down in appropriate languages. More specifically, dependent types, category
theory, and string diagrams are some of those languages, and they should be in the toolbox of
the mathematically inclined functional programmer. In the case of dependent types, they can be
expressive enough to replace traditional (equational) specifications and proofs. For example, in place
of Mu’s [2024] derivation, retabulate can be constructed by assigning it a type having sufficient
information (Section 2.3), and the dependently typed tdandbucan be proved equal simply by
showing that they have the same, uniquely inhabited type (Section 2.5). This approach to program
correctness and program equality is still under-explored, and has potential to reduce proof burdens
drastically. As for category theory, even though we use it only in a lightweight manner, it still
offers a somewhat useful abstraction for managing more complex (in our case, indexed) definitions
as if they were simply typed (Section 3.1). More importantly, the categorical abstraction enables
the use of string diagrams to simplify proofs about functoriality and naturality. These properties
are only the simplest ones that string diagrams can handle — for other kinds of properties [Coecke
and Kissinger 2017; Hinze and Marsden 2023] the proof simplification can be even more dramatic,
although many of those properties are highly abstract. Our comparison between diagrammatic
and traditional equational reasoning (Figures 4 and 5, and Figures 6 and 7) should be a good, albeit
modest, demonstration of the power of string diagrams in a more practical, algorithmic scenario.
Page 26:
26 Hsiang-Shang Ko, Shin-Cheng Mu, and Jeremy Gibbons
ACKNOWLEDGMENTS
We would like to thank Liang-Ting Chen for offering helpful suggestions about the development;
Julie Summers, Royal Literary Fund Fellow at Kellogg College, Oxford, for commenting on an early
draft; and Gene Tsai and Zhixuan Yang for proofreading a draft.
REFERENCES
Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. 2012. Proofs for Free: Parametricity for Dependent Types.
Journal of Functional Programming 22, 2 (2012), 107–152. https://doi.org/10.1017/S0956796812000056
Richard Bird and Ralf Hinze. 2003. Functional Pearl: Trouble Shared is Trouble Halved. In Workshop on Haskell . ACM, 1–6.
https://doi.org/10.1145/871895.871896
Richard S. Bird. 2008. Zippy Tabulations of Recursive Functions. In International Conference on Mathematics of Program
Construction (MPC) (Lecture Notes in Computer Science, Vol. 5133) . Springer, 92–109. https://doi.org/10.1007/978-3-540-
70594-9_7
James Chapman, Pierre-Évariste Dagand, Conor McBride, and Peter Morris. 2010. The Gentle Art of Levitation. In
International Conference on Functional Programming (ICFP) . ACM, 3–14. https://doi.org/10.1145/1863543.1863547
Bob Coecke and Aleks Kissinger. 2017. Picturing Quantum Processes . Cambridge University Press. https://doi.org/10.1017/
9781316219317
Peter Dybjer. 1994. Inductive Families. Formal Aspects of Computing 6, 4 (1994), 440–465. https://doi.org/10.1007/BF01211308
Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, and Tarmo Uustalu. 2016. Combining Effects
and Coeffects via Grading. In International Conference on Functional Programming (ICFP) . ACM, 476–489. https:
//doi.org/10.1145/2951913.2951939
Ralf Hinze and Dan Marsden. 2023. Introducing String Diagrams: The Art of Category Theory . Cambridge University Press.
https://doi.org/10.1017/9781009317825
Shin-Cheng Mu. 2024. Bottom-Up Computation Using Trees of Sublists. Journal of Functional Programming 34 (2024),
e14:1–16. https://doi.org/10.1017/S0956796824000145
The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics . Institute for
Advanced Study. https://homotopytypetheory.org/book/
Antoine Van Muylder, Andreas Nuyts, and Dominique Devriese. 2024. Internal and Observational Parametricity for Cubical
Agda. Proceedings of the ACM on Programming Languages 8, POPL (2024), 8:1–32. https://doi.org/10.1145/3632850
Janis Voigtländer. 2009. Bidirectionalization for Free!. In Symposium on Principles of Programming Languages (POPL) . ACM,
165–176. https://doi.org/10.1145/1480881.1480904
