Browse Source

CLEANUP: Clean up and document basic interface for functors.

pull/518/head
Evan Patterson 3 weeks ago
parent
commit
386f15d562
  1. 23
      docs/src/apis/categorical_algebra.md
  2. 28
      src/categorical_algebra/Categories.jl
  3. 12
      src/categorical_algebra/FinCats.jl
  4. 1
      test/categorical_algebra/CategoricalAlgebra.jl
  5. 13
      test/categorical_algebra/Categories.jl

23
docs/src/apis/categorical_algebra.md

@ -1,20 +1,21 @@
# [Categorical algebra](@id categorical_algebra)
## FinSet and FinRel
## Sets and Relations
The following APIs implement FinSet, the category of Finite Sets (actually the skeleton of FinSet). The objects of this category are natural numbers where `n` represents a set with `n` elements. The morphisms are functions between such sets. We use the skeleton of FinSet in order to ensure that all sets are finite and morphisms can be stored using lists of integers. Finite relations are built out of FinSet and can be used to do some relational algebra.
```@autodocs
Modules = [
CategoricalAlgebra.Sets,
CategoricalAlgebra.FinSets,
CategoricalAlgebra.FinRelations,
]
Private = false
```
## Diagrams, Limits, and Colimts
## Free Diagrams, Limits, and Colimts
The following modules define diagrams in an arbitrary category and specify limit and colimt cones over said diagrams. Thes constructions enjoy the fullest support for FinSet and are used below to define presheaf categories as C-Sets. The general idea of these functions is that you set up a limit computation by specifying a diagram and asking for a limit or colimit cone, which is returned as a struct containing the apex object and the leg morphisms. This cone structure can be queried using the functions [`apex`](@ref) and [`legs`](@ref). Julia's multiple dispatch feature is heavily used to specialize limit and colimit computations for various diagram shapes like product/coproduct and equalizer/coequalizer. As a consumer of this API, it is highly recommended that you use multiple dispatch to specialize your code on the diagram shape whenever possible.
The following modules define free diagrams in an arbitrary category and specify limit and colimt cones over said diagrams. Thes constructions enjoy the fullest support for FinSet and are used below to define presheaf categories as C-Sets. The general idea of these functions is that you set up a limit computation by specifying a diagram and asking for a limit or colimit cone, which is returned as a struct containing the apex object and the leg morphisms. This cone structure can be queried using the functions [`apex`](@ref) and [`legs`](@ref). Julia's multiple dispatch feature is heavily used to specialize limit and colimit computations for various diagram shapes like product/coproduct and equalizer/coequalizer. As a consumer of this API, it is highly recommended that you use multiple dispatch to specialize your code on the diagram shape whenever possible.
```@autodocs
Modules = [
@ -24,9 +25,18 @@ Modules = [
Private = false
```
# Acsets
## Categories
## Overview and Theory
```@autodocs
Modules = [
CategoricalAlgebra.Categories,
CategoricalAlgebra.FinCats,
]
```
## Acsets
### Overview and Theory
For an in depth look into the theory behind acsets, we refer the reader to [our paper](https://arxiv.org/abs/2106.04703) on the subject, which also gives some sense as to how the implementation works. Here, we give a brief tutorial before the the API documentation.
@ -80,7 +90,7 @@ g = @acset WeightedGraph{Float64} begin
end
```
## API
### API
We first give an overview of the data types used in the acset machinery.
@ -93,7 +103,6 @@ We first give an overview of the data types used in the acset machinery.
`CatDesc/AttrDesc` the encoding of a schema into a Julia type. These exist because Julia only allows certain kinds of data in the parameter of a dependent type. Thus, we have to serialize a schema into those primitive data types so that we can use them to parameterize the ACSet type over the schema. This is an implementation detail subject to complete overhaul.
```@autodocs
Modules = [
CategoricalAlgebra.CSets,

28
src/categorical_algebra/Categories.jl

@ -13,9 +13,10 @@ instances are supported through the wrapper type [`TypeCat`](@ref). Finitely
presented categories are provided by another module, [`FinCats`](@ref).
"""
module Categories
export Cat, Functor, dom, codom, TypeCat
export Cat, TypeCat, Ob, Functor, dom, codom, ob_map, hom_map
import ...Theories: dom, codom
using ..Sets
import ...Theories: Ob, dom, codom
# Generic interface
###################
@ -33,12 +34,33 @@ in the graph.
abstract type Cat{Ob,Hom} end
""" Abstract base type for a functor between categories.
A functor has a domain and a codomain ([`dom`](@ref) and [`codom`](@ref)), which
are categories, and object and morphism maps, which can be evaluated using
[`ob_map`](@ref) and [`hom_map`](@ref). The functor object can also be called
directly when the objects and morphisms have distinct Julia types. This is often
but not always the case (see [`Cat`](@ref)), so when writing generic code one
should prefer the `ob_map` and `hom_map` functions.
"""
abstract type Functor{Dom<:Cat,Codom<:Cat} end
dom(F::Functor) = F.dom
codom(F::Functor) = F.codom
""" Evaluate functor on object.
"""
function ob_map end
""" Evaluate functor on morphism.
"""
function hom_map end
""" Forgetful functor Ob: Cat → Set.
Sends a category to its set of objects and a functor to its object map.
"""
function Ob end
# Instances
###########
@ -49,4 +71,6 @@ The Julia types should form an `@instance` of the theory of categories
"""
struct TypeCat{Ob,Hom} <: Cat{Ob,Hom} end
Ob(::TypeCat{T}) where T = TypeSet{T}()
end

12
src/categorical_algebra/FinCats.jl

@ -5,23 +5,25 @@ the category **Set**: a finitary, combinatorial setting where explicit
calculations are possible.
"""
module FinCats
export FinCat, FinCatGraph, Ob, is_free, ob_generators, hom_generators,
export FinCat, FinCatGraph, is_free, ob_generators, hom_generators,
equations, presentation,
FinFunctor, FinDomFunctor, is_functorial, ob_map, hom_map,
collect_ob, collect_hom,
FinFunctor, FinDomFunctor, is_functorial, collect_ob, collect_hom,
Vertex, Edge, Path, graph, edges, src, tgt
using AutoHashEquals
using Reexport
using StaticArrays: SVector
@reexport using ..Categories
using ...GAT, ...Present, ...Syntax
import ...Present: equations
using ...Theories: Category, ObExpr, HomExpr
import ...Theories: Ob, dom, codom, id, compose, ,
using ...Graphs, ..FreeDiagrams, ..FinSets, ..CSets, ..Categories
import ...Theories: dom, codom, id, compose, ,
using ...Graphs, ..FreeDiagrams, ..FinSets, ..CSets
import ...Graphs: edges, src, tgt
import ..FreeDiagrams: FreeDiagram, diagram_ob_type, cone_objects, cocone_objects
import ..Limits: limit, colimit
import ..Categories: Ob, ob_map, hom_map
# Categories
############

1
test/categorical_algebra/CategoricalAlgebra.jl

@ -37,6 +37,7 @@ end
end
@testset "Categories" begin
include("Categories.jl")
include("FinCats.jl")
include("CatElements.jl")
end

13
test/categorical_algebra/Categories.jl

@ -0,0 +1,13 @@
module TestCategories
using Test
using Catlab.Theories
using Catlab.CategoricalAlgebra.Sets, Catlab.CategoricalAlgebra.Categories
# Categories from Julia types
#############################
C = TypeCat{FreeCategory.Ob,FreeCategory.Hom}()
@test Ob(C) == TypeSet{FreeCategory.Ob}()
end
Loading…
Cancel
Save