Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Binomial Tabulation: A Short Story

Hsiang-Shang Ko, Shin-Cheng Mu, Jeremy Gibbons

TL;DR

This work reinterprets Bird's binomial tabulations using dependent types and string diagrams to connect top-down and bottom-up approaches for sublist problems. It introduces binomial-tree structures (B, B^n_k, BT) and a dependently typed retabulate operation to precisely capture the sublist-indexed data and their transformations, enabling typed specifications that subsume traditional equational proofs. By framing the algorithms in categories of families and employing natural transformations, the paper demonstrates parametricity-based equalities (td = bu) and uses string diagrams to separate construction and demolition phases and to compare two-phase reasoning. The combination of dependent types, category theory, and diagrammatic reasoning yields a compact, correctness-driven path to understanding and potentially improving dynamic-programming-style tabulations, with explicit attention to efficiency via a two-layer table strategy.

Abstract

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.

Binomial Tabulation: A Short Story

TL;DR

This work reinterprets Bird's binomial tabulations using dependent types and string diagrams to connect top-down and bottom-up approaches for sublist problems. It introduces binomial-tree structures (B, B^n_k, BT) and a dependently typed retabulate operation to precisely capture the sublist-indexed data and their transformations, enabling typed specifications that subsume traditional equational proofs. By framing the algorithms in categories of families and employing natural transformations, the paper demonstrates parametricity-based equalities (td = bu) and uses string diagrams to separate construction and demolition phases and to compare two-phase reasoning. The combination of dependent types, category theory, and diagrammatic reasoning yields a compact, correctness-driven path to understanding and potentially improving dynamic-programming-style tabulations, with explicit attention to efficiency via a two-layer table strategy.

Abstract

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.

Paper Structure

This paper contains 13 sections, 6 equations, 9 figures.

Table of Contents

  1. Functions
  2. Top-Down and Bottom-Up Algorithms
  3. Rearranging Binary Trees
  4. Rearranging Binomial Trees
  5. Types
  6. Shapes in Types
  7. Properties in Types
  8. Specifications as Types
  9. Precision of Types
  10. Equality from Types
  11. Diagrams
  12. From Categories to String Diagrams
  13. Diagrammatic Reasoning

Figures (9)

  • Figure 1: Computing top-down.
  • Figure 2: Computing bottom-up.
  • Figure 3: How constructs a new level.
  • Figure 4: A special case of the top-down algorithm as a string diagram.
  • Figure 5: Rewriting $\mathord{\textsf{td}}\;\mathit{s}\;\mathit{e}\;\mathit{g}\;\mathrm 3$ into two phases using functoriality.
  • ...and 4 more figures