A note on notation
Disclaimer. The content of this page is largely LM-generated. It was written as a stopgap to make the panproto system legible while we work through the book verifying and editing the content by hand. When a chapter has been verified or edited by a human, the parts that were verified or edited will be noted at the head of the chapter.
Categories and their inhabitants are written in a standard way across the mathematical literature, and this book follows the standard without deviation.
A category is written with a script capital letter: , , . Two specific categories come up often enough to earn shorter names. is the category whose objects are sets and whose morphisms are functions. is the category whose objects are Haskell types and whose morphisms are Haskell functions. Specific categories of panproto objects carry subscripts: is the category of schemas under a protocol .
Objects of a category are written with capital letters: , , . Morphisms are written with lowercase letters and an arrow: reads “ is a morphism from to ”. Composition is written right-to-left with a small circle: is “ after ”, and applied to an argument it computes . The right-to-left order matches ordinary function application but disagrees with the left-to-right convention of Unix pipes and F#’s >> operator, which do not appear in this book.
The identity morphism on an object is . The set of morphisms from to is the hom-set ; some authors write this . Two objects and are isomorphic, written , when an invertible morphism between them exists.
Functors are written with capital Latin letters: , , . A functor from to is written , and its action on a morphism of is . A natural transformation between two functors is written with a Greek letter and a double arrow: . Its component at an object is .
Displayed mathematics sits on its own line between the usual delimiters, like this:
Commutative diagrams are rendered as squares and triangles in the pattern
with the understanding that the diagram commutes: the composite equals the composite . Identity morphisms are elided in diagrams by the universal convention, and composites are drawn only where they bear on the argument.
Code appears in fenced blocks. Haskell is used for the mathematical examples of Part I because its type syntax is the closest syntax to the mathematics. Rust is used for the panproto implementation. A language tag on every block identifies which is which:
id :: a -> a
id x = x
#![allow(unused)]
fn main() {
fn identity<T>(x: T) -> T { x }
}
Short code examples with no caption need no further comment. Where a code example earns a reference back from later prose, it carries a caption beneath it, numbered within the chapter.
Panproto-specific symbols accumulate as the book proceeds. The notation reference appendix collects them in one table with page references.