Wiring diagrams for dagger categories and compact closed categories

docs/literate/graphics/composejl_wiring_diagrams.jl

@@ -61,8 +61,7 @@ to_composejl(mcopy(A)⋅(f⊗f)⋅mmerge(B))
 
 # The unit and co-unit of a compact closed category appear as caps and cups.
 
-A, B = Ob(FreeBicategoryRelations, :A, :B)
-f = Hom(:f, A, B)
+A, B = Ob(FreeCompactClosedCategory, :A, :B)
 
 to_composejl(dunit(A))
 #-
@@ -72,6 +71,9 @@ to_composejl(dcounit(A))
 # every morphism $f: A \to B$ has a transpose $f^\dagger: B \to A$ given by
 # bending wires:
 
+A, B = Ob(FreeBicategoryRelations, :A, :B)
+f = Hom(:f, A, B)
+
 to_composejl((dunit(A) ⊗ id(B)) ⋅ (id(A) ⊗ f ⊗ id(B)) ⋅ (id(A) ⊗ dcounit(B)))
 
 # ## Custom styles

docs/literate/graphics/tikz_wiring_diagrams.jl

@@ -65,17 +65,19 @@ to_tikz(mcopy(A)⋅(f⊗f)⋅mmerge(B), labels=true)
 
 # The unit and co-unit of a compact closed category appear as caps and cups.
 
-A, B = Ob(FreeBicategoryRelations, :A, :B)
-f = Hom(:f, A, B)
+A, B = Ob(FreeCompactClosedCategory, :A, :B)
 
-to_tikz(dunit(A))
+to_tikz(dunit(A), arrowtip="Stealth", labels=true)
 #-
-to_tikz(dcounit(A))
+to_tikz(dcounit(A), arrowtip="Stealth", labels=true)
 
 # In a self-dual compact closed category, such as a bicategory of relations,
 # every morphism $f: A \to B$ has a transpose $f^\dagger: B \to A$ given by
 # bending wires:
 
+A, B = Ob(FreeBicategoryRelations, :A, :B)
+f = Hom(:f, A, B)
+
 to_tikz((dunit(A) ⊗ id(B)) ⋅ (id(A) ⊗ f ⊗ id(B)) ⋅ (id(A) ⊗ dcounit(B)))
 
 # ## Custom styles

src/core/Rewrite.jl

@@ -4,8 +4,9 @@ The current content of this module is just a stopgap until I can implement
 a generic term rewriting system.
 """
 module Rewrite
-export associate, associate_unit, distribute_unary, anti_involute
+export associate, associate_unit, distribute_unary, involute
 
+using Compat
 using ..Syntax
 
 """ Simplify associative binary operation.
@@ -31,36 +32,29 @@ function associate_unit(expr::GATExpr, unit::Function)::GATExpr
   else associate(expr) end
 end
 
