Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

String Diagrams for $λ$-calculi and Functional Computation

Dan Ghica, Fabio Zanasi

TL;DR

This tutorial gives an advanced introduction to string diagrams and graph languages for higher-order computation by rationally reconstructing a syntax from the categorical model, which in many ways is shown to be an improvement over the conventional linear term syntax.

Abstract

This tutorial gives an advanced introduction to string diagrams and graph languages for higher-order computation. The subject matter develops in a principled way, starting from the two dimensional syntax of key categorical concepts such as functors, adjunctions, and strictification, and leading up to Cartesian Closed Categories, the core mathematical model of the lambda calculus and of functional programming languages. This methodology inverts the usual approach of proceeding from syntax to a categorical interpretation, by rationally reconstructing a syntax from the categorical model. The result is a graph syntax -- more precisely, a hierarchical hypergraph syntax -- which in many ways is shown to be an improvement over the conventional linear term syntax. The rest of the tutorial focuses on applications of interest to programming languages: operational semantics, general frameworks for type inference, and complex whole-program transformations such as closure conversion and automatic differentiation.

String Diagrams for $λ$-calculi and Functional Computation

TL;DR

This tutorial gives an advanced introduction to string diagrams and graph languages for higher-order computation by rationally reconstructing a syntax from the categorical model, which in many ways is shown to be an improvement over the conventional linear term syntax.

Abstract

This tutorial gives an advanced introduction to string diagrams and graph languages for higher-order computation. The subject matter develops in a principled way, starting from the two dimensional syntax of key categorical concepts such as functors, adjunctions, and strictification, and leading up to Cartesian Closed Categories, the core mathematical model of the lambda calculus and of functional programming languages. This methodology inverts the usual approach of proceeding from syntax to a categorical interpretation, by rationally reconstructing a syntax from the categorical model. The result is a graph syntax -- more precisely, a hierarchical hypergraph syntax -- which in many ways is shown to be an improvement over the conventional linear term syntax. The rest of the tutorial focuses on applications of interest to programming languages: operational semantics, general frameworks for type inference, and complex whole-program transformations such as closure conversion and automatic differentiation.
Paper Structure (30 sections, 8 theorems, 170 equations, 8 figures)

This paper contains 30 sections, 8 theorems, 170 equations, 8 figures.

Table of Contents

  1. Introduction
  2. Syntactic trinitarianism
  3. Further reading and related work
  4. String Diagrams
  5. Categories and their graphical language
  6. Functors and boxes
  7. Natural transformations
  8. Adjunctions
  9. Homset adjunctions
  10. Monoidal categories
  11. Strictification and string diagrams
  12. Symmetric monoidal categories
  13. Foliations
  14. Properties of foliations
  15. Further reading and related work
  16. ...and 15 more sections

Key Result

Theorem 2.44

Any morphism $f$ in a freely generated (strict) monoidal category can be presented as where $f_{j,k}$ are elements of the signature or structural morphisms (identities, symmetries if the category is symmetric, etc.).

Figures (8)

  • Figure 1: An example of a string diagram
  • Figure 2: Strictification equations (Definition \ref{['definition:catd']})
  • Figure 3: Symmetry equations
  • Figure 4: Symmetry equations absorbed into the graphical notation
  • Figure 5: Symmetric closed monoidal adjunction equations
  • ...and 3 more figures

Theorems & Definitions (63)

  • Definition 2.1: Category
  • Definition 2.3
  • Remark 2.4
  • Definition 2.5
  • Definition 2.6
  • Remark 2.7
  • Definition 2.8: Functor
  • Remark 2.9
  • Remark 2.10
  • Definition 2.11: Natural transformation
  • ...and 53 more