# Realizing applied category theory in Julia¶

### An introduction to Catlab.jl, an experimental framework for ACT¶

Evan Patterson
Stanford University, Statistics Department

MIT (Applied) Categories Seminar
January 16, 2020

## Applied category theory in 2020¶

Applications of category theory began in logic/type theory but have now spread to

• Quantum mechanics
• Chemistry (reaction networks, Petri nets)
• Databases and knowledge representation
• Control theory and robotics
• Probability and statistics
• ...

Why? CT offers a unifying and widely applicable toolbox for building mathematical models of compositional phenomena.

### But where are the tools?¶

In applied math, the math is only half the story.

Applied mathematics must ultimately feed back into better scientific and computational methods.

Software is a big part of this, but software tools for ACT are early and fragmented.

Question: How do we usefully realize the mathematical models of ACT on a computer?

### Two views on categories and software¶

1. Designing with categories: CT informing the design, architecture, and implementation of computer programs, in any domain

Slogan: "Design patterns, but better"

2. Computing on categories: data structures and algorithms for computing with objects and morphisms in categories

Slogan: "Computer algebra of categories" or "computational category theory"

Both are valuable, but they are not the same. In principle, they are orthogonal.

This talk is about computational category theory (mostly).

## Catlab.jl: an experimental framework for ACT¶

We are developing Catlab.jl, a Julia package that aims to be:

• programming library
• computer algebra system
• interactive computing environment (mainly through Jupyter)

Some specific features:

• Work with symbolic expressions for objects and morphisms
• Create, manipulate, and visualize wiring diagrams for morphisms
• Generate efficient Julia programs for algorithms expressed categorically

### Overview: representing morphisms in monoidal categories¶

As of today, one of Catlab's most powerful capabilities is transforming between different computational representations of morphisms in symmetric monoidal categories. ### Why Julia?¶

Why use Julia for ACT? Julia is a modern programming language:

• Multiple dispatch gives generic operations of composition, monoidal products, etc.
• Unicode operators enable familiar mathematical notation
• Macro system ala Lisp allows further customization of syntax

Yet Julia is also practical:

• Designed to be fast, thanks to JIT (just-in-time) compiler
• Growing force in conventional applied math community:
• Numerical linear algebra
• Differential equations
• Optimization
• Statistics and machine learning

### Some other projects in computational category theory¶

• Cateno by Jason Morton, in Julia
• Prototype, unmaintained since 2015
• Early inspiration for Catlab
• In turn, draws inspiration from Haskell type classes
• Categorical Query Language by Conexus AI (AGPL/proprietary)
• Solves word problems in finitely presented categories
• Statebox (AGPL/proprietary)
• Compositional programming with formal verification
• Rewriting and proof assistants for monoidal/higher categories:

### Talk outline¶

1. Major features
• Signatures, instances, and symbolic expressions
• Wiring diagrams
• Generating and parsing Julia programs
2. Applications
3. Future directions

## Signatures, instances, and symbolic expressions¶

In Catlab, you can define signatures of algebraic structures (@signature macro).

In :
module Sandbox # Encapsulate in module to avoid name conflicts later
export dom, codom, id, compose

using Catlab

@signature Category(Ob,Hom) begin
Ob::TYPE
Hom(dom::Ob,codom::Ob)::TYPE

id(A::Ob)::Hom(A,A)
compose(f::Hom(A,B), g::Hom(B,C))::Hom(A,C) <= (A::Ob, B::Ob, C::Ob)
end

end

Out:
Main.Sandbox

Note: Usually use Category from "standard library" (Catlab.Doctrines)

### Signature interface¶

Signatures define generic functions in Julia.

In :
methodswith(Sandbox.Category.Ob, Sandbox)

Out:
1-element Array{Method,1}:
• id(A::Main.Sandbox.Category.Ob) in Main.Sandbox
In :
methodswith(Sandbox.Category.Hom, Sandbox)

Out:
3-element Array{Method,1}:
• codom(::Main.Sandbox.Category.Hom) in Main.Sandbox
• compose(f::Main.Sandbox.Category.Hom, g::Main.Sandbox.Category.Hom) in Main.Sandbox
• dom(::Main.Sandbox.Category.Hom) in Main.Sandbox

### Instances¶

Two ways to instantiate a signature:

1. As Julia functions on concrete data types (@instance macro or standard Julia)
2. As typed systems of symbolic expressions (@syntax macro)

### Instance: category of matrices¶

Instance of Category with (element type, dimension) pairs as objects and matrices as morphisms.