-""" Distribute unary operation over a binary operation.
+""" Distribute unary operation over binary operation.
 """
-function distribute_unary(raw_expr::GATExpr, un_op::Function,
-                          bin_op::Function)::GATExpr
-  if head(raw_expr) != nameof(un_op)
-    return raw_expr
-  end
-  expr = first(raw_expr)
-  if head(expr) == nameof(bin_op)
-    bin_op([un_op(A) for A in args(expr)]...)
+function distribute_unary(expr::GATExpr, unary::Function, binary::Function;
+                          unit::Union{Function,Nothing}=nothing,
+                          contravariant::Bool=false)::GATExpr
+  if (head(expr) != nameof(unary)) return expr end
+  @assert length(args(expr)) == 1
+  arg = first(expr)
+  if head(arg) == nameof(binary)
+    binary(map(unary, (contravariant ? reverse : identity)(args(arg))))
+  elseif !isnothing(unit) && head(arg) == nameof(unit)
+    arg
   else
-    raw_expr
+    expr
   end
 end
 
-""" Simplify unary operation that is an anti-involution on a (typed) monoid.
-""" 
-function anti_involute(raw_expr::GATExpr, inv::Function, op::Function,
-                       unit::Function)::GATExpr
-  if head(raw_expr) != nameof(inv)
-    return raw_expr
-  end
-  expr = first(raw_expr)
-  if head(expr) == nameof(inv)
-    first(expr)
-  elseif head(expr) == nameof(op)
-    op([inv(A) for A in reverse(args(expr))]...)
-  elseif head(expr) == nameof(unit)
-    expr
-  else raw_expr end
+""" Simplify involutive unary operation.
+"""
+function involute(expr::GATExpr)
+  @assert length(args(expr)) == 1
+  arg = first(expr)
+  head(expr) == head(arg) ? first(arg) : expr
 end
 
 end

src/core/Syntax.jl

@@ -535,13 +535,21 @@ end
 
 function show_latex_infix(io::IO, expr::GATExpr, op::String;
                           paren::Bool=false, kw...)
-  show_latex_paren(io, expr) = show_latex(io, expr; paren=true, kw...)
+  show_latex_paren(io, expr) = show_latex(io, expr, paren=true)
   sep = op == " " ? op : " $op "
   if (paren) print(io, "\\left(") end
   join(io, [sprint(show_latex_paren, arg) for arg in args(expr)], sep)
   if (paren) print(io, "\\right)") end
 end
 
+function show_latex_postfix(io::IO, expr::GATExpr, op::String; kw...)
+  @assert length(args(expr)) == 1
+  print(io, "{")
+  show_latex(io, first(expr), paren=true)
+  print(io, "}")
+  print(io, op)
+end
+
 function show_latex_script(io::IO, expr::GATExpr, head::String;
                            super::Bool=false, kw...)
   print(io, head, super ? "^" : "_", "{")

src/doctrines/Monoidal.jl

@@ -6,8 +6,9 @@ export MonoidalCategory, otimes, munit, ⊗, collect, ndims,
   mmerge, create, copair, incl1, incl2, ∇, □,
   MonoidalCategoryWithBidiagonals, BiproductCategory, FreeBiproductCategory,
   CartesianClosedCategory, FreeCartesianClosedCategory, hom, ev, curry,
-  CompactClosedCategory, FreeCompactClosedCategory, dual, dunit, dcounit,
+  CompactClosedCategory, FreeCompactClosedCategory, dual, dunit, dcounit, mate,
   DaggerCategory, FreeDaggerCategory, dagger,
+  DaggerSymmetricMonoidalCategory, FreeDaggerSymmetricMonoidalCategory,
   DaggerCompactCategory, FreeDaggerCompactCategory
 
 import Base: collect, ndims
@@ -211,7 +212,8 @@ intended to mean a monoidal category with coherent diagonals and codiagonals.
 Unlike in a biproduct category, the naturality axioms need not be satisfied.
 
 FIXME: This signature should extend both `MonoidalCategoryWithDiagonals` and
-`MonoidalCategoryWithCodiagonals`, but we don't support multiple inheritance.
+`MonoidalCategoryWithCodiagonals`, but multiple inheritance is not yet
+supported.
 """
 @signature SymmetricMonoidalCategory(Ob,Hom) => MonoidalCategoryWithBidiagonals(Ob,Hom) begin
   mcopy(A::Ob)::Hom(A,otimes(A,A))
@@ -231,8 +233,8 @@ end
 Also known as a *semiadditive category*.
 
 FIXME: This signature should extend `MonoidalCategoryWithBidiagonals`,
