Merge pull request #459 from epatters/monoidal-from-limits

(Co)cartesian category instances from (co)products

src/categorical_algebra/CSets.jl

@@ -450,6 +450,9 @@ end
 
 fin_sets(X::ACSet) = map(table -> FinSet(length(table)), tables(X))
 
+@cartesian_monoidal_instance CSet CSetTransformation
+@cocartesian_monoidal_instance ACSet ACSetTransformation
+
 # Limits and colimits
 #####################
 
@@ -598,8 +601,9 @@ cocone_objects(diagram::BipartiteFreeDiagram) = ob₂(diagram)
 cocone_objects(span::Multispan) = feet(span)
 cocone_objects(para::ParallelMorphisms) = SVector(codom(para))
 
-# Serialization and Deserialization of ACSets
-#############################################
+# Serialization
+###############
+
 """ Serialize an ACSet object to a JSON string
 """
 function generate_json_acset(x::T) where T <: AbstractACSet

src/categorical_algebra/FinSets.jl

@@ -13,7 +13,8 @@ import StaticArrays
 using StaticArrays: StaticVector, SVector, SizedVector, similar_type
 
 @reexport using ..Sets
-using ...Theories, ...CSetDataStructures, ...Graphs, ..FreeDiagrams, ..Limits
+using ...GAT, ...Theories
+using ...CSetDataStructures, ...Graphs, ..FreeDiagrams, ..Limits
 import ...Theories: dom, codom
 import ..Limits: limit, colimit, universal
 using ..Sets: SetFunctionCallable, SetFunctionIdentity
@@ -146,6 +147,10 @@ Base.show(io::IO, f::FinFunctionVector) =
 Sets.compose_impl(f::FinFunctionVector, g::FinDomFunctionVector) =
   FinDomFunctionVector(g.func[f.func], codom(g))
 
+# Note: Cartesian monoidal structure is implemented generically for Set but
+# cocartesian only for FinSet.
+@cocartesian_monoidal_instance FinSet FinFunction
+
 # Indexed functions
 #------------------
 

src/categorical_algebra/Limits.jl

@@ -11,6 +11,7 @@ export AbstractLimit, AbstractColimit, Limit, Colimit,
   BinaryCoproduct, Coproduct, coproduct, coproj1, coproj2, copair,
   BinaryPushout, Pushout, pushout,
   BinaryCoequalizer, Coequalizer, coequalizer, proj,
+  @cartesian_monoidal_instance, @cocartesian_monoidal_instance,
   ComposeProductEqualizer, ComposeCoproductCoequalizer
 
 using AutoHashEquals
@@ -258,6 +259,92 @@ define the method `universal(::Coequalizer{T}, ::SMulticospan{1,T})`.
 factorize(lim::Equalizer, h) = universal(lim, SMultispan{1}(h))
 factorize(colim::Coequalizer, h) = universal(colim, SMulticospan{1}(h))
 
+# (Co)cartesian monoidal categories
+###################################
+
+""" Define cartesian monoidal structure using limits.
+
+Implements an instance of [`CartesianCategory`](@ref) assuming that finite
+products have been implemented following the limits interface.
+"""
+macro cartesian_monoidal_instance(Ob, Hom)
+  esc(quote
+    import Catlab.Theories: CartesianCategory, otimes, ⊗, munit, braid, σ,
+      mcopy, delete, pair, proj1, proj2, Δ, ◊
+
+    @instance CartesianCategory{$Ob, $Hom} begin
+      @import dom, codom, compose, ⋅, id, munit, delete, pair
+
+      otimes(A::$Ob, B::$Ob) = ob(product(A, B))
+
+      function otimes(f::$Hom, g::$Hom)
+        π1, π2 = product(dom(f), dom(g))
+        pair(product(codom(f), codom(g)), π1⋅f, π2⋅g)
+      end
+
+      function braid(A::$Ob, B::$Ob)
+        AB, BA = product(A, B), product(B, A)
+        pair(BA, proj2(AB), proj1(AB))
+      end
+
+      mcopy(A::$Ob) = pair(id(A),id(A))
+      proj1(A::$Ob, B::$Ob) = proj1(product(A, B))
+      proj2(A::$Ob, B::$Ob) = proj2(product(A, B))
+    end
+
+    otimes(As::AbstractVector{<:$Ob}) = ob(product(As))
+
+    function otimes(fs::AbstractVector{<:$Hom})
+      Π, Π′ = product(map(dom, fs)), product(map(codom, fs))
+      pair(Π′, map(compose, legs(Π), fs))
+    end
+
+    munit(::Type{T}) where T <: $Ob = ob(terminal(T))
+  end)
+end
+
+""" Define cocartesian monoidal structure using colimits.
+
+Implements an instance of [`CocartesianCategory`](@ref) assuming that finite
+coproducts have been implemented following the colimits interface.
+"""
+macro cocartesian_monoidal_instance(Ob, Hom)
+  esc(quote
+    import Catlab.Theories: CocartesianCategory, oplus, ⊕, mzero, swap,
+      plus, zero, copair, coproj1, coproj2
+
+    @instance CocartesianCategory{$Ob, $Hom} begin
+      @import dom, codom, compose, ⋅, id, mzero, copair
+
+      oplus(A::$Ob, B::$Ob) = ob(coproduct(A, B))
+
+      function oplus(f::$Hom, g::$Hom)
+        ι1, ι2 = coproduct(codom(f), codom(g))
+        copair(coproduct(dom(f), dom(g)), f⋅ι1, g⋅ι2)
+      end
+
+      function swap(A::$Ob, B::$Ob)
+        AB, BA = coproduct(A, B), coproduct(B, A)
+        copair(AB, coproj2(BA), coproj1(BA))
+      end
+
+      plus(A::$Ob) = copair(id(A),id(A))
+      zero(A::$Ob) = create(A)
+      coproj1(A::$Ob, B::$Ob) = coproj1(coproduct(A, B))
+      coproj2(A::$Ob, B::$Ob) = coproj2(coproduct(A, B))
+    end
+
+    oplus(As::AbstractVector{<:$Ob}) = ob(coproduct(As))
+
+    function oplus(fs::AbstractVector{<:$Hom})
+      ⊔, ⊔′ = coproduct(map(dom, fs)), coproduct(map(codom, fs))
+      copair(⊔, map(compose, fs, legs(⊔′)))
+    end
+
+    mzero(::Type{T}) where T <: $Ob = ob(initial(T))
+  end)
+end
+
 # Composite (co)limits
 ######################
 

