Catlab refactor II: Basic Sets

Set interfaces

We saw the interface for ThSet in the previous post. Let’s reproduce it here:

@theory ThSet begin
  X::TYPE
  Bool′::TYPE{Bool}
  contains(elem::X)::Bool′
end

Any implementation of ThSet must pick a Julia datatype for its elements, and we name this type X. However, the set might be smaller than the entire type. So, part of the data one must always provide, in order to implement ThSet, is a membership predicate, contains. This evaluates to true for the elements of the Julia type X which are actually in the set.

Now we define a Julia type, SetOb, which wraps arbitrary implementations of the theory of sets:

ThSet.Meta.@wrapper SetOb # `Set` already claimed by Julia!

Our predicate contains only accepts arguments which were of the right Julia type, but we can overload the in method to be more permissive: it returns false if the input was not of the right type rather than throwing a MethodNotFound error.

Base.in(x, set::AbsSet) = try 
  ThFinSet.contains(set, x)
catch e 
  e isa MethodError || throw(e)
  false
end

Next we consider how ThFinSet extends this theory with a Julia iterator¹ and an integer cardinality, i.e. a length.

@theory ThFinSet <: ThSet begin
  Int′::TYPE{Int}
  Any′::TYPE{Any}
  length()::Int′
  iterator()::Any′ # length(collect(iterator()) == length()
end

ThFinSet.Meta.@wrapper FinSet

const AbsSet = Union{SetOb, FinSet} # `AbstractSet` already claimed by Julia!

Now, when you receive a FinSet, you know you have something which you can check for membership, get the length, and iterate over. There are no type parameters, in contrast to old Catlab:

abstract type FinSet{S,T} <: SetOb{T} end # OLD CATLAB

This extra type parameter S was needed because we wanted different code to be executed when we were working in \mathsf{Skel(FinSet)} versus when we happened to have some other type of set with Int elements. This is an example of complicated type acrobatics needed to work directly with multiple dispatch, in contrast to the model-based approach taken in the refactored code.

Set implementations

The theories of sets and finite sets will make more sense if you see some examples of implementations of them. Some of these are shown below:

""" 
Unbiased Cartesian product. `S` is either SetOb or FinSet. 
`T` is the type of the tuple elements.
"""
struct ProdSet{S<:AbsSet, T}
  sets::Vector{S}
  ProdSet(sets::Vector{S}) where {S<:AbsSet} = 
    new{S, Tuple{eltype.(sets)...}}(sets)
end

# Common method for ThSet and ThFinSet implementations
contains_set(model::ProdSet{<:Any, T}, i::T) = 
  all(e ∈ s for (s, e) in zip(model.sets, i))

@instance ThSet{T} [model::ProdSet{SetOb,T}] where T begin
  contains(i::T)::Bool = contains_set(model, i)
end

@instance ThFinSet{T} [model::ProdSet{FinSet,T}] where T begin
  contains(i::T)::Bool = contains_set(model, i)
  length()::Int = prod(length.(model.sets))
  iterator()::Any = Iterators.product(model.sets...)
end

struct FinSetInt
  n::Int
end 

@instance ThFinSet{Int} [model::FinSetInt] begin
  contains(i::Int)::Bool = 0 < i ≤ model.n
  length()::Int = model.n
  iterator()::Any = 1:model.n
end

struct SingletonSet end 

@instance ThFinSet{Nothing} [model::SingletonSet] begin
  contains(::Nothing)::Bool = true
  length()::Int = 1
  iterator()::Any = [nothing]
end

struct EmptySet end 

@instance ThFinSet{Union{}} [model::EmptySet] begin
  contains(::Union{})::Bool = false
  length()::Int = 0
  iterator()::Any = Union{}[]
end

Default implementations

Suppose I want a TypeSet, which in the previous post we saw is a particular implementation of ThSet that is specified by Julia type.

string_set = SetOb(TypeSet(String))
int_set = SetOb(TypeSet(Int))

In old Catlab, one simply writes TypeSet(String) and gets a SetOb; this is because we used to have TypeSet <: SetOb. That is no longer the case, so it seems like we’ve lost something; we have to do this tedious wrapping if we want to use TypeSet(String) as the codom of a function, since the function is expecting a model wrapped in a smart constructor, not a raw model (which could be any Julia type).

However, in all honesty, how many different implementations of SetOb are there? (not many) And how many of them simply take in a Julia type as their only data? (just one). Thus we should feel entitled to define the following shortcut:

""" Default model for a Set made out of a Julia `Type` """
SetOb(T::Type) = SetOb(TypeSet{T}())

Now it is just as easy as before (though we use SetOb rather than TypeSet):

string_set = SetOb(String)
int_set = SetOb(Int)

The general lesson is: if there is a ‘canonical’ implementation for some given data, we can define a method for the wrapper type to simply take in that data, call the canonical implementation on the data and then wrap that. This pattern for model wrapper types gets used all the time throughout the refactor. Another example would be:

FinSet(::Nothing) = FinSet(SingletonSet())

There are times where there isn’t a canonical implementation. Consider:

FinSet(s1::FinSet, s2::FinSet) = ...