-`CartesianCategory`, and `CocartesianCategory`, but we don't support multiple
-inheritance.
+`CartesianCategory`, and `CocartesianCategory`, but multiple inheritance is not
+yet supported.
 """
 @signature MonoidalCategoryWithBidiagonals(Ob,Hom) => BiproductCategory(Ob,Hom) begin
   pair(f::Hom(A,B), g::Hom(A,C))::Hom(A,otimes(B,C)) <= (A::Ob, B::Ob, C::Ob)
@@ -289,8 +291,9 @@ See also `FreeCartesianCategory`.
 end
 
 function show_latex(io::IO, expr::ObExpr{:hom}; kw...)
-  show_latex(io, last(expr))
-  print(io, "^{")
+  print(io, "{")
+  show_latex(io, last(expr), paren=true)
+  print(io, "}^{")
   show_latex(io, first(expr))
   print(io, "}")
 end
@@ -317,71 +320,116 @@ end
   # Counit of duality, aka the evaluation map
   dcounit(A::Ob)::Hom(otimes(A,dual(A)), munit())
 
+  # Adjoint mate of morphism f.
+  mate(f::Hom(A,B))::Hom(dual(B),dual(A)) <= (A::Ob, B::Ob)
+
   # Closed monoidal category
   hom(A::Ob, B::Ob) = otimes(B, dual(A))
   ev(A::Ob, B::Ob) = otimes(id(B), compose(braid(dual(A),A), dcounit(A)))
   curry(A::Ob, B::Ob, f::Hom) = compose(
     otimes(id(A), compose(dunit(B), braid(dual(B),B))),
-    otimes(f, id(dual(B)))
-  )
+    otimes(f, id(dual(B))))
 end
 
 @syntax FreeCompactClosedCategory(ObExpr,HomExpr) CompactClosedCategory begin
-  dual(A::Ob) = anti_involute(Super.dual(A), dual, otimes, munit)
+  dual(A::Ob) = distribute_unary(involute(Super.dual(A)), dual, otimes,
+                                 unit=munit, contravariant=true)
   otimes(A::Ob, B::Ob) = associate_unit(Super.otimes(A,B), munit)
   otimes(f::Hom, g::Hom) = associate(Super.otimes(f,g))
   compose(f::Hom, g::Hom) = associate(Super.compose(f,g; strict=true))
+  mate(f::Hom) = distribute_mate(involute(Super.mate(f)))
+end
+
+""" Distribute adjoint mates over composition and products.
+"""
+function distribute_mate(f::HomExpr)
+  distribute_unary(
+    distribute_unary(f, mate, compose, contravariant=true),
+    mate, otimes, contravariant=true)
 end
 
 function show_latex(io::IO, expr::ObExpr{:dual}; kw...)
-  show_latex(io, first(expr))
-  print(io, "^*")
+  Syntax.show_latex_postfix(io, expr, "^*")
 end
 function show_latex(io::IO, expr::HomExpr{:dunit}; kw...)
   Syntax.show_latex_script(io, expr, "\\eta")
 end
 function show_latex(io::IO, expr::HomExpr{:dcounit}; kw...)
   Syntax.show_latex_script(io, expr, "\\varepsilon")
 end
+function show_latex(io::IO, expr::HomExpr{:mate}; kw...)
+  Syntax.show_latex_postfix(io, expr, "^*")
+end
 
 # Dagger category
 #################
 
 """ Doctrine of *dagger category*
 """
 @signature Category(Ob,Hom) => DaggerCategory(Ob,Hom) begin
-  dagger(f::Hom(A,B))::Hom(B,A) <= (A::Ob,B::Ob)
+  dagger(f::Hom(A,B))::Hom(B,A) <= (A::Ob, B::Ob)
 end
 
 @syntax FreeDaggerCategory(ObExpr,HomExpr) DaggerCategory begin
   compose(f::Hom, g::Hom) = associate(Super.compose(f,g; strict=true))
-  dagger(f::Hom) = anti_involute(Super.dagger(f), dagger, compose, id)
+  dagger(f::Hom) = distribute_dagger(involute(Super.dagger(f)))
+end
+
+""" Distribute dagger over composition.
+"""
+function distribute_dagger(f::HomExpr)
+  distribute_unary(f, dagger, compose, unit=id, contravariant=true)
+end
+
+""" Doctrine of *dagger symmetric monoidal category*
+
+Also known as a [symmetric monoidal dagger
+category](https://ncatlab.org/nlab/show/symmetric+monoidal+dagger-category).
+
+FIXME: This signature should extend both `DaggerCategory` and
+`SymmetricMonoidalCategory`, but multiple inheritance is not yet supported.
+"""
+@signature SymmetricMonoidalCategory(Ob,Hom) => DaggerSymmetricMonoidalCategory(Ob,Hom) begin
+  dagger(f::Hom(A,B))::Hom(B,A) <= (A::Ob, B::Ob)
+end
+
+@syntax FreeDaggerSymmetricMonoidalCategory(ObExpr,HomExpr) DaggerSymmetricMonoidalCategory begin
+  otimes(A::Ob, B::Ob) = associate_unit(Super.otimes(A,B), munit)
+  otimes(f::Hom, g::Hom) = associate(Super.otimes(f,g))
+  compose(f::Hom, g::Hom) = associate(Super.compose(f,g; strict=true))
+  dagger(f::Hom) = distribute_unary(distribute_dagger(involute(Super.dagger(f))),
+                                    dagger, otimes)
 end
 
 """ Doctrine of *dagger compact category*
 
+In a dagger compact category, there are two kinds of adjoints of a morphism
+`f::Hom(A,B)`, the adjoint mate `mate(f)::Hom(dual(B),dual(A))` and the dagger
+adjoint `dagger(f)::Hom(B,A)`. In the category of Hilbert spaces, these are
+respectively the Banach space adjoint and the Hilbert space adjoint (Reed-Simon,
+Vol I, Sec VI.2). In Julia, they would correspond to `transpose` and `adjoint`
+in the official `LinearAlegbra` module. For the general relationship between
+mates and daggers, see Selinger's survey of graphical languages for monoidal
+categories.
+
 FIXME: This signature should extend both `DaggerCategory` and
-`CompactClosedCategory`, but we don't support multiple inheritance yet.
+`CompactClosedCategory`, but multiple inheritance is not yet supported.
 """
 @signature CompactClosedCategory(Ob,Hom) => DaggerCompactCategory(Ob,Hom) begin
-  dagger(f::Hom(A,B))::Hom(B,A) <= (A::Ob,B::Ob)
+  dagger(f::Hom(A,B))::Hom(B,A) <= (A::Ob, B::Ob)
 end
 
 @syntax FreeDaggerCompactCategory(ObExpr,HomExpr) DaggerCompactCategory begin
-  dual(A::Ob) = anti_involute(Super.dual(A), dual, otimes, munit)
+  dual(A::Ob) = distribute_unary(involute(Super.dual(A)), dual, otimes,
+                                 unit=munit, contravariant=true)
   otimes(A::Ob, B::Ob) = associate_unit(Super.otimes(A,B), munit)
   otimes(f::Hom, g::Hom) = associate(Super.otimes(f,g))
   compose(f::Hom, g::Hom) = associate(Super.compose(f,g; strict=true))
-  function dagger(f::Hom)
-    f = anti_involute(Super.dagger(f), dagger, compose, id)
-    distribute_unary(f, dagger, otimes)
-  end
+  dagger(f::Hom) = distribute_unary(distribute_dagger(involute(Super.dagger(f))),
+                                    dagger, otimes)
+  mate(f::Hom) = distribute_mate(involute(Super.mate(f)))
 end
 
 function show_latex(io::IO, expr::HomExpr{:dagger}; kw...)
-  f = first(expr)
-  if (head(f) != :generator) print(io, "\\left(") end
-  show_latex(io, f)
-  if (head(f) != :generator) print(io, "\\right)") end
-  print(io, "^\\dagger")
+  Syntax.show_latex_postfix(io, expr, "^\\dagger")
 end

src/doctrines/Relations.jl

@@ -32,12 +32,8 @@ end
   otimes(A::Ob, B::Ob) = associate_unit(Super.otimes(A,B), munit)
   otimes(f::Hom, g::Hom) = associate(Super.otimes(f,g))
   compose(f::Hom, g::Hom) = associate(Super.compose(f,g; strict=true))
-
-  function dagger(f::Hom)
-    f = anti_involute(Super.dagger(f), dagger, compose, id)
-    distribute_unary(f, dagger, otimes)
-  end
-
+  dagger(f::Hom) = distribute_unary(distribute_dagger(involute(Super.dagger(f))),
+                                    dagger, otimes)
   meet(f::Hom, g::Hom) = compose(mcopy(dom(f)), otimes(f,g), mmerge(codom(f)))
   top(A::Ob, B::Ob) = compose(delete(A), create(B))
 end
@@ -63,12 +59,8 @@ end
   otimes(A::Ob, B::Ob) = associate_unit(Super.otimes(A,B), munit)
   otimes(f::Hom, g::Hom) = associate(Super.otimes(f,g))
   compose(f::Hom, g::Hom) = associate(Super.compose(f,g; strict=true))
-
-  function dagger(f::Hom)
-    f = anti_involute(Super.dagger(f), dagger, compose, id)
-    distribute_unary(f, dagger, otimes)
-  end
-
+  dagger(f::Hom) = distribute_unary(distribute_dagger(involute(Super.dagger(f))),
+                                    dagger, otimes)
   meet(f::Hom, g::Hom) = compose(mcopy(dom(f)), otimes(f,g), mmerge(codom(f)))
   top(A::Ob, B::Ob) = compose(delete(A), create(B))
 end

src/graphics/ComposeWiringDiagrams.jl

@@ -10,9 +10,9 @@ const C = Compose
 
 using ...WiringDiagrams
 using ..WiringDiagramLayouts
-using ..WiringDiagramLayouts: AbstractVector2D, Vector2D,
-  BoxShape, RectangleShape, JunctionShape, NoShape,
-  position, size, lower_corner, upper_corner, normal, tangent, wire_points
+using ..WiringDiagramLayouts: AbstractVector2D, Vector2D, BoxShape,
+  RectangleShape, JunctionShape, NoShape, box_label, position, size,
+  lower_corner, upper_corner, normal, tangent, wire_points
 
 # Data types
 ############
@@ -130,7 +130,7 @@ function render_box(shape::BoxShape, value::Any, opts::ComposeOptions)
   render_box(Val(shape), value, opts)
 end
 function render_box(::Val{RectangleShape}, value::Any, opts::ComposeOptions)
-  labeled_rectangle(string(value), rounded=opts.rounded_boxes,
+  labeled_rectangle(box_label(value), rounded=opts.rounded_boxes,
     rect_props=opts.box_props, text_props=opts.text_props)
 end
 function render_box(::Val{JunctionShape}, ::Any, opts::ComposeOptions)