Juliacon 2024

The core idea of GATlab is the following. Consider the following module signature in OCaml.

module type MONOID =
  sig
    type t
    val zero : t
    val add : (t, t) -> t
  end

A module can be said to "implement" this signature if the module contains a type t along with a "zero value" for t and a function which adds two elements of t.

module INTMONOID : MONOID =
  struct
    type t = int
    let zero = 0
    let add (x, y) = x + y
  end

However, we could also interpret that signature in a different way: we could interpret it as a specification for syntax trees. Specifically, we could make a data structure which looks like the following (we now switch back to Julia)

abstract type MonoidTerm{T} end

eltype(t::MonoidTerm{T}) where {T} = T

struct Zero{T} <: MonoidTerm{T}
end

struct Add{T} <: MonoidTerm{T}
  lhs::MonoidTerm
  rhs::MonoidTerm
end

struct Val{T} <: MonoidTerm{T}
  value::T
end

We can then make implementations using multiple dispatch

abstract type Monoid{T} end

struct IntMonoid <: Monoid{Int}
end

zero(::IntMonoid) = 0
add(::IntMonoid, x::Int, y::Int) = x + y

Using such a "module" of type Monoid{T}, we can interpret any MonoidTerm{T} to produce a T! That is, we can write a function

function interpret(M::Monoid{T}, t::MonoidTerm{T}) where {T}
  if t isa Zero
    zero(M)
  elseif t isa Add
    add(M, interpret(M, t.lhs), interpret(M, t.rhs))
  elseif t isa Val
    t.value
  end
end

If we build a signature+module system from the ground up using macros and multiple dispatch, we can also build in these syntax trees and corresponding interpreters. It is also possible to compile a syntax tree to a Julia function.

GATlab is an implementation of this... and significantly more. First of all, one can add laws to a signature to produce a theory (theory = signature + laws).

@theory ThMonoid begin
  T::TYPE
  zero::T
  add(x::T, y::T)::T
  add(x, zero) == x ⊣ [x::T]
  add(zero, x) == x ⊣ [x::T]
  add(add(x, y), z) == add(x, add(y, z)) ⊣ [x::T, y::T, z::T]
end

We call a law-abiding implementation of the signature of a theory a model of that theory.

Now, we cannot statically check that a model of a theory satisfies the laws, but the laws do provide a principled way of doing rewriting on the syntax trees associated to a signature. We use e-graphs to perform this rewriting, with a custom type-aware implementation.

The mathematics behind all of this is studied within universal algebra. Many of the features of ML-style module systems have analogues within universal algebra. For instance, one can build up complex theories via inheriting simpler theories, or create maps between theories (analogous to ML-style functors), and these operations on theories can be used to generate new models from old ones.

However, universal algebra cannot capture certain structures important for our work in Catlab, first and foremost categories. To support categories, we upgrade from algebraic theories to generalized algebraic theories (or GATs, which is where the name of GATlab comes from), as introduced by Cartmell. These support theories with dependent types, which looks like the following

@theory ThCategory begin
  Ob::TYPE
  Hom(dom, codom)::TYPE ⊣ [dom::Ob, codom::Ob]
  id(a::Ob)::Hom(a, a)
  compose(f::Hom(a, b), g::Hom(b, c))::Hom(a, c) ⊣ [a::Ob, b::Ob, c::Ob]
  compose(f, id(b)) == g ⊣ [a::Ob, b::Ob, f::Hom(a, b)]
  ...
end  

Just like with algebraic theories, we can work with syntax trees, we can write interpreters, and we can programmatically manipulate models.

GATlab can be compared to frameworks like MMT, but with the ability to have models compute fast. Another comparison would be to Julia libraries like Symbolics.jl. Symbolics.jl is far more advanced for traditional computer algebra, but the underlying assumption is that variables are some sort of number, while GATlab does not assume this. Finally, we might compare with Julia libraries like WhereTraits.jl which add traits/typeclasses to Julia. GATlab differs from these in being more similar to Standard ML modules rather than Haskell typeclasses or Rust traits, and in its CAS aspects. We hope to learn from these other projects and integrate their strengths as GATlab evolves.

In this talk, we will give an introduction to GATlab from a practical perspective, showing how to work with simple theories and modules, and emphasizing the connection (as described above) between computer algebra and module systems.