src/categorical_algebra/Sets.jl

@@ -173,6 +173,8 @@ compose_impl(c::ConstantFunction, f::SetFunction) =
 compose_impl(c::ConstantFunction, d::ConstantFunction) =
   ConstantFunction(d.value, dom(c), codom(d))
 
+@cartesian_monoidal_instance SetOb SetFunction
+
 # Limits
 ########
 

src/core/GAT.jl

@@ -634,15 +634,12 @@ end
 """ Julia functions for term and type aliases of GAT.
 """
 function alias_functions(theory::Theory)::Vector{JuliaFunction}
-  # collect all of the types and terms from the theory
-  terms_types = [theory.types; theory.terms]
-  # iterate over the specified aliases
   collect(Iterators.flatten(map(collect(theory.aliases)) do alias
     # collect all of the destination function definitions to alias
     # allows an alias to overite all the type definitions of a function
-    dests = filter(i -> i.name == last(alias), map(x -> x, terms_types))
+    dests = filter(term -> term.name == last(alias), theory.terms)
     # If there are no matching functions, throw a parse error
-    if isempty(dests)
+    if isempty(dests) && !any(type.name == last(alias) for type in theory.types)
       throw(ParseError("Cannot alias undefined type or term $alias"))
     end
     # For each destination, create a Julia function

src/theories/Category.jl

@@ -44,7 +44,7 @@ We use symbol ⋅ (\\cdot) for diagrammatic composition: f⋅g = compose(f,g).
 end
 
 # Convenience constructors
-compose(fs::Vector) = foldl(compose, fs)
+compose(fs::AbstractVector) = foldl(compose, fs)
 compose(f, g, h, fs...) = compose([f, g, h, fs...])
 
 @syntax FreeCategory{ObExpr,HomExpr} Category begin

src/theories/HigherCategory.jl

@@ -32,7 +32,7 @@ abstract type HomHExpr{T} <: CategoryExpr{T} end
 end
 
 # Convenience constructors
-composeH(αs::Vector) = foldl(composeH, αs)
+composeH(αs::AbstractVector) = foldl(composeH, αs)
 composeH(α, β, γ, αs...) = composeH([α, β, γ, αs...])
 
 """ Syntax for a 2-category.
@@ -119,7 +119,7 @@ end
 end
 
 # Convenience constructors
-composeV(αs::Vector) = foldl(composeV, αs)
+composeV(αs::AbstractVector) = foldl(composeV, αs)
 composeV(α, β, γ, αs...) = composeV([α, β, γ, αs...])
 
 """ Syntax for a double category.

src/theories/Monoidal.jl

@@ -52,7 +52,8 @@ theory for weak monoidal categories later.
 end
 
 # Convenience constructors
-otimes(xs::Vector{T}) where T = isempty(xs) ? munit(T) : foldl(otimes, xs)
+otimes(xs::AbstractVector{T}) where T =
+  isempty(xs) ? munit(T) : foldl(otimes, xs)
 otimes(x, y, z, xs...) = otimes([x, y, z, xs...])
 
 """ Collect generators of object in monoidal category as a vector.

src/theories/MonoidalAdditive.jl

@@ -25,7 +25,7 @@ notation.
 end
 
 # Convenience constructors
-oplus(xs::Vector{T}) where T = isempty(xs) ? mzero(T) : foldl(oplus, xs)
+oplus(xs::AbstractVector{T}) where T = isempty(xs) ? mzero(T) : foldl(oplus, xs)
 oplus(x, y, z, xs...) = oplus([x, y, z, xs...])
 
 # Overload `collect` and `ndims` as for multiplicative monoidal categories.

src/wiring_diagrams/Undirected.jl

@@ -10,7 +10,7 @@ export UndirectedWiringDiagram, UntypedUWD, TypedUWD,
 
 using ...Present, ...CategoricalAlgebra.CSets, ...CategoricalAlgebra.Limits
 using ...CategoricalAlgebra.FinSets: FinSet, FinFunction
-using ...Theories: dom, codom, compose, ⋅, id
+using ...Theories: dom, codom, compose, ⋅, id, oplus
 import ..DirectedWiringDiagrams: box, boxes, nboxes, add_box!, add_wire!,
   add_wires!, singleton_diagram, ocompose, substitute
 
@@ -305,9 +305,4 @@ end
 flat(x) = reduce(vcat, x, init=Int[])
 flatmap(f, xs...) = mapreduce(f, vcat, xs..., init=Int[])
 
-# FIXME: Should be defined in FinSets.
-function oplus(fs::AbstractVector{<:FinFunction})
-  copair(coproduct(map(dom, fs)), map(compose, fs, coproduct(map(codom, fs))))
-end
-
 end

test/categorical_algebra/CSets.jl

@@ -348,8 +348,8 @@ h = cycle_graph(LabeledGraph{Symbol}, 4, V=(label=[:c,:d,:a,:b],))
 h = cycle_graph(LabeledGraph{Symbol}, 4, V=(label=[:a,:b,:d,:c],))
 @test !is_homomorphic(g, h)
 
-# Serialization and Deserialization of ACSets
-#############################################
+# Serialization
+###############
 
 @present TheoryDDS(FreeSchema) begin
   X::Ob

test/categorical_algebra/FinSets.jl

@@ -278,6 +278,16 @@ colim = coproduct([FinSet(2), FinSet(3)])
 @test force(first(legs(colim)) ⋅ copair(colim,[f,g])) == f
 @test force(last(legs(colim)) ⋅ copair(colim,[f,g])) == g
 
+# Cocartesian monoidal structure.
+@test FinSet(2)⊕FinSet(3) == FinSet(5)
+@test oplus([FinSet(2), FinSet(3), FinSet(4)]) == FinSet(9)
+@test f⊕g == FinFunction([3,5,6,7,8], 10)
+@test mzero(FinSet{Int}) == FinSet(0)
+@test swap(FinSet(2), FinSet(3)) == FinFunction([4,5,1,2,3])
+ι1, ι2 = coproj1(FinSet(2),FinSet(3)), coproj2(FinSet(2),FinSet(3))
+@test ι1 == FinFunction([1,2], 5)
+@test ι2 == FinFunction([3,4,5], 5)
+
 # Coequalizers
 #-------------
 

test/categorical_algebra/Sets.jl

@@ -83,4 +83,19 @@ lim = product(fill(TypeSet(Int), 3))
 fs = [ SetFunction(x -> x+i, TypeSet(Int), TypeSet(Int)) for i in 1:3 ]
 @test pair(lim, fs)(3) == (4,5,6)
 
+# Cartesian monoidal structure.
+@test TypeSet(Int) ⊗ TypeSet(String) == TypeSet(Tuple{Int,String})
+@test munit(TypeSet) == TypeSet(Nothing)
+@test σ(TypeSet(Int), TypeSet(String))((1,"foo")) == ("foo",1)
+π1 = proj1(TypeSet(Int), TypeSet(String))
+π2 = proj2(TypeSet(Int), TypeSet(String))
+@test (π1((1,"foo")), π2((1,"foo"))) == (1,"foo")
+
+@test (f⊗g)((["foo"], ["bar", "baz"])) == (1, "barbaz")
+@test Δ(TypeSet(Int))(2) == (2,2)
+@test ◊(TypeSet(Int))(1) == nothing
+
+@test otimes(fill(TypeSet(Int), 3)) == TypeSet(Tuple{Int,Int,Int})
+@test otimes(fs)((1,5,10)) == (2,7,13)
+
 end

test/core/GAT.jl

@@ -192,10 +192,7 @@ accessors = [ GAT.JuliaFunction(:(dom(::Hom)), :Ob),
               GAT.JuliaFunction(:(codom(::Hom)), :Ob) ]
 constructors = [ GAT.JuliaFunction(:(id(X::Ob)), :Hom),
                  GAT.JuliaFunction(:(compose(f::Hom, g::Hom)), :Hom) ]
-alias_functions = [
-  GAT.JuliaFunction(:(⋅(f::Hom, g::Hom)), :Hom, :(compose(f, g))),
-  GAT.JuliaFunction(:(→(dom::Ob, codom::Ob)), :Hom, :(Hom(dom, codom))),
-]
+alias_functions = [ GAT.JuliaFunction(:(⋅(f::Hom, g::Hom)), :Hom, :(compose(f, g))) ]
 theory = GAT.theory(Category)
 @test GAT.accessors(theory) == accessors
 @test GAT.constructors(theory) == constructors