Generalized Algebraic Theories (GAT)

• : an extension of algebraic theories sufficient to axiomatize categorical structures
• : more suggestively called a dependently typed algebraic theory
  • eg: type of a morphism depends on a pair of objects, the domain and codomain

Algebraic Theories

• An algebraic structure is a mathematical object whose axioms all take the form of equations that are universally quantified (the equations have no exceptions)
• eg: a group, a category

Why generalizing it?

• the theory of categories is not algebraic
  • ie: a category cannot be defined as a (multi-sorted) algebraic theory
  • : the operation of composition is partial, since you can only compose morphisms with compatible (co)domains
• first attempt on generalizing it: Freyd’s essentially algebraic theories
  • nlab link
  • downside:
    • to maintain the equational character of the system, the domains of operations must themselves be defined equationally
    • As your theories get more elaborate, the sets of equations defining the domains get more complicated and reasoning about the structure is overwhelming.
• later: Cartmell proposed GAT, solving the issue (to have total operations) by using dependent types

Components

Context

• : a finite (ordered) list of named variables tagged with types, where the type at a given position may depend on variables at previous positions
• eg: [a::Ob, b::Ob, c::Ob], or equivalently [(a, b, c)::Ob]
• eg: [a::Ob, b::Ob, f::Hom(a, b)]
  • type of variable f depends on previous variables a and b
• eg: [], no context

Judgments

• : A GAT is defined by a sequence of judgments.
• Every judgment has a context, which we write to the right of the turnstile ($\dashv$)
• 3 kinds of judgments
  1. Type constructor
     • : introduce new types, which are possibly dependent on variables in the context
     • eg: Ob::TYPE ⊣ [], or $\text{Ob}: \text{type} \dashv$ in math notation
     • eg: Hom(d, c)::TYPE ⊣ [(d, c)::Ob], or $\text{Hom}(d, c) : \text{type} \dashv c, d : \text{Ob}$
  2. Term constructor
     • : introduce typed terms. Both the term and its type may depend on variables in the context.
     • eg: id(a)::Hom(a,a) ⊣ [a::Ob]
     • eg: (a ⊗ b)::Ob ⊣ [(a,b)::Ob]
  3. Term equality
     • : Axioms asserting equations between terms in context
     • eg: (a ⊗ b) ⊗ c == a ⊗ (b ⊗ c) ⊣ [(a,b,c)::Ob]
       (4.) Type equality. excluded by GATlab.jl as equations between types are better handled by isomorphisms.

Summary

• In general, a GAT consists of a signature, defining the types and terms of the theory, and a set of axioms, the equational laws satisfied by models of the theory

Module Systems in the ML Language Family

• signature
• module: implements the signature, comprises:
  1. a choice of concrete type for each type in the signature
  2. a function for each term constructor