We should not define a such a method. Do we want the product? The disjoint union? In those cases we really ought be explicit about which implementation we intend.

Function interfaces

Let’s look at the theory for functions in the new Catlab refactor, starting with a core theory shared by SetFunction, FinFunction, and FinDomFunction:

@theory ThFunctionCore begin
  Dom::TYPE
  Cod::TYPE
  app(e::Dom)::Cod
end

The ThFunctionCore interface states that we require function implementations to apply a function to some Julia type Dom to get elements of some other Julia type Codom.

abstract type SetFunction′ end # *only* subtyped by SetFunction

@theory ThSetFunction <: ThFunctionCore begin
  Fun′::TYPE{SetFunction′}
  DomSet::TYPE{SetOb}
  CodSet::TYPE{SetOb}
  dom()::DomSet # eltype(dom()) <: Dom
  codom()::CodSet # eltype(codom()) <: Cod
  postcompose(t::Fun′)::Fun′
end

ThSetFunction.Meta.@wrapper SetFunction

Implementations of the theory of ThSetFunction can be understand as morphisms in \mathsf{Set}. For these we require that one must supply a (co)domain SetOb⁴ and be able to postcompose another function. When we eventually compose these SetFunctions (in \mathsf{Set}), the immediate result will be a sequence of functions. However, for performance considerations, we’ll want to be able to evaluate this sequence into a single SetFunction (via a force method which calls the underlying postcompose methods). Being able to repeatedly post-compose the first function in such a sequence is sufficient for this task and is often a more natural choice than precomposing.⁵

We can overload the call syntax of Julia to use the app function.

(f::SetFunction)(x) = ThSetFunction.app(f, x)

The theory of functions, now thought of as living in \mathsf{FinSet}, is very similar:

abstract type FinFunction′ end # *only* subtyped by FinFunction

@theory ThFinFunction <: ThFunctionCore begin
  Fun′::TYPE{FinFunction′}
  DomSet::TYPE{FinSet}
  CodSet::TYPE{FinSet}
  dom()::DomSet # eltype(dom()) <: Dom
  codom()::CodSet # eltype(codom()) <: Cod
  postcompose(t::Fun′)::Fun′
end

ThFinFunction.Meta.@wrapper FinFunction <: FinFunction′

Note in both cases we did use an abstract type to avoid a chicken-egg problem: in the theory of finite functions we need to refer to the wrapper type for models of the theory of finite functions (which we can’t really define until the theory has been defined). Because only FinFunction type subtypes FinFunction′, we can treat the two types as equivalent.

The theory for a FinDomFunction is similar, where DomSet must be a FinSet but CodSet must be a SetOb.

Function instances

Let’s see a couple models of these theories to get a sense of them:

struct IdentityFunction{S<:AbsSet, T}
  set::S
  IdentityFunction(d::S) where S<:AbsSet = new{S, eltype(d)}(d)
end

@instance ThFinFunction{T,T} [model::IdentityFunction{FinSet, T}] where T begin
  dom()::FinSet = model.set
  codom()::FinSet = model.set
  app(i::T)::T = i
  postcompose(f::FinFunction′)::FinFunction′ = f
end

@instance ThSetFunction{T,T} [model::IdentityFunction{SetOb,T}] where T begin
  dom()::SetOb = model.set
  codom()::SetOb = model.set
  app(i::T)::T = i
  postcompose(f::SetFunction′)::SetFunction′ = f
end

struct FinFunctionVector{S<:AbsSet,T}
  val::AbstractVector
  codom::S
  FinFunctionVector(val::AbstractVector,codom::S) where {S<:AbsSet} =
    new{S,eltype(codom)}(val, codom)
end

@instance ThFinFunction{Int,T} [model::FinFunctionVector{FinSet,T}] where T begin
  dom()::FinSet = FinSet(length(model.val))
  codom()::FinSet = model.codom
  app(i::Int)::T = model.val[i]
  postcompose(f::FinFunction′)::FinFunction′ =
    FinFunction(FinFunctionVector(f.(model.val), codom(f)))
end

@instance ThFinDomFunction{Int,T} [model::FinFunctionVector{SetOb,T}] where T begin
  dom()::FinSet = FinSet(length(model.val))
  codom()::SetOb = model.codom
  app(i::Int)::T = model.val[i]
  postcompose(f::SetFunction)::FinDomFunction =
    FinDomFunction(FinFunctionVector(f.(model.val), codom(f)))
end

File structure and future posts

The v0.16 to v0.17 refactor is concentrated on Catlab’s CategoricalAlgebra module. This was a folder with about 15 files in it, including FinCats (826 Lines Of Code), FinSets (1507 LOC), CSets (1418 LOC), FunctorialDataMigrations (456 LOC).

In the refactored version, these large files have been broken down into smaller ones which for the most part either declare a theory or declare a data structure and show how that data structure is a model of various theories. Another major structural change is to subdivide this into a sequence of modules:

1. Cats (general machinery for categories, functors, limits, etc.)
2. SetCats (specializing machinery in Cats to Set-like categories, including FinSet)
3. Pointwise (specializing machinery in Cats to \mathsf{C}-Set-like categories, such as ACSets and VarACSets).

We’ll cover these in a follow-up blog post!