Updated standard library, tests, and documentation to adopt the new where clause notation

docs/src/apis/core.md

@@ -13,13 +13,13 @@ transformed, usually functorially, into more concrete representations, such as
 
 The basic elements of this system are:
 
-1. **Signatures** of generalized algebraic theories (GATs), defined using the 
+1. **Signatures** of generalized algebraic theories (GATs), defined using the
    [`@signature`](@ref) macro. Categories and other typed (multisorted)
    algebraic structures can be defined as GATs.
-   
+
 2. **Instances**, or concrete implementations, of signatures, asserted using the
    [`@instance`](@ref) macro.
-   
+
 3. **Syntax systems** for signatures, defined using the [`@syntax`](@ref) macro.
    These are type-safe expression trees constructed using ordinary Julia
    functions.
@@ -56,9 +56,9 @@ import Catlab.Doctrines: Ob, Hom, ObExpr, HomExpr, dom, codom, compose, id
 @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)
+  compose(f::Hom(A,B), g::Hom(B,C))::Hom(A,C) ⊣ (A::Ob, B::Ob, C::Ob)
 end
 nothing # hide
 ```
@@ -71,13 +71,14 @@ constructors*, `id` (identity) and `compose` (composition).
 
 Notice how the return types of the term constructors depend on the argument
 values. For example, the term `id(A)` has type `Hom(A,A)`. The term constructor
-`compose` also uses *context variables*, listed to the right of the `<=` symbol.
-This allows us to write `compose(f,g)`, instead of the more verbose
-`compose(A,B,C,f,g)` (for discussion, see Cartmell, 1986, Sec 10: Informal
-syntax).
+`compose` also uses *context variables*, listed to the right of the `⊣`
+symbol. These context variables can also be defined after a `where` clause,
+but the left hand side must be surrounded by parentheses. This allows us to
+write `compose(f,g)`, instead of the more verbose `compose(A,B,C,f,g)` (for
+discussion, see Cartmell, 1986, Sec 10: Informal syntax).
 
 !!! note
-    
+
     In general, a GAT consists of a *signature*, defining the types and terms of
     the theory, and a set of *axioms*, the equational laws satisfied by models
     of the theory. The theory of categories, for example, has axioms of
@@ -117,7 +118,7 @@ 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
@@ -223,8 +224,8 @@ import Catlab.Doctrines: Ob, Hom, ObExpr, HomExpr, SymmetricMonoidalCategory,
 @signature SymmetricMonoidalCategory(Ob,Hom) => CartesianCategory(Ob,Hom) begin
   mcopy(A::Ob)::Hom(A,otimes(A,A))
   delete(A::Ob)::Hom(A,munit())
-  
-  pair(f::Hom(A,B), g::Hom(A,C))::Hom(A,otimes(B,C)) <= (A::Ob, B::Ob, C::Ob)
+
+  pair(f::Hom(A,B), g::Hom(A,C))::Hom(A,otimes(B,C)) ⊣ (A::Ob, B::Ob, C::Ob)
   proj1(A::Ob, B::Ob)::Hom(otimes(A,B),A)
   proj2(A::Ob, B::Ob)::Hom(otimes(A,B),B)
 end

src/core/GAT.jl

@@ -63,7 +63,8 @@ end
   context::Context
   doc::Union{String,Nothing}
 
-  function AxiomConstructor(name::Symbol, left::Expr0, right::Expr0, context::Context, doc=nothing)
+  function AxiomConstructor(name::Symbol, left::Expr0, right::Expr0,
+                            context::Context, doc=nothing)
     new(name, left, right, context, doc)
   end
 end
@@ -73,6 +74,8 @@ end
 @auto_hash_equals struct Signature
   types::Vector{TypeConstructor}
   terms::Vector{TermConstructor}
+  axioms::Vector{AxiomConstructor}
+  aliases::Dict{Symbol, Symbol}
 end
 
 """ Typeclass = GAT signature + Julia-specific content.
@@ -122,8 +125,8 @@ macro signature(head, body)
   end
 
   # Parse signature body: GAT types/terms and extra Julia functions.
-  types, terms, functions, axioms = parse_signature_body(body)
-  signature = Signature(types, terms)
+  types, terms, functions, axioms, aliases = parse_signature_body(body)
+  signature = Signature(types, terms, axioms, aliases)
   class = Typeclass(head.main.name, head.main.params, signature, functions)
 
   # We must generate and evaluate the code at *run time* because the base
@@ -134,6 +137,7 @@ macro signature(head, body)
     :(Core.@__doc__ $(esc(head.main.name))))
 end
 function signature_code(main_class, base_mod, base_params)
+  # TODO: Generate code to do something with main_class.signature.axioms
   # Add types/terms/functions from base class, if provided.
   if isnothing(base_mod)
     class = main_class
@@ -143,7 +147,9 @@ function signature_code(main_class, base_mod, base_params)
     main_sig = main_class.signature
     base_sig = replace_types(bindings, base_class.signature)
     sig = Signature([base_sig.types; main_sig.types],
-                    [base_sig.terms; main_sig.terms])
+                    [base_sig.terms; main_sig.terms],
+                    [base_sig.axioms; main_sig.axioms],
+                    merge(base_sig.aliases, main_sig.aliases))
     functions = [ [ replace_symbols(bindings, f) for f in base_class.functions ];
                   main_class.functions ]
     class = Typeclass(main_class.name, main_class.type_params, sig, functions)
@@ -168,6 +174,9 @@ function signature_code(main_class, base_mod, base_params)
   fns = interface(class)
   toplevel = [ generate_function(replace_symbols(bindings, f)) for f in fns ]
 
+  # add to toplevel
+  toplevel = [toplevel; [Expr(:(=), Expr(:call, a, Expr(:..., :args)), Expr(:call, signature.aliases[a], Expr(:..., :args))) for a in keys(signature.aliases)]]
+
   # Modules must be at top level:
   # https://github.com/JuliaLang/julia/issues/21009
   Expr(:toplevel, mod, toplevel...)
@@ -194,13 +203,15 @@ end
 """
 function parse_signature_body(expr::Expr)
   @assert expr.head == :block
+  aliases = Dict{Symbol,Symbol}()
   types = OrderedDict{Symbol,TypeConstructor}()
   terms = TermConstructor[]
   axioms = AxiomConstructor[]
   funs = JuliaFunction[]
   for elem in strip_lines(expr).args
+    elem = replace_symbols(aliases, strip_lines(elem))
     head = last(parse_docstring(elem)).head
-    if head in (:(::), :call, :where)
+    if head in (:(::), :call, :comparison, :where)
       cons = parse_constructor(elem)
       if isa(cons, TypeConstructor)
         if haskey(types, cons.name)
@@ -215,11 +226,13 @@ function parse_signature_body(expr::Expr)
       end
     elseif head in (:(=), :function)
       push!(funs, parse_function(elem))
+    elseif head == :macrocall && elem.args[1] == Symbol("@op")
+      aliases[elem.args[3].value] = elem.args[2]
     else
       throw(ParseError("Ill-formed signature element $elem"))
     end
   end
-  return (collect(values(types)), terms, funs, axioms)
+  return (collect(values(types)), terms, funs, axioms, aliases)
 end
 
 """ Julia functions for type parameter accessors.
@@ -336,9 +349,10 @@ function parse_constructor(expr::Expr)::Union{TypeConstructor,TermConstructor,
   doc, expr = parse_docstring(expr)
   cons_expr, context = @match expr begin
     Expr(:call, [:<=, inner, context]) => (inner, parse_context(context))
+    Expr(:call, [:⊣, inner, context]) => (inner, parse_context(context))
+    Expr(:comparison, [cons_left, cons_sym, cons_right, :⊣, context]) => (
+      Expr(:call, cons_sym, cons_left, cons_right), parse_context(context))
     Expr(:where, [inner, context]) => (inner, parse_context(context))
-    Expr(cons_sym, [cons_left, Expr(:where, [cons_right, context])]) => (
-      Expr(cons_sym, cons_left, cons_right), parse_context(context))
     _ => (expr, Context())
   end
 
@@ -380,7 +394,9 @@ end
 """
 function replace_types(bindings::Dict, sig::Signature)::Signature
   Signature([ replace_types(bindings, t) for t in sig.types ],
-            [ replace_types(bindings, t) for t in sig.terms ])
+            [ replace_types(bindings, t) for t in sig.terms ],
+            [ replace_types(bindings, t) for t in sig.axioms ],
+            replace_types(bindings, sig.aliases))
 end
 function replace_types(bindings::Dict, cons::TypeConstructor)::TypeConstructor
   TypeConstructor(replace_symbols(bindings, cons.name), cons.params,
@@ -391,6 +407,16 @@ function replace_types(bindings::Dict, cons::TermConstructor)::TermConstructor
                   replace_symbols(bindings, cons.typ),
                   replace_types(bindings, cons.context), cons.doc)
 end
+function replace_types(bindings::Dict, cons::AxiomConstructor)::AxiomConstructor
+  AxiomConstructor(cons.name,
+                   replace_symbols(bindings, cons.left),
+                   replace_symbols(bindings, cons.right),
+                   replace_types(bindings, cons.context), cons.doc)
+end
+function replace_types(bindings::Dict, aliases::Dict)::Dict
+  Dict(a => replace_symbols(bindings, aliases[a])
+       for a in keys(aliases))
+end
 function replace_types(bindings::Dict, context::Context)::Context
   GAT.Context(((name => @match expr begin
     (Expr(:call, [sym::Symbol, args...]) =>

src/doctrines/Category.jl

@@ -24,16 +24,16 @@ We use symbol ⋅ (\\cdot) for diagrammatic composition: f⋅g = compose(f,g).
   Hom(dom::Ob,codom::Ob)::TYPE
 
   id(A::Ob)::Hom(A,A)
-  compose(f::Hom(A,B), g::Hom(B,C))::Hom(A,C) where (A::Ob, B::Ob, C::Ob)
+  compose(f::Hom(A,B), g::Hom(B,C))::Hom(A,C) ⊣ (A::Ob, B::Ob, C::Ob)
 
   # Unicode syntax
   ⋅(f::Hom, g::Hom) = compose(f, g)
   ∘(f::Hom, g::Hom) = compose(g, f)
 
   # Equivalency Axioms in a category
-  compose(compose(f,g),h) == compose(f,compose(g,h)) where (A::Ob, B::Ob, C::Ob, D::Ob, f::Hom(A,B), g::Hom(B,C), h::Hom(C,D))
-  compose(f,id(B)) == f where (A::Ob, B::Ob, f::Hom(A,B))
-  compose(id(A),f) == f where (A::Ob, B::Ob, f::Hom(A,B))
+  compose(compose(f,g),h) == compose(f,compose(g,h)) ⊣ (A::Ob, B::Ob, C::Ob, D::Ob, f::Hom(A,B), g::Hom(B,C), h::Hom(C,D))
+  compose(f,id(B)) == f ⊣ (A::Ob, B::Ob, f::Hom(A,B))
+  compose(id(A),f) == f ⊣ (A::Ob, B::Ob, f::Hom(A,B))
 end
 
 # Convenience constructors
@@ -78,15 +78,15 @@ end
 """
 @signature Category(Ob,Hom) => Category2(Ob,Hom,Hom2) begin
   """ 2-morphism in a 2-category """
-  Hom2(dom::Hom(A,B), codom::Hom(A,B))::TYPE <= (A::Ob, B::Ob)
+  Hom2(dom::Hom(A,B), codom::Hom(A,B))::TYPE ⊣ (A::Ob, B::Ob)
 
   # Hom categories: Vertical composition
-  id(f)::Hom2(f,f) <= (A::Ob, B::Ob, f::Hom(A,B))
-  compose(α::Hom2(f,g), β::Hom2(g,h))::Hom2(f,h) <=
+  id(f)::Hom2(f,f) ⊣ (A::Ob, B::Ob, f::Hom(A,B))
+  compose(α::Hom2(f,g), β::Hom2(g,h))::Hom2(f,h) ⊣
     (A::Ob, B::Ob, f::Hom(A,B), g::Hom(A,B), h::Hom(A,B))
 
   # Horizontal compostion
-  compose2(α::Hom2(f,g), β::Hom2(h,k))::Hom2(compose(f,h),compose(g,k)) <=
+  compose2(α::Hom2(f,g), β::Hom2(h,k))::Hom2(compose(f,h),compose(g,k)) ⊣
     (A::Ob, B::Ob, C::Ob, f::Hom(A,B), g::Hom(A,B), h::Hom(B,C), k::Hom(B,C))
 
   # Unicode syntax

src/doctrines/Monoidal.jl

@@ -25,10 +25,10 @@ signature for weak monoidal categories later.
 """
 @signature Category(Ob,Hom) => MonoidalCategory(Ob,Hom) begin
   otimes(A::Ob, B::Ob)::Ob
-  otimes(f::Hom(A,B), g::Hom(C,D))::Hom(otimes(A,C),otimes(B,D)) <=
+  otimes(f::Hom(A,B), g::Hom(C,D))::Hom(otimes(A,C),otimes(B,D)) ⊣
     (A::Ob, B::Ob, C::Ob, D::Ob)
   munit()::Ob
-  
+
   # Unicode syntax
   ⊗(A::Ob, B::Ob) = otimes(A, B)
   ⊗(f::Hom, g::Hom) = otimes(f, g)
@@ -109,7 +109,7 @@ References:
 @signature SymmetricMonoidalCategory(Ob,Hom) => MonoidalCategoryWithDiagonals(Ob,Hom) begin
   mcopy(A::Ob)::Hom(A,otimes(A,A))
   delete(A::Ob)::Hom(A,munit())
-  
+
   # Unicode syntax
   Δ(A::Ob) = mcopy(A)
   ◇(A::Ob) = delete(A)
@@ -121,7 +121,7 @@ Actually, this is a cartesian *symmetric monoidal* category but we omit these
 qualifiers for brevity.
 """
 @signature MonoidalCategoryWithDiagonals(Ob,Hom) => CartesianCategory(Ob,Hom) begin
-  pair(f::Hom(A,B), g::Hom(A,C))::Hom(A,otimes(B,C)) <= (A::Ob, B::Ob, C::Ob)
+  pair(f::Hom(A,B), g::Hom(A,C))::Hom(A,otimes(B,C)) ⊣ (A::Ob, B::Ob, C::Ob)
   proj1(A::Ob, B::Ob)::Hom(otimes(A,B),A)
   proj2(A::Ob, B::Ob)::Hom(otimes(A,B),B)
 end
@@ -136,7 +136,7 @@ Of course, this convention could be reversed.
   otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
   otimes(f::Hom, g::Hom) = associate(new(f,g))
   compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
-  
+
   pair(f::Hom, g::Hom) = compose(mcopy(dom(f)), otimes(f,g))
   proj1(A::Ob, B::Ob) = otimes(id(A), delete(B))
   proj2(A::Ob, B::Ob) = otimes(delete(A), id(B))
@@ -175,7 +175,7 @@ Actually, this is a cocartesian *symmetric monoidal* category but we omit these
 qualifiers for brevity.
 """
 @signature MonoidalCategoryWithCodiagonals(Ob,Hom) => CocartesianCategory(Ob,Hom) begin
-  copair(f::Hom(A,C), g::Hom(B,C))::Hom(otimes(A,B),C) <= (A::Ob, B::Ob, C::Ob)
+  copair(f::Hom(A,C), g::Hom(B,C))::Hom(otimes(A,B),C) ⊣ (A::Ob, B::Ob, C::Ob)
   incl1(A::Ob, B::Ob)::Hom(A,otimes(A,B))
   incl2(A::Ob, B::Ob)::Hom(B,otimes(A,B))
 end
@@ -190,7 +190,7 @@ Of course, this convention could be reversed.
   otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
   otimes(f::Hom, g::Hom) = associate(new(f,g))
   compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
-  
+
   copair(f::Hom, g::Hom) = compose(otimes(f,g), mmerge(codom(f)))
   incl1(A::Ob, B::Ob) = otimes(id(A), create(B))
   incl2(A::Ob, B::Ob) = otimes(create(A), id(B))
@@ -221,7 +221,7 @@ supported.
   mmerge(A::Ob)::Hom(otimes(A,A),A)
   delete(A::Ob)::Hom(A,munit())
   create(A::Ob)::Hom(munit(),A)
-  
+
   # Unicode syntax
   ∇(A::Ob) = mmerge(A)
   Δ(A::Ob) = mcopy(A)
@@ -238,8 +238,8 @@ FIXME: This signature should extend `MonoidalCategoryWithBidiagonals`,
 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)
-  copair(f::Hom(A,C), g::Hom(B,C))::Hom(otimes(A,B),C) <= (A::Ob, B::Ob, C::Ob)
+  pair(f::Hom(A,B), g::Hom(A,C))::Hom(A,otimes(B,C)) ⊣ (A::Ob, B::Ob, C::Ob)
+  copair(f::Hom(A,C), g::Hom(B,C))::Hom(otimes(A,B),C) ⊣ (A::Ob, B::Ob, C::Ob)
   proj1(A::Ob, B::Ob)::Hom(otimes(A,B),A)
   proj2(A::Ob, B::Ob)::Hom(otimes(A,B),B)
   incl1(A::Ob, B::Ob)::Hom(A,otimes(A,B))
@@ -269,12 +269,12 @@ A CCC is a cartesian category with internal homs (aka, exponential objects).
 @signature CartesianCategory(Ob,Hom) => CartesianClosedCategory(Ob,Hom) begin
   # Internal hom of A and B, an object representing Hom(A,B)
   hom(A::Ob, B::Ob)::Ob
-  
+
   # Evaluation map
   ev(A::Ob, B::Ob)::Hom(otimes(hom(A,B),A),B)
-  
+
   # Currying (aka, lambda abstraction)
-  curry(A::Ob, B::Ob, f::Hom(otimes(A,B),C))::Hom(A,hom(B,C)) <= (C::Ob)
+  curry(A::Ob, B::Ob, f::Hom(otimes(A,B),C))::Hom(A,hom(B,C)) ⊣ (C::Ob)
 end
 
 """ Syntax for a free cartesian closed category.
@@ -285,7 +285,7 @@ See also `FreeCartesianCategory`.
   otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
   otimes(f::Hom, g::Hom) = associate(new(f,g))
   compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
-  
+
   pair(f::Hom, g::Hom) = compose(mcopy(dom(f)), otimes(f,g))
   proj1(A::Ob, B::Ob) = otimes(id(A), delete(B))
   proj2(A::Ob, B::Ob) = otimes(delete(A), id(B))
@@ -314,16 +314,16 @@ end
 @signature SymmetricMonoidalCategory(Ob,Hom) => CompactClosedCategory(Ob,Hom) begin
   # Dual A^* of object A
   dual(A::Ob)::Ob
-  
+
   # Unit of duality, aka the coevaluation map
   dunit(A::Ob)::Hom(munit(), otimes(dual(A),A))
-  
+
   # 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)
-  
+  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)))
@@ -368,7 +368,7 @@ end
 """ 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
@@ -391,7 +391,7 @@ 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)
+  dagger(f::Hom(A,B))::Hom(B,A) ⊣ (A::Ob, B::Ob)
 end
 
 @syntax FreeDaggerSymmetricMonoidalCategory(ObExpr,HomExpr) DaggerSymmetricMonoidalCategory begin
@@ -417,7 +417,7 @@ FIXME: This signature should extend both `DaggerCategory` and
 `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