In :
using Catlab, Catlab.Doctrines
import Catlab.Doctrines: Ob, Hom, dom, codom, id, compose, ⋅, ∘
using LinearAlgebra: I

struct MatrixDomain
eltype::Type
dim::Int
end

@instance Category(MatrixDomain, Matrix) begin
dom(M::Matrix) = MatrixDomain(eltype(M), size(M,1))
codom(M::Matrix) = MatrixDomain(eltype(M), size(M,2))

id(m::MatrixDomain) = Matrix{m.eltype}(I, m.dim, m.dim)
compose(M::Matrix, N::Matrix) = M*N
end


### Instance: Category of matrices¶

In :
M = [0 1; -1 0]

Out:
2×2 Array{Int64,2}:
0  1
-1  0
In :
compose(M,M)

Out:
2×2 Array{Int64,2}:
-1   0
0  -1
In :
id(dom(M))

Out:
2×2 Array{Int64,2}:
1  0
0  1

### Symbolic expressions¶

Automatically generate system of symbolic expressions for Category.

In :
@syntax CategoryExprs(ObExpr, HomExpr) Category begin
# Empty, so no simplification logic!
end

A, B, C, D = Ob(CategoryExprs, :A, :B, :C, :D)
f, g, h = Hom(:f, A, B), Hom(:g, B, C), Hom(:h, C, D)
f

Out:
$f : A \to B$
In :
compose(f,g)

Out:
$f \cdot g : A \to C$
In :
compose(compose(f,g),h)

Out:
$\left(f \cdot g\right) \cdot h : A \to D$

### Symbolic expressions¶

#### Expression types¶

In :
[ expr => typeof(expr) for expr in [A, f, id(A), compose(f,g) ] ]

Out:
4-element Array{Pair{A,DataType} where A,1}:
A => Main.CategoryExprs.Ob{:generator}
f => Main.CategoryExprs.Hom{:generator}
id(A) => Main.CategoryExprs.Hom{:id}
compose(f,g) => Main.CategoryExprs.Hom{:compose}  

#### Unicode operators¶

In :
f⋅g == compose(f,g)

Out:
true
In :
g∘f == compose(f,g)

Out:
true

### Simplification of symbolic expressions¶

By default, no simplification or normalization is performed.

In :
(f⋅g)⋅h == f⋅(g⋅h)

Out:
false

But we can define symbolic expressions that normalize at construction.

In :
@syntax NormalizingCategoryExprs(ObExpr, HomExpr) Category begin
compose(f::Hom, g::Hom) = associate_unit(new(f,g), id)
end

A, B, C, D = Ob(NormalizingCategoryExprs, :A, :B, :C, :D)
f, g, h = Hom(:f, A, B), Hom(:g, B, C), Hom(:h, C, D);


Note: Rewriting function associate_unit is built-in. You can also define your own.

### Simplification of symbolic expressions¶

#### Associativity and unitality¶

In :
(f⋅g)⋅h == f⋅(g⋅h)

Out:
true
In :
id(A)⋅f == f && f⋅id(B) == f

Out:
true

#### Unbiased representation¶

In :
args(f⋅g⋅h)

Out:
3-element Array{Main.NormalizingCategoryExprs.Hom{:generator},1}:
f
g
h

### Math interlude: generalized algebraic theories (GATs)¶

Signatures are based on GATs (Cartmell 1978; Cartmell 1986)

• GATs = algebraic theories + simple dependent types
• Same expressivity as esentially algebraic theories (Freyd 1972)
• Minimal logical system for axiomatizing categorical doctrines

Caveat: Catlab only supports signature of theory; axioms for the future.

Wanted: Math and data structures for treating GATs, or doctrines, as data.

## Wiring diagrams¶

Wiring diagrams, also known as

• string diagrams in physics and CT
• port graphs in computer science,

are a graphical syntax for morphisms in symmetric monoidal categories
(Spivak 2013; Rupel, Spivak 2013; Yau 2018).

Out:
$\left(f \otimes g\right) \cdot \sigma_{B,B} \cdot h \cdot \sigma_{C,C} : A \otimes A \to C \otimes C$
Out:

### Two kinds of wiring diagrams¶

1. Combinatorial: Wiring diagrams as data structure, no geometry (Catlab.WiringDiagrams)
2. Topological: Wiring diagrams as visualization, embedded in the plane (Catlab.Graphics)

By default, "wiring diagram" has the first meaning.

Another distinction: Catlab has extensive support for directed wiring diagrams.
Undirected wiring diagrams are planned for the future.

### Wiring diagrams as a data structure¶

Wiring diagrams are built on top of digraphs from LightGraphs.jl:

• Each box corresponds to a vertex
• Two special vertices for inputs/outputs of outer box
• Arbitrary metadata on boxes, ports, and wires

Two interfaces for wiring diagrams:

1. Imperative: Mutate wiring diagram by adding/removing boxes and wires
2. Categorical: Construct new diagrams from old by composing, tensoring, etc

### Imperative interface for wiring diagrams¶

Manually constructing the wiring diagram visualized above:

In :
using Catlab.WiringDiagrams

d = WiringDiagram([:A,:A], [:C,:C])
fv = add_box!(d, Box(:f, [:A], [:B]))
gv = add_box!(d, Box(:g, [:A], [:B]))
hv = add_box!(d, Box(:h, [:B,:B], [:C,:C]))
add_wires!(d, [ (input_id(d),1) => (fv,1), (input_id(d),2) => (gv,1),
(fv,1) => (hv,2), (gv,1) => (hv,1),
(hv,1) => (output_id(d),2), (hv,2) => (output_id(d),1) ])

d

Out:
WiringDiagram([:A,:A], [:C,:C],
[ 1 => {inputs},
2 => {outputs},
3 => Box(:f, [:A], [:B]),
4 => Box(:g, [:A], [:B]),
5 => Box(:h, [:B,:B], [:C,:C]) ],
[ Wire((1,1) => (3,1)),
Wire((1,2) => (4,1)),
Wire((3,1) => (5,2)),
Wire((4,1) => (5,1)),
Wire((5,1) => (2,2)),
Wire((5,2) => (2,1)) ])

### Wiring diagrams as a monoidal category¶

Making the same diagram, compositionally:

In :
A, B, C = Ports([:A]), Ports([:B]), Ports([:C])
f = singleton_diagram(Box(:f, A, B))
g = singleton_diagram(Box(:g, A, B))
h = singleton_diagram(Box(:h, B⊗B, C⊗C))

(f⊗g)⋅braid(B,B)⋅h⋅braid(C,C) == d

Out:
true
• All wiring diagrams are an instance of SymmetricMonoidalCategory
• Extra structure by parametrizing the base type, e.g., WiringDiagram{CartesianCategory.Hom}

### Wiring diagrams as an operad¶

The fundamental operation is substitution of diagrams for boxes (substitute), aka operadic composition (ocompose).

Example: Implementing compose for wiring diagrams

function compose(f::WiringDiagram, g::WiringDiagram)
d = WiringDiagram(dom(f), codom(g))
add_wires!(d, ((input_id(d),i) => (fv,i) for i in eachindex(dom(f))))
add_wires!(d, ((fv,i) => (gv,i) for i in eachindex(codom(f))))
add_wires!(d, ((gv,i) => (output_id(d),i) for i in eachindex(codom(g))))
substitute(d, [fv, gv])
end


Inverse of substitution is encapsulation of subdiagrams (encapsulate).

### Wiring diagrams and morphism expressions¶

Morphism expressions $\to$ wiring diagrams:

• Easy
• Uniquely defined
• One-liner using generic functor from expressions to another instance

Wiring diagrams $\to$ morphism expressions:

Caveat: Need to make math out of this algorithm!

### Normalization by round-tripping?¶

Decomposition algorithm maximizes parallelism (prefers $\circ$ over $\otimes$).

In :
roundtrip(expr) = to_hom_expr(FreeCartesianCategory, to_wiring_diagram(expr))

A, B, C = Ob(FreeCartesianCategory, :A, :B, :C)
f, g, h, k = Hom(:f, A, B), Hom(:g, B, C), Hom(:h, A, B), Hom(:k, B, C)

expr = compose(otimes(f,h), otimes(g,k))

Out:
$\left(f \otimes h\right) \cdot \left(g \otimes k\right) : A \otimes A \to C \otimes C$
In :
expr2 = roundtrip(expr)

Out:
$\left(f \cdot g\right) \otimes \left(h \cdot k\right) : A \otimes A \to C \otimes C$
In :
roundtrip(expr2) == expr2

Out:
true

### Normalization by round-tripping?¶

Implicitly uses coherence axioms for copying, deleting, etc.

In :
mcopy(otimes(A,B))

Out:
$\Delta_{A \otimes B} : A \otimes B \to A \otimes B \otimes A \otimes B$
In :
roundtrip(mcopy(otimes(A,B)))

Out:
$\left(\Delta_{A} \otimes \Delta_{B}\right) \cdot \left(\mathrm{id}_{A} \otimes \sigma_{A,B} \otimes \mathrm{id}_{B}\right) : A \otimes B \to A \otimes B \otimes A \otimes B$
In :
delete(otimes(A,B))

Out:
$\lozenge_{A \otimes B} : A \otimes B \to I$
In :
roundtrip(delete(otimes(A,B)))

Out:
$\lozenge_{A} \otimes \lozenge_{B} : A \otimes B \to I$

## Visualizing wiring diagrams¶ ### Wiring diagrams in Graphviz¶

In :
using Catlab.Graphics

to_graphviz(d, orientation=LeftToRight)

Out:
In :
to_graphviz(d, orientation=TopToBottom, labels=true, label_attr=:taillabel)

Out:

### Wiring diagrams in Compose.jl/TikZ¶

In :
using Compose: fill, stroke

to_composejl(FreeSymmetricMonoidalCategory, d,
box_props=[fill("lavender"),stroke("black")])

Out:
In :
to_tikz(FreeSymmetricMonoidalCategory, d,
labels=true, labels_pos=0.25, arrowtip="Latex", arrowtip_pos=1.0)

Out:

### Serializing wiring diagrams¶

Read and write wiring diagrams as:

Warning: No standards in this area, so interoperability is limited.

## Generating and parsing Julia code¶

Catlab can transform Julia programs to/from other representations of morphisms.

Convenient to specify available functions by presenting a cartesian monoidal category.

In :
@present TrigFunctions(FreeCartesianCategory) begin
R::Ob  # Real numbers
sin::Hom(R,R)
cos::Hom(R,R)
(+)::Hom(otimes(R,R),R)
(*)::Hom(otimes(R,R),R)
end

generator(TrigFunctions, :+)

Out:
$+ : R \otimes R \to R$

### Generating Julia programs from morphism expressions¶

Functorial compilation of morphism expression into Julia function:

In :
gen(name::Symbol) = generator(TrigFunctions, name)

expr = compose(mcopy(gen(:R)), otimes(gen(:sin),gen(:cos)), gen(:*))

Out:
$\Delta_{R} \cdot \left(\mathrm{sin} \otimes \mathrm{cos}\right) \cdot * : R \to R$
In :
using Catlab.Programs

compile_expr(expr, name=:my_trig_polynomial, args=[:x])

Out:
:(function my_trig_polynomial(x)
v1 = sin(x)
v2 = cos(x)
v3 = v1 * v2
return v3
end)

### Parsing wiring diagrams from Julia code¶

Conversely, parse wiring diagrams by evaluating code in fragment of Julia language.

In :
parsed = @parse_wiring_diagram TrigFunctions (x::R) begin
y1, y2 = sin(x), cos(x)
return y1 * y2
end

to_graphviz(parsed, orientation=LeftToRight,
node_attrs=Dict(:fontname => "Courier"))

Out:
In :
parsed == @parse_wiring_diagram(TrigFunctions, (x::R) -> sin(x) * cos(x))

Out:
true

### Application: semantics of data science code¶

Project at IBM Research AI and Stanford (Patterson, Baldini, Mojsilovic, Varshney 2018): $\xrightarrow{\text{analyze}}$ $\xrightarrow{\text{enrich}}$ ### Application: compositional assembly planning¶

Prototype project at Siemens (Master, Patterson, Yousfi, Canedo 2019):

• Planning and scheduling for automated assembly
• Toy domain: simulated LEGO assembly in Minecraft ### Application: scientific model augmentation¶

Ongoing project at Georgia Tech Research Institute (Halter, Herlihy, Fairbanks 2019):

• Model augmentation: transform existing scientific models to create new models
• Current focus on epidemiology (SIR, SIRS, etc): agent-based models and ODEs
• Code available as SemanticModels.jl ## Future directions¶

Many! I'll just mention a few areas.

#### Computer algebra¶

• Declarative, rule-based rewriting for
• symbolic expressions
• wiring diagrams
• Solving word problems
• Calculating hom-sets
• GATs and beyond
• Data structures for, and operations on, GATs
• Extensions for unbiased operations, such as products and permutations

# Thanks!¶

### Resources¶ epatters/Catlab.jl on GitHub #catlab on the Julia Slack evan@epatters.org

### Getting involved¶

I'm looking for both users and contributors. There is much to do!