Algebraic data types

Algebraic data types are data types that are specified in an algebraic or equational way. Beyond that obvious connotation, this area is plagued by a hodge-podge of terminology—“algebra data types” (ADTs), “generalized algebraic data types” (GADTs), “inductive types”—that describe similar concepts but are used inconsistently by category theorists, type theorists, and programmers (TCS.SE ). There is no universally accepted, precise definition of an algebraic data type. Worse, the term seems to have two distinct usages:

  1. Algebraic as involving algebraic operations. Algebraic data types in this sense certainly involve units, products, and sums. Depending on the context, they may also involve exponentials and recursive (inductive) definitions. This now seems to be the dominant usage, especially in PLT.
  2. Algebraic as equational. Here the essential feature is the specification, ala sketches, of data types by equations between function compositions (where products and sums may or may not be allowed). Some the category-theoretic literature on “algebraic data type specification” uses this interpretation.

Literature

Algebras for endofunctors and monads

Algebras for endofunctors , aka F-algebras , are one approach to the categorical semantics of ADTs. In particular, ADTs can be formalized the initial algebras of polynomial functors.

  • Barr & Wells, 1998: Category theory for computing science, Chapter 14: Algebras for endofunctors
  • Awodey, 2010: Category theory, 2nd ed., Section 10.5: Alegebras for endofunctors
  • Riehl, 2016: Category theory in context, Chapter 5: Monads and their algebras

Algebraic data specifications

  • Piessens & Steegmans, 1995: Categorical data-specifications (pdf)

Miscellaneous

  • Bunkenburg, 1993: The Boom hierarchy (doi, pdf)
    • Interesting, though stylistically idiosyncratic
    • Establishes a dictionary between common data structures and free algebras of algebraic theories with a single binary operator: ordered binary trees are free unital magmas, lists are free monoids (or free associative unital magmas), multisets (or bags) are free commutative monoids, and sets are free idempotent commutative monoids