Repository: AlgebraicJulia/Catlab.jl
Pull request #237 (2020-08-10 22:25:14)

More conventional Julia syntax for GAT extension
I have implemented the change in the GAT parsing, and also converted a couple theories to the new syntax (right now, both syntaxes are supported). I can go convert the other theories, but I thought I'd get some feedback first.


Patch:
diff --git a/docs/src/apis/core.md b/docs/src/apis/core.md
index c66133011..e421c0318 100644
--- a/docs/src/apis/core.md
+++ b/docs/src/apis/core.md
@@ -51,7 +51,7 @@ import Catlab.Theories: Ob, Hom, ObExpr, HomExpr, dom, codom, compose, ⋅, id
 ```
 
 ```@example category
-@theory Category(Ob,Hom) begin
+@theory Category{Ob,Hom} begin
   @op begin
     (→) := Hom
     (⋅) := compose
@@ -132,7 +132,7 @@ struct MatrixDomain
   dim::Int
 end
 
-@instance Category(MatrixDomain, Matrix) begin
+@instance Category{MatrixDomain, Matrix} begin
   dom(M::Matrix) = MatrixDomain(eltype(M), size(M,1))
   codom(M::Matrix) = MatrixDomain(eltype(M), size(M,2))
 
@@ -171,7 +171,7 @@ Below, we subtype from Catlab's abstract types `ObExpr` and `HomExpr` to enable
 LaTeX pretty-printing and other convenient features, but this is not required.
 
 ```@example category
-@syntax CategoryExprs(ObExpr, HomExpr) Category begin
+@syntax CategoryExprs{ObExpr, HomExpr} Category begin
 end
 
 A, B, C, D = [ Ob(CategoryExprs.Ob, X) for X in [:A, :B, :C, :D] ]
@@ -198,7 +198,7 @@ $n$. The option `strict=true` tells Catlab to check that the domain and codomain
 objects are strictly equal and throw an error if they are not.
 
 ```@example category
-@syntax SimplifyingCategoryExprs(ObExpr, HomExpr) Category begin
+@syntax SimplifyingCategoryExprs{ObExpr, HomExpr} Category begin
   compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
 end
 
@@ -238,7 +238,7 @@ import Catlab.Theories: Ob, Hom, ObExpr, HomExpr, SymmetricMonoidalCategory,
 ```
 
 ```@example cartesian-monoidal-category
-@signature SymmetricMonoidalCategory(Ob,Hom) => CartesianCategory(Ob,Hom) begin
+@signature CartesianCategory{Ob,Hom} <: SymmetricMonoidalCategory{Ob,Hom} begin
   mcopy(A::Ob)::(A → (A ⊗ A))
   delete(A::Ob)::(A → munit())
 
@@ -252,7 +252,7 @@ nothing # hide
 We could then define the copying operation in terms of the pairing.
 
 ```@example cartesian-monoidal-category
-@syntax CartesianCategoryExprsV1(ObExpr,HomExpr) CartesianCategory begin
+@syntax CartesianCategoryExprsV1{ObExpr,HomExpr} CartesianCategory begin
   mcopy(A::Ob) = pair(id(A), id(A))
 end
 
@@ -264,7 +264,7 @@ Alternatively, we could define the pairing and projections in terms of the
 copying and deleting operations.
 
 ```@example cartesian-monoidal-category
-@syntax CartesianCategoryExprsV2(ObExpr,HomExpr) CartesianCategory begin
+@syntax CartesianCategoryExprsV2{ObExpr,HomExpr} CartesianCategory begin
   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))
diff --git a/experiments/CompAlgebra/src/AlgebraicNets.jl b/experiments/CompAlgebra/src/AlgebraicNets.jl
index b80b9e4c4..d3fb51cc8 100644
--- a/experiments/CompAlgebra/src/AlgebraicNets.jl
+++ b/experiments/CompAlgebra/src/AlgebraicNets.jl
@@ -33,12 +33,12 @@ import Catlab.Programs.GenerateJuliaPrograms: genvar, genvars, to_function_expr,
 
 TODO: Explain
 """
-@signature MonoidalCategoryWithBidiagonals(Ob,Hom) => AlgebraicNetTheory(Ob,Hom) begin
+@signature AlgebraicNetTheory{Ob,Hom} <: MonoidalCategoryWithBidiagonals{Ob,Hom} begin
   linear(x::Any, A::Ob, B::Ob)::(A → B)
   constant(x::Any, A::Ob)::(munit() → A)
 end
 
-@syntax AlgebraicNet(ObExpr,HomExpr) AlgebraicNetTheory begin
+@syntax AlgebraicNet{ObExpr,HomExpr} AlgebraicNetTheory begin
   # FIXME: `compose` and `otimes` should delegate to wiring layer when possible.
   compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
   otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
diff --git a/experiments/CompAlgebra/src/MathFormulas.jl b/experiments/CompAlgebra/src/MathFormulas.jl
index 7c7d43edb..7f383882b 100644
--- a/experiments/CompAlgebra/src/MathFormulas.jl
+++ b/experiments/CompAlgebra/src/MathFormulas.jl
@@ -99,7 +99,7 @@ end
 These methods should only be used with `gensym`-ed variables since they assume
 that any two formulas have disjoint variables.
 """
-@instance AlgebraicNetTheory(NFormula, Formulas) begin
+@instance AlgebraicNetTheory{NFormula, Formulas} begin
   dom(f::Formulas) = NFormula(length(f.inputs))
   codom(f::Formulas) = NFormula(length(f.terms))
 
diff --git a/experiments/Markov/src/MarkovCategories.jl b/experiments/Markov/src/MarkovCategories.jl
index 2e33741a3..41ef82617 100644
--- a/experiments/Markov/src/MarkovCategories.jl
+++ b/experiments/Markov/src/MarkovCategories.jl
@@ -13,12 +13,12 @@ import Catlab.Theories: Ob, Hom, dom, codom, compose, ⋅, ∘, otimes, ⊗, bra
 
 """ Theory of *Markov categories*
 """
-@signature MonoidalCategoryWithDiagonals(Ob,Hom) => MarkovCategory(Ob,Hom) begin
+@signature MarkovCategory{Ob,Hom} <: MonoidalCategoryWithDiagonals{Ob,Hom} begin
   expectation(M::(A → B))::(A → B) <= (A::Ob, B::Ob)
   @op (𝔼) := expectation
 end
 
-@syntax FreeMarkovCategory(ObExpr,HomExpr) MarkovCategory begin
+@syntax FreeMarkovCategory{ObExpr,HomExpr} MarkovCategory begin
   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))
diff --git a/src/categorical_algebra/FinRelations.jl b/src/categorical_algebra/FinRelations.jl
index 3f244b1f6..dc083b898 100644
--- a/src/categorical_algebra/FinRelations.jl
+++ b/src/categorical_algebra/FinRelations.jl
@@ -113,7 +113,7 @@ FIXME: Many methods only work for `FinRel{Int}`. The default methods should
 assume `FinRel{<:AbstractSet}` and the case `FinRel{Int}` should be handled
 specially.
 """
-@instance DistributiveBicategoryRelations(FinRel, FinRelation) begin
+@instance DistributiveBicategoryRelations{FinRel, FinRelation} begin
   dom(R::FinRelation) = R.dom
   codom(R::FinRelation) = R.codom
 
diff --git a/src/categorical_algebra/FinSets.jl b/src/categorical_algebra/FinSets.jl
index 2eb3b3297..0a9ceafb1 100644
--- a/src/categorical_algebra/FinSets.jl
+++ b/src/categorical_algebra/FinSets.jl
@@ -103,7 +103,7 @@ Base.collect(f::FinFunction) = force(f).func
 
 """ Category of finite sets and functions.
 """
-@instance Category(FinSet, FinFunction) begin
+@instance Category{FinSet, FinFunction} begin
   dom(f::FinFunction) = f.dom
   codom(f::FinFunction) = f.codom
   
diff --git a/src/categorical_algebra/Matrices.jl b/src/categorical_algebra/Matrices.jl
index a87168ed4..9ba81f01a 100644
--- a/src/categorical_algebra/Matrices.jl
+++ b/src/categorical_algebra/Matrices.jl
@@ -43,9 +43,9 @@ For a similar design (only for sparse matrices) by the Julia core developers,
 see [SemiringAlgebra.jl](https://github.com/JuliaComputing/SemiringAlgebra.jl)
 and [accompanying short paper](https://doi.org/10.1109/HPEC.2013.6670347).
 """
-@instance DistributiveSemiadditiveCategory(MatrixDom, AbstractMatrix) begin
+@instance DistributiveSemiadditiveCategory{MatrixDom, AbstractMatrix} begin
   # FIXME: Cannot define type-parameterized instances.
-  #@instance AdditiveBiproductCategory(MatrixDom{M}, M) where M <: AbstractMatrix begin
+  #@instance AdditiveBiproductCategory{MatrixDom{M}, M} where M <: AbstractMatrix begin
   @import +, dom, codom, id, mzero, munit, braid
   
   compose(A::AbstractMatrix, B::AbstractMatrix) = B*A
diff --git a/src/categorical_algebra/PredicatedSets.jl b/src/categorical_algebra/PredicatedSets.jl
index 45022a107..5f14692b6 100644
--- a/src/categorical_algebra/PredicatedSets.jl
+++ b/src/categorical_algebra/PredicatedSets.jl
@@ -44,7 +44,7 @@ function compose(f::PredicatedHom{T,S},g::PredicatedHom{S,U}) where {T,S,U}
 end
 
 # This is really the category of decidable sets and partial functions...
-@instance Category(PredicatedSet, PredicatedHom) begin
+@instance Category{PredicatedSet, PredicatedHom} begin
   dom(f::PredicatedHom) = f.dom
   codom(f::PredicatedHom) = f.codom
 
diff --git a/src/core/GAT.jl b/src/core/GAT.jl
index 3e61a7426..304247539 100644
--- a/src/core/GAT.jl
+++ b/src/core/GAT.jl
@@ -7,6 +7,7 @@ using Base.Meta: ParseError
 using Compat
 using AutoHashEquals
 using DataStructures: OrderedDict
+using Logging
 using MLStyle: @match
 
 using ..Meta
@@ -188,21 +189,43 @@ end
 
 function parse_theory_head(expr::Expr)::TheoryHead
   parse = parse_theory_binding
+  parse_jl = parse_theory_binding_jlstyle
+  parse_either = parse_theory_binding_either
   @match expr begin
     (Expr(:call, :(=>), Expr(:tuple, bases), main)
       => TheoryHead(parse(main), map(parse, bases)))
+    (Expr(:(<:), main, Expr(:tuple,bases))
+      => TheoryHead(parse_jl(main), map(parse_jl, bases)))
     Expr(:call, :(=>), base, main) => TheoryHead(parse(main), [parse(base)])
-    _ => TheoryHead(parse(expr))
+    Expr(:(<:), main, base) => TheoryHead(parse_jl(main), [parse_jl(base)])
+    _ => TheoryHead(parse_either(expr))
   end
 end
 
 function parse_theory_binding(expr::Expr)::TheoryBinding
+  @warn "Using Haskell-style theory declaration with parentheses is deprecated," *
+    " use Julia-style with curly braces." _file=missing _line=missing
   @match expr begin
     Expr(:call, name::Symbol, params...) => TheoryBinding(name, params)
     _ => throw(ParseError("Ill-formed theory binding $expr"))
   end
 end
 
+function parse_theory_binding_jlstyle(expr::Expr)::TheoryBinding
+  @match expr begin
+    Expr(:curly, name::Symbol, params...) => TheoryBinding(name, params)
+    _ => throw(ParseError("Ill-formed theory binding $expr"))
+  end
+end
+
+function parse_theory_binding_either(expr::Expr)::TheoryBinding
+  @match expr begin
+    Expr(:call, name::Symbol, params...) => TheoryBinding(name, params)
+    Expr(:curly, name::Symbol, params...) => TheoryBinding(name, params)
+    _ => throw(ParseError("Ill-formed theory binding $expr"))
+  end
+end
+
 """ Parse the body of a GAT declaration.
 """
 function parse_theory_body(expr::Expr)
@@ -515,7 +538,7 @@ end
 """
 macro instance(head, body)
   # Parse the instance definition.
-  head = parse_theory_binding(head)
+  head = parse_theory_binding_either(head)
   functions, ext_functions = parse_instance_body(body)
 
   # We must generate and evaluate the code at *run time* because the theory
diff --git a/src/core/Syntax.jl b/src/core/Syntax.jl
index 331d2fe27..e3c374499 100644
--- a/src/core/Syntax.jl
+++ b/src/core/Syntax.jl
@@ -105,7 +105,12 @@ macro syntax(syntax_head, mod_name, body=nothing)
   if isnothing(body); body = Expr(:block) end
   @assert body.head == :block
   syntax_name, base_types = @match syntax_head begin
-    Expr(:call, name::Symbol, args...) => (name, args)
+    Expr(:call, name::Symbol, args...) => begin
+      @warn "Using Haskell-style theory declaration with parentheses is deprecated," *
+        " use Julia-style with curly braces." _file=missing _line=missing
+      (name, args)
+    end
+    Expr(:curly, name::Symbol, args...) => (name, args)
     name::Symbol => (name, [])
     _ => throw(ParseError("Ill-formed syntax signature $syntax_head"))
   end
diff --git a/src/linear_algebra/GLA.jl b/src/linear_algebra/GLA.jl
index c6d0284ea..00dad77ce 100644
--- a/src/linear_algebra/GLA.jl
+++ b/src/linear_algebra/GLA.jl
@@ -25,7 +25,7 @@ import ...Programs: evaluate_hom
 
 Functional fragment of graphical linear algebra.
 """
-@theory SemiadditiveCategory(Ob,Hom) => LinearFunctions(Ob,Hom) begin
+@theory LinearFunctions{Ob,Hom} <: SemiadditiveCategory{Ob,Hom} begin
   adjoint(f::(A → B))::(B → A) ⊣ (A::Ob, B::Ob)
   
   scalar(A::Ob, c::Number)::(A → A)
@@ -45,7 +45,7 @@ Functional fragment of graphical linear algebra.
   scalar(A, c) ⋅ f == f ⋅ scalar(B, c) ⊣ (A::Ob, B::Ob, c::Number, f::(A → B))
 end
 
-@syntax FreeLinearFunctions(ObExpr,HomExpr) LinearFunctions begin
+@syntax FreeLinearFunctions{ObExpr,HomExpr} LinearFunctions begin
   oplus(A::Ob, B::Ob) = associate_unit(new(A,B), mzero)
   oplus(f::Hom, g::Hom) = associate(new(f,g))
   compose(f::Hom, g::Hom) = new(f,g; strict=true) # No normalization!
@@ -55,7 +55,7 @@ end
 
 The full relational language of graphical linear algebra.
 """
-@theory AbelianBicategoryRelations(Ob,Hom) => LinearRelations(Ob,Hom) begin
+@theory LinearRelations{Ob,Hom} <: AbelianBicategoryRelations{Ob,Hom} begin
   adjoint(R::(A → B))::(B → A) ⊣ (A::Ob, B::Ob)
 
   scalar(A::Ob, c::Number)::(A → A)
@@ -67,7 +67,7 @@ The full relational language of graphical linear algebra.
   scalar(A, c) ⋅ R == R ⋅ scalar(B, c) ⊣ (A::Ob, B::Ob, c::Number, R::(A → B))
 end
 
-@syntax FreeLinearRelations(ObExpr,HomExpr) LinearRelations begin
+@syntax FreeLinearRelations{ObExpr,HomExpr} LinearRelations begin
   oplus(A::Ob, B::Ob) = associate_unit(new(A,B), mzero)
   oplus(R::Hom, S::Hom) = associate(new(R,S))
   compose(R::Hom, S::Hom) = new(R,S; strict=true) # No normalization!
diff --git a/src/linear_algebra/LinearMapsExternal.jl b/src/linear_algebra/LinearMapsExternal.jl
index 468fafcb4..a1f575256 100644
--- a/src/linear_algebra/LinearMapsExternal.jl
+++ b/src/linear_algebra/LinearMapsExternal.jl
@@ -11,7 +11,7 @@ const LMs = LinearMaps
   N::Int
 end
 
-@instance LinearFunctions(LinearMapDom, LinearMap) begin
+@instance LinearFunctions{LinearMapDom, LinearMap} begin
   @import adjoint, +
 
   dom(f::LinearMap) = LinearMapDom(size(f,2))
diff --git a/src/linear_algebra/LinearOperatorsExternal.jl b/src/linear_algebra/LinearOperatorsExternal.jl
index c0a365649..c498a57bf 100644
--- a/src/linear_algebra/LinearOperatorsExternal.jl
+++ b/src/linear_algebra/LinearOperatorsExternal.jl
@@ -9,7 +9,7 @@ using .LinearOperators: opEye, opExtension, opRestriction, opZeros
   N::Int
 end
 
-@instance LinearFunctions(LinearOpDom, LinearOperator) begin
+@instance LinearFunctions{LinearOpDom, LinearOperator} begin
   @import adjoint, +
 
   dom(f::LinearOperator) = LinearOpDom(size(f,2))
diff --git a/src/linear_algebra/StructuredGLA.jl b/src/linear_algebra/StructuredGLA.jl
index f7ff5fde6..94526357c 100644
--- a/src/linear_algebra/StructuredGLA.jl
+++ b/src/linear_algebra/StructuredGLA.jl
@@ -22,7 +22,7 @@ import ..GraphicalLinearAlgebra:
 Structured matrices have some properties that allow us to compute with them faster
 than general dense matrices. Morphisms in this category represent structured matrices.
 """
-@theory LinearFunctions(Ob,Hom) => StructuredLinearFunctions(Ob, Hom) begin
+@theory StructuredLinearFunctions{Ob,Hom} <: LinearFunctions{Ob,Hom} begin
   munit()::Ob
   @op (ℝ) := munit
 
@@ -51,7 +51,7 @@ than general dense matrices. Morphisms in this category represent structured mat
   symtridiag(a,b) == tridiagonal(a,b,b) ⊣ (A::Ob, a::(ℝ()→A⊗ℝ()), b::(ℝ()→A))
 end
 
-@syntax FreeStructuredLinearFunctions(ObExpr,HomExpr) StructuredLinearFunctions begin
+@syntax FreeStructuredLinearFunctions{ObExpr,HomExpr} StructuredLinearFunctions begin
   oplus(A::Ob, B::Ob) = associate_unit(new(A,B), mzero)
   oplus(f::Hom, g::Hom) = associate(new(f,g))
   compose(f::Hom, g::Hom) = new(f,g; strict=true) # No normalization!
diff --git a/src/theories/Category.jl b/src/theories/Category.jl
index 666739528..f4a7c7392 100644
--- a/src/theories/Category.jl
+++ b/src/theories/Category.jl
@@ -16,7 +16,7 @@ We retain the usual meaning of the symbol ∘ (\\circ), i.e., g∘f = compose(f,
 This usage is too entrenched to overturn, inconvenient though it may be.
 We use symbol ⋅ (\\cdot) for diagrammatic composition: f⋅g = compose(f,g).
 """
-@theory Category(Ob,Hom) begin
+@theory Category{Ob,Hom} begin
   # Unicode aliases.
   @op begin
     (→) := Hom
@@ -43,7 +43,7 @@ end
 compose(fs::Vector) = foldl(compose, fs)
 compose(f, g, h, fs...) = compose([f, g, h, fs...])
 
-@syntax FreeCategory(ObExpr,HomExpr) Category begin
+@syntax FreeCategory{ObExpr,HomExpr} Category begin
   compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
 end
 
@@ -79,7 +79,7 @@ end
 
 """ Theory of (strict) *2-categories*
 """
-@signature Category(Ob,Hom) => Category2(Ob,Hom,Hom2) begin
+@signature Category2{Ob,Hom,Hom2} <: Category{Ob,Hom} begin
   """ 2-morphism in a 2-category """
   Hom2(dom::Hom(A,B), codom::Hom(A,B))::TYPE ⊣ (A::Ob, B::Ob)
   @op (⇒) := Hom2
@@ -102,7 +102,7 @@ compose2(α, β, γ, αs...) = compose2([α, β, γ, αs...])
 
 Checks domains of morphisms but not 2-morphisms.
 """
-@syntax FreeCategory2(ObExpr,HomExpr,Hom2Expr) Category2 begin
+@syntax FreeCategory2{ObExpr,HomExpr,Hom2Expr} Category2 begin
   compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
   compose(α::Hom2, β::Hom2) = associate(new(α,β))
   compose2(α::Hom2, β::Hom2) = associate(new(α,β))
diff --git a/src/theories/Limits.jl b/src/theories/Limits.jl
index dd5da31cd..2ed1caf12 100644
--- a/src/theories/Limits.jl
+++ b/src/theories/Limits.jl
@@ -15,7 +15,7 @@ Section I.3).
 
 For a monoidal category axiomatization, see [`CartesianCategory`](@ref).
 """
-@theory Category(Ob,Hom) => CategoryWithProducts(Ob,Hom,Terminal,Product) begin
+@theory CategoryWithProducts{Ob,Hom,Terminal,Product} <: Category{Ob,Hom} begin
   Terminal()::TYPE
   Product(foot1::Ob, foot2::Ob)::TYPE
   
@@ -50,8 +50,8 @@ Finite limits are presented in biased style, via finite products and equalizers.
 The equational axioms for equalizers are obscure, but can found in (Lambek &
 Scott, 1986, Section 0.5), apparently following "Burroni's pioneering ideas".
 """
-@theory CategoryWithProducts(Ob,Hom,Terminal,Product) =>
-    CompleteCategory(Ob,Hom,Terminal,Product,Equalizer) begin
+@theory CompleteCategory{Ob,Hom,Terminal,Product,Equalizer} <:
+    CategoryWithProducts{Ob,Hom,Terminal,Product} begin
   Equalizer(f::(A → B), g::(A → B))::TYPE ⊣ (A::Ob, B::Ob)
   
   # Equalizers.
@@ -87,7 +87,7 @@ of [`CategoryWithProducts`](@ref).
 
 For a monoidal category axiomatization, see [`CocartesianCategory`](@ref).
 """
-@theory Category(Ob,Hom) => CategoryWithCoproducts(Ob,Hom,Initial,Coproduct) begin
+@theory CategoryWithCoproducts{Ob,Hom,Initial,Coproduct} <: Category{Ob,Hom} begin
   Initial()::TYPE
   Coproduct(foot1::Ob, foot2::Ob)::TYPE
 
@@ -121,8 +121,8 @@ end
 Finite colimits are presented in biased style, via finite coproducts and
 coequalizers. The axioms are dual to those of [`CompleteCategory`](@ref).
 """
-@theory CategoryWithCoproducts(Ob,Hom,Initial,Coproduct) =>
-    CocompleteCategory(Ob,Hom,Initial,Coproduct,Coequalizer) begin
+@theory CocompleteCategory{Ob,Hom,Initial,Coproduct,Coequalizer} <:
+    CategoryWithCoproducts{Ob,Hom,Initial,Coproduct} begin
   Coequalizer(f::(A → B), g::(A → B))::TYPE ⊣ (A::Ob, B::Ob)
   
   # Coequalizers.
diff --git a/src/theories/Monoidal.jl b/src/theories/Monoidal.jl
index ad4d29916..a3f163acd 100644
--- a/src/theories/Monoidal.jl
+++ b/src/theories/Monoidal.jl
@@ -24,7 +24,7 @@ To avoid associators and unitors, we assume the monoidal category is *strict*.
 By the coherence theorem there is no loss of generality, but we may add a
 theory for weak monoidal categories later.
 """
-@signature Category(Ob,Hom) => MonoidalCategory(Ob,Hom) begin
+@signature MonoidalCategory{Ob,Hom} <: Category{Ob,Hom} begin
   otimes(A::Ob, B::Ob)::Ob
   otimes(f::(A → B), g::(C → D))::((A ⊗ C) → (B ⊗ D)) ⊣
     (A::Ob, B::Ob, C::Ob, D::Ob)
@@ -69,12 +69,12 @@ show_latex(io::IO, expr::ObExpr{:munit}; kw...) = print(io, "I")
 
 The theory (but not the axioms) is the same as a braided monoidal category.
 """
-@signature MonoidalCategory(Ob,Hom) => SymmetricMonoidalCategory(Ob,Hom) begin
+@signature SymmetricMonoidalCategory{Ob,Hom} <: MonoidalCategory{Ob,Hom} begin
   braid(A::Ob, B::Ob)::((A ⊗ B) → (B ⊗ A))
   @op (σ) := braid
 end
 
-@syntax FreeSymmetricMonoidalCategory(ObExpr,HomExpr) SymmetricMonoidalCategory begin
+@syntax FreeSymmetricMonoidalCategory{ObExpr,HomExpr} SymmetricMonoidalCategory begin
   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))
@@ -102,7 +102,7 @@ References:
   Section 6.6: "Cartesian center"
 - Selinger, 1999, "Categorical structure of asynchrony"
 """
-@signature SymmetricMonoidalCategory(Ob,Hom) => MonoidalCategoryWithDiagonals(Ob,Hom) begin
+@signature MonoidalCategoryWithDiagonals{Ob,Hom} <: SymmetricMonoidalCategory{Ob,Hom} begin
   mcopy(A::Ob)::(A → (A ⊗ A))
   @op (Δ) := mcopy
   delete(A::Ob)::(A → munit())
@@ -114,7 +114,7 @@ end
 For the traditional axiomatization of products, see
 [`CategoryWithProducts`](@ref).
 """
-@theory MonoidalCategoryWithDiagonals(Ob,Hom) => CartesianCategory(Ob,Hom) begin
+@theory CartesianCategory{Ob,Hom} <: MonoidalCategoryWithDiagonals{Ob,Hom} begin
   pair(f::(A → B), g::(A → C))::(A → (B ⊗ C)) ⊣ (A::Ob, B::Ob, C::Ob)
   proj1(A::Ob, B::Ob)::((A ⊗ B) → A)
   proj2(A::Ob, B::Ob)::((A ⊗ B) → B)
@@ -134,7 +134,7 @@ In this syntax, the pairing and projection operations are defined using
 duplication and deletion, and do not have their own syntactic elements.
 This convention could be dropped or reversed.
 """
-@syntax FreeCartesianCategory(ObExpr,HomExpr) CartesianCategory begin
+@syntax FreeCartesianCategory{ObExpr,HomExpr} CartesianCategory begin
   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))
@@ -160,7 +160,8 @@ The terminology is nonstandard (is there any standard terminology?) but is
 supposed to mean a monoidal category with coherent diagonals and codiagonals.
 Unlike in a biproduct category, the naturality axioms need not be satisfied.
 """
-@signature MonoidalCategoryWithDiagonals(Ob,Hom) => MonoidalCategoryWithBidiagonals(Ob,Hom) begin
+@signature MonoidalCategoryWithBidiagonals{Ob,Hom} <:
+    MonoidalCategoryWithDiagonals{Ob,Hom} begin
   mmerge(A::Ob)::((A ⊗ A) → A)
   @op (∇) := mmerge
   create(A::Ob)::(munit() → A)
@@ -172,7 +173,7 @@ end
 Mathematically the same as [`SemiadditiveCategory`](@ref) but written
 multiplicatively, instead of additively.
 """
-@theory MonoidalCategoryWithBidiagonals(Ob,Hom) => BiproductCategory(Ob,Hom) begin
+@theory BiproductCategory{Ob,Hom} <: MonoidalCategoryWithBidiagonals{Ob,Hom} begin
   pair(f::(A → B), g::(A → C))::(A → (B ⊗ C)) ⊣ (A::Ob, B::Ob, C::Ob)
   copair(f::(A → C), g::(B → C))::((A ⊗ B) → C) ⊣ (A::Ob, B::Ob, C::Ob)
   proj1(A::Ob, B::Ob)::((A ⊗ B) → A)
@@ -193,7 +194,7 @@ multiplicatively, instead of additively.
   □(A)⋅◊(A) == id(munit()) ⊣ (A::Ob)
 end
 
-@syntax FreeBiproductCategory(ObExpr,HomExpr) BiproductCategory begin
+@syntax FreeBiproductCategory{ObExpr,HomExpr} BiproductCategory begin
   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))
@@ -218,7 +219,7 @@ end
 
 """ Theory of (symmetric) *closed monoidal categories*
 """
-@signature SymmetricMonoidalCategory(Ob,Hom) => ClosedMonoidalCategory(Ob,Hom) begin
+@signature ClosedMonoidalCategory{Ob,Hom} <: SymmetricMonoidalCategory{Ob,Hom} begin
   # Internal hom of A and B, an object representing Hom(A,B)
   hom(A::Ob, B::Ob)::Ob
 
@@ -231,7 +232,7 @@ end
 
 """ Syntax for a free closed monoidal category.
 """
-@syntax FreeClosedMonoidalCategory(ObExpr,HomExpr) ClosedMonoidalCategory begin
+@syntax FreeClosedMonoidalCategory{ObExpr,HomExpr} ClosedMonoidalCategory begin
   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))
@@ -262,7 +263,7 @@ A CCC is a cartesian category with internal homs (aka, exponential objects).
 FIXME: This theory should also extend `ClosedMonoidalCategory`, but multiple
 inheritance is not yet supported.
 """
-@signature CartesianCategory(Ob,Hom) => CartesianClosedCategory(Ob,Hom) begin
+@signature CartesianClosedCategory{Ob,Hom} <: CartesianCategory{Ob,Hom} begin
   hom(A::Ob, B::Ob)::Ob
   ev(A::Ob, B::Ob)::((hom(A,B) ⊗ A) → B)
   curry(A::Ob, B::Ob, f::((A ⊗ B) → C))::(A → hom(B,C)) ⊣ (C::Ob)
@@ -272,7 +273,7 @@ end
 
 See also `FreeCartesianCategory`.
 """
-@syntax FreeCartesianClosedCategory(ObExpr,HomExpr) CartesianClosedCategory begin
+@syntax FreeCartesianClosedCategory{ObExpr,HomExpr} CartesianClosedCategory begin
   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))
@@ -287,7 +288,7 @@ end
 
 """ Theory of *compact closed categories*
 """
-@theory ClosedMonoidalCategory(Ob,Hom) => CompactClosedCategory(Ob,Hom) begin
+@theory CompactClosedCategory{Ob,Hom} <: ClosedMonoidalCategory{Ob,Hom} begin
   # Dual A^* of object A
   dual(A::Ob)::Ob
 
@@ -307,7 +308,7 @@ end
    ⊣ (A::Ob, B::Ob, C::Ob, f::((A ⊗ B) → C)))
 end
 
-@syntax FreeCompactClosedCategory(ObExpr,HomExpr) CompactClosedCategory begin
+@syntax FreeCompactClosedCategory{ObExpr,HomExpr} CompactClosedCategory begin
   dual(A::Ob) = distribute_unary(involute(new(A)), dual, otimes,
                                  unit=munit, contravariant=true)
   otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
@@ -346,11 +347,11 @@ end
 
 """ Theory of *dagger categories*
 """
-@signature Category(Ob,Hom) => DaggerCategory(Ob,Hom) begin
+@signature DaggerCategory{Ob,Hom} <: Category{Ob,Hom} begin
   dagger(f::(A → B))::(B → A) ⊣ (A::Ob, B::Ob)
 end
 
-@syntax FreeDaggerCategory(ObExpr,HomExpr) DaggerCategory begin
+@syntax FreeDaggerCategory{ObExpr,HomExpr} DaggerCategory begin
   compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
   dagger(f::Hom) = distribute_dagger(involute(new(f)))
 end
@@ -369,11 +370,11 @@ category](https://ncatlab.org/nlab/show/symmetric+monoidal+dagger-category).
 FIXME: This theory should also extend `DaggerCategory`, but multiple inheritance
 is not yet supported.
 """
-@signature SymmetricMonoidalCategory(Ob,Hom) => DaggerSymmetricMonoidalCategory(Ob,Hom) begin
+@signature DaggerSymmetricMonoidalCategory{Ob,Hom} <: SymmetricMonoidalCategory{Ob,Hom} begin
   dagger(f::(A → B))::(B → A) ⊣ (A::Ob, B::Ob)
 end
 
-@syntax FreeDaggerSymmetricMonoidalCategory(ObExpr,HomExpr) DaggerSymmetricMonoidalCategory begin
+@syntax FreeDaggerSymmetricMonoidalCategory{ObExpr,HomExpr} DaggerSymmetricMonoidalCategory begin
   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))
@@ -395,11 +396,11 @@ categories.
 FIXME: This theory should also extend `DaggerCategory`, but multiple inheritance
 is not yet supported.
 """
-@signature CompactClosedCategory(Ob,Hom) => DaggerCompactCategory(Ob,Hom) begin
+@signature DaggerCompactCategory{Ob,Hom} <: CompactClosedCategory{Ob,Hom} begin
   dagger(f::(A → B))::(B → A) ⊣ (A::Ob, B::Ob)
 end
 
-@syntax FreeDaggerCompactCategory(ObExpr,HomExpr) DaggerCompactCategory begin
+@syntax FreeDaggerCompactCategory{ObExpr,HomExpr} DaggerCompactCategory begin
   dual(A::Ob) = distribute_unary(involute(new(A)), dual, otimes,
                                  unit=munit, contravariant=true)
   otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
@@ -419,11 +420,11 @@ end
 
 """ Theory of *traced monoidal categories*
 """
-@signature SymmetricMonoidalCategory(Ob,Hom) => TracedMonoidalCategory(Ob,Hom) begin
+@signature TracedMonoidalCategory{Ob,Hom} <: SymmetricMonoidalCategory{Ob,Hom} begin
   trace(X::Ob, A::Ob, B::Ob, f::((X ⊗ A) → (X ⊗ B)))::(A → B)
 end
 
-@syntax FreeTracedMonoidalCategory(ObExpr,HomExpr) TracedMonoidalCategory begin
+@syntax FreeTracedMonoidalCategory{ObExpr,HomExpr} TracedMonoidalCategory begin
   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))
@@ -447,7 +448,7 @@ categories" and "spidered/dungeon categories", among other things.
 FIXME: Should also inherit `ClosedMonoidalCategory` and `DaggerCategory`, but
 multiple inheritance is not yet supported.
 """
-@theory MonoidalCategoryWithBidiagonals(Ob,Hom) => HypergraphCategory(Ob,Hom) begin
+@theory HypergraphCategory{Ob,Hom} <: MonoidalCategoryWithBidiagonals{Ob,Hom} begin
   # Self-dual compact closed category.
   dunit(A::Ob)::(munit() → (A ⊗ A))
   dcounit(A::Ob)::((A ⊗ A) → munit())
diff --git a/src/theories/MonoidalAdditive.jl b/src/theories/MonoidalAdditive.jl
index fa5807992..090bdf360 100644
--- a/src/theories/MonoidalAdditive.jl
+++ b/src/theories/MonoidalAdditive.jl
@@ -16,7 +16,7 @@ import Base: collect, ndims, +, zero
 Mathematically the same as [`MonoidalCategory`](@ref) but with different
 notation.
 """
-@signature Category(Ob,Hom) => MonoidalCategoryAdditive(Ob,Hom) begin
+@signature MonoidalCategoryAdditive{Ob,Hom} <: Category{Ob,Hom} begin
   oplus(A::Ob, B::Ob)::Ob
   oplus(f::(A → B), g::(C → D))::((A ⊕ C) → (B ⊕ D)) <=
     (A::Ob, B::Ob, C::Ob, D::Ob)
@@ -52,11 +52,12 @@ show_latex(io::IO, expr::ObExpr{:mzero}; kw...) = print(io, "O")
 Mathematically the same as [`SymmetricMonoidalCategory`](@ref) but with
 different notation.
 """
-@signature MonoidalCategoryAdditive(Ob,Hom) => SymmetricMonoidalCategoryAdditive(Ob,Hom) begin
+@signature SymmetricMonoidalCategoryAdditive{Ob,Hom} <:
+    MonoidalCategoryAdditive{Ob,Hom} begin
   swap(A::Ob, B::Ob)::Hom(oplus(A,B),oplus(B,A))
 end
 
-@syntax FreeSymmetricMonoidalCategoryAdditive(ObExpr,HomExpr) SymmetricMonoidalCategoryAdditive begin
+@syntax FreeSymmetricMonoidalCategoryAdditive{ObExpr,HomExpr} SymmetricMonoidalCategoryAdditive begin
   oplus(A::Ob, B::Ob) = associate_unit(new(A,B), mzero)
   oplus(f::Hom, g::Hom) = associate(new(f,g))
   compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
@@ -77,7 +78,8 @@ Unlike in a cocartesian category, the naturality axioms need not be satisfied.
 
 For references, see [`MonoidalCategoryWithDiagonals`](@ref).
 """
-@theory SymmetricMonoidalCategoryAdditive(Ob,Hom) => MonoidalCategoryWithCodiagonals(Ob,Hom) begin
+@theory MonoidalCategoryWithCodiagonals{Ob,Hom} <:
+    SymmetricMonoidalCategoryAdditive{Ob,Hom} begin
   plus(A::Ob)::((A ⊕ A) → A)
   zero(A::Ob)::(mzero() → A)
   
@@ -93,7 +95,7 @@ end
 For the traditional axiomatization of coproducts, see
 [`CategoryWithCoproducts`](@ref).
 """
-@theory MonoidalCategoryWithCodiagonals(Ob,Hom) => CocartesianCategory(Ob,Hom) begin
+@theory CocartesianCategory{Ob,Hom} <: MonoidalCategoryWithCodiagonals{Ob,Hom} begin
   copair(f::(A → C), g::(B → C))::((A ⊕ B) → C) <= (A::Ob, B::Ob, C::Ob)
   coproj1(A::Ob, B::Ob)::(A → (A ⊕ B))
   coproj2(A::Ob, B::Ob)::(B → (A ⊕ B))
@@ -113,7 +115,7 @@ In this syntax, the copairing and inclusion operations are defined using merging
 and creation, and do not have their own syntactic elements. This convention
 could be dropped or reversed.
 """
-@syntax FreeCocartesianCategory(ObExpr,HomExpr) CocartesianCategory begin
+@syntax FreeCocartesianCategory{ObExpr,HomExpr} CocartesianCategory begin
   oplus(A::Ob, B::Ob) = associate_unit(new(A,B), mzero)
   oplus(f::Hom, g::Hom) = associate(new(f,g))
   compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
@@ -143,8 +145,8 @@ end
 Mathematically the same as [`MonoidalCategoryWithBidiagonals`](@ref) but written
 additively, instead of multiplicatively.
 """
-@theory MonoidalCategoryWithCodiagonals(Ob,Hom) =>
-    MonoidalCategoryWithBidiagonalsAdditive(Ob,Hom) begin
+@theory MonoidalCategoryWithBidiagonalsAdditive{Ob,Hom} <:
+    MonoidalCategoryWithCodiagonals{Ob,Hom} begin
   mcopy(A::Ob)::(A → (A ⊕ A))
   @op (Δ) := mcopy
   delete(A::Ob)::(A → mzero())
@@ -162,8 +164,8 @@ end
 Mathematically the same as [`BiproductCategory`](@ref) but written additively,
 instead of multiplicatively.
 """
-@theory MonoidalCategoryWithBidiagonalsAdditive(Ob,Hom) =>
-    SemiadditiveCategory(Ob,Hom) begin
+@theory SemiadditiveCategory{Ob,Hom} <:
+    MonoidalCategoryWithBidiagonalsAdditive{Ob,Hom} begin
   pair(f::(A → B), g::(A → C))::(A → (B ⊕ C)) ⊣ (A::Ob, B::Ob, C::Ob)
   copair(f::(A → C), g::(B → C))::((A ⊕ B) → C) ⊣ (A::Ob, B::Ob, C::Ob)
   proj1(A::Ob, B::Ob)::((A ⊕ B) → A)
@@ -195,8 +197,8 @@ end
 Mathematically the same as [`HypergraphCategory`](@ref) but with different
 notation.
 """
-@signature SymmetricMonoidalCategoryAdditive(Ob,Hom) =>
-    HypergraphCategoryAdditive(Ob,Hom) begin
+@signature HypergraphCategoryAdditive{Ob,Hom} <:
+    SymmetricMonoidalCategoryAdditive{Ob,Hom} begin
   # Supply of Frobenius monoids.
   mcopy(A::Ob)::(A → (A ⊕ A))
   @op (Δ) := mcopy
diff --git a/src/theories/MonoidalMultiple.jl b/src/theories/MonoidalMultiple.jl
index ae3e6a180..dd6d57e40 100644
--- a/src/theories/MonoidalMultiple.jl
+++ b/src/theories/MonoidalMultiple.jl
@@ -16,7 +16,7 @@ ignore coherence isomorphisms such as associators and unitors.
 FIXME: This theory should also inherit `MonoidalCategory`, but multiple
 inheritance is not supported.
 """
-@signature SymmetricMonoidalCategoryAdditive(Ob,Hom) => RigCategory(Ob,Hom) begin
+@signature RigCategory{Ob,Hom} <: SymmetricMonoidalCategoryAdditive{Ob,Hom} begin
   otimes(A::Ob, B::Ob)::Ob
   otimes(f::(A → B), g::(C → D))::((A ⊗ C) → (B ⊗ D)) ⊣
     (A::Ob, B::Ob, C::Ob, D::Ob)
@@ -28,7 +28,7 @@ end
 
 FIXME: Should also inherit `SymmetricMonoidalCategory`.
 """
-@signature RigCategory(Ob,Hom) => SymmetricRigCategory(Ob,Hom) begin
+@signature SymmetricRigCategory{Ob,Hom} <: RigCategory{Ob,Hom} begin
   braid(A::Ob, B::Ob)::((A ⊗ B) → (B ⊗ A))
   @op (σ) := braid
 end
@@ -40,7 +40,7 @@ universal invariants", Section 3.2
 
 FIXME: Should also inherit `CocartesianCategory`.
 """
-@theory SymmetricRigCategory(Ob,Hom) => DistributiveMonoidalCategory(Ob,Hom) begin
+@theory DistributiveMonoidalCategory{Ob,Hom} <: SymmetricRigCategory{Ob,Hom} begin
   plus(A::Ob)::((A ⊕ A) → A)
   zero(A::Ob)::(mzero() → A)
   
@@ -61,8 +61,8 @@ end
 
 FIXME: Should also inherit `MonoidalCategoryWithDiagonals`.
 """
-@theory DistributiveMonoidalCategory(Ob,Hom) =>
-    DistributiveMonoidalCategoryWithDiagonals(Ob,Hom) begin
+@theory DistributiveMonoidalCategoryWithDiagonals{Ob,Hom} <:
+    DistributiveMonoidalCategory{Ob,Hom} begin
   mcopy(A::Ob)::(A → (A ⊗ A))
   @op (Δ) := mcopy
   delete(A::Ob)::(A → munit())
@@ -78,7 +78,7 @@ biproduct.
 
 FIXME: Should also inherit `SemiadditiveCategory`
 """
-@theory DistributiveMonoidalCategory(Ob,Hom) => DistributiveSemiadditiveCategory(Ob,Hom) begin
+@theory DistributiveSemiadditiveCategory{Ob,Hom} <: DistributiveMonoidalCategory{Ob,Hom} begin
   mcopy(A::Ob)::(A → (A ⊕ A))
   @op (Δ) := mcopy
   delete(A::Ob)::(A → mzero())
@@ -100,7 +100,7 @@ is the cartesian product, see [`DistributiveMonoidalCategory`](@ref).
 
 FIXME: Should also inherit `CartesianCategory`.
 """
-@theory DistributiveMonoidalCategoryWithDiagonals(Ob,Hom) => DistributiveCategory(Ob,Hom) begin
+@theory DistributiveCategory{Ob,Hom} <: DistributiveMonoidalCategoryWithDiagonals{Ob,Hom} begin
   pair(f::(A → B), g::(A → C))::(A → (B ⊗ C)) ⊣ (A::Ob, B::Ob, C::Ob)
   proj1(A::Ob, B::Ob)::((A ⊗ B) → A)
   proj2(A::Ob, B::Ob)::((A ⊗ B) → B)
diff --git a/src/theories/Preorders.jl b/src/theories/Preorders.jl
index dc2ba85bd..e536c1dea 100644
--- a/src/theories/Preorders.jl
+++ b/src/theories/Preorders.jl
@@ -9,19 +9,19 @@ export ThinCategory, FreeThinCategory,
 
 Thin categories have at most one morphism between any two objects.
 """
-@theory Category(Ob,Hom) => ThinCategory(Ob,Hom) begin
+@theory ThinCategory{Ob,Hom} <: Category{Ob,Hom} begin
   f == g ⊣ (A::Ob, B::Ob, f::Hom(A,B), g::Hom(A,B))
 end
 
-@syntax FreeThinCategory(ObExpr,HomExpr) ThinCategory begin
+@syntax FreeThinCategory{ObExpr,HomExpr} ThinCategory begin
   compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
 end
 
-@theory SymmetricMonoidalCategory(Ob,Hom) => ThinSymmetricMonoidalCategory(Ob,Hom) begin
+@theory ThinSymmetricMonoidalCategory{Ob,Hom} <: SymmetricMonoidalCategory{Ob,Hom} begin
   f == g ⊣ (A::Ob, B::Ob, f::Hom(A,B), g::Hom(A,B))
 end
 
-@syntax FreeThinSymmetricMonoidalCategory(ObExpr,HomExpr) ThinSymmetricMonoidalCategory begin
+@syntax FreeThinSymmetricMonoidalCategory{ObExpr,HomExpr} ThinSymmetricMonoidalCategory begin
   compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
   otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
   otimes(f::Hom, g::Hom) = associate(new(f,g))
@@ -34,7 +34,7 @@ end
 
 Preorders encode the axioms of reflexivity and transitivity as term constructors.
 """
-@theory Preorder(Elt,Leq) begin
+@theory Preorder{Elt,Leq} begin
   Elt::TYPE
   Leq(lhs::Elt, rhs::Elt)::TYPE
   @op (≤) := Leq
@@ -48,7 +48,7 @@ Preorders encode the axioms of reflexivity and transitivity as term constructors
   # Read as (f⟹ A≤B ∧ g⟹ A≤B) ⟹ f ≡ g
 end
 
-@syntax FreePreorder(ObExpr,HomExpr) Preorder begin
+@syntax FreePreorder{ObExpr,HomExpr} Preorder begin
   transitive(f::Leq, g::Leq) = associate(new(f,g; strict=true))
 end
 
diff --git a/src/theories/Relations.jl b/src/theories/Relations.jl
index 18c61611e..abf8dfd75 100644
--- a/src/theories/Relations.jl
+++ b/src/theories/Relations.jl
@@ -18,13 +18,13 @@ References:
 - Walters, 2009, blog post, "Categorical algebras of relations",
   http://rfcwalters.blogspot.com/2009/10/categorical-algebras-of-relations.html
 """
-@signature HypergraphCategory(Ob,Hom) => BicategoryRelations(Ob,Hom) begin
+@signature BicategoryRelations{Ob,Hom} <: HypergraphCategory{Ob,Hom} begin
   # Logical operations.
   meet(R::(A → B), S::(A → B))::(A → B) ⊣ (A::Ob, B::Ob)
   top(A::Ob, B::Ob)::(A → B)
 end
 
-@syntax FreeBicategoryRelations(ObExpr,HomExpr) BicategoryRelations begin
+@syntax FreeBicategoryRelations{ObExpr,HomExpr} BicategoryRelations begin
   otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
   otimes(R::Hom, S::Hom) = associate(new(R,S))
   compose(R::Hom, S::Hom) = associate(new(R,S; strict=true))
@@ -43,8 +43,7 @@ References:
 - Carboni & Walters, 1987, "Cartesian bicategories I", Sec. 5
 - Baez & Erbele, 2015, "Categories in control"
 """
-@signature HypergraphCategoryAdditive(Ob,Hom) =>
-    AbelianBicategoryRelations(Ob,Hom) begin
+@signature AbelianBicategoryRelations{Ob,Hom} <: HypergraphCategoryAdditive{Ob,Hom} begin
   # Second supply of Frobenius monoids.
   plus(A::Ob)::((A ⊕ A) → A)
   zero(A::Ob)::(mzero() → A)
@@ -58,7 +57,7 @@ References:
   bottom(A::Ob, B::Ob)::(A → B)
 end
 
-@syntax FreeAbelianBicategoryRelations(ObExpr,HomExpr) AbelianBicategoryRelations begin
+@syntax FreeAbelianBicategoryRelations{ObExpr,HomExpr} AbelianBicategoryRelations begin
   oplus(A::Ob, B::Ob) = associate_unit(new(A,B), mzero)
   oplus(R::Hom, S::Hom) = associate(new(R,S))
   compose(R::Hom, S::Hom) = associate(new(R,S; strict=true))
@@ -81,8 +80,8 @@ References:
 FIXME: Should also inherit `BicategoryOfRelations`, but multiple inheritance is
 not yet supported.
 """
-@signature DistributiveMonoidalCategoryWithDiagonals(Ob,Hom) =>
-    DistributiveBicategoryRelations(Ob,Hom) begin
+@signature DistributiveBicategoryRelations{Ob,Hom} <:
+    DistributiveMonoidalCategoryWithDiagonals{Ob,Hom} begin
   # Self-dual dagger compact category.
   dagger(R::(A → B))::(B → A) ⊣ (A::Ob, B::Ob)
   dunit(A::Ob)::(munit() → (A ⊗ A))
diff --git a/src/wiring_diagrams/MonoidalDirected.jl b/src/wiring_diagrams/MonoidalDirected.jl
index be48c1fc0..1e3c71ed9 100644
--- a/src/wiring_diagrams/MonoidalDirected.jl
+++ b/src/wiring_diagrams/MonoidalDirected.jl
@@ -77,7 +77,7 @@ Extra structure, such as copying or merging, can be added to wiring diagrams in
 different ways, but wiring diagrams always form a symmetric monoidal category in
 the same way.
 """
-@instance SymmetricMonoidalCategory(Ports, WiringDiagram) begin
+@instance SymmetricMonoidalCategory{Ports, WiringDiagram} begin
   @import dom, codom
 
   function id(A::Ports)
diff --git a/src/wiring_diagrams/MonoidalUndirected.jl b/src/wiring_diagrams/MonoidalUndirected.jl
index c831107dd..d333d922f 100644
--- a/src/wiring_diagrams/MonoidalUndirected.jl
+++ b/src/wiring_diagrams/MonoidalUndirected.jl
@@ -114,7 +114,7 @@ codom(f::HomUWD{UWD}) where UWD = ObUWD{UWD}(codom_port_types(f))
 The objects are lists of port types and morphisms are undirected wiring diagrams
 whose outer ports are partitioned into domain and codomain.
 """
-@instance HypergraphCategory(ObUWD, HomUWD) begin
+@instance HypergraphCategory{ObUWD, HomUWD} begin
   @import dom, codom
 
   function compose(f::HomUWD, g::HomUWD)


Test patch:
diff --git a/test/core/GAT.jl b/test/core/GAT.jl
index 4c48befd0..8b0a24e35 100644
--- a/test/core/GAT.jl
+++ b/test/core/GAT.jl
@@ -98,7 +98,7 @@ target = Dict(:→ => :Mor)
 
 # This try-catch block is a necessary work around because of a current bug
 # where test_throws doesn't catch errors thrown from inside of a macro
-@test_throws ParseError try @eval @signature Category(Ob,Hom) begin
+@test_throws ParseError try @eval @signature Category{Ob,Hom} begin
   Ob::TYPE
   Hom(dom, codom)::TYPE ⊣ (dom::Ob, codom::Ob)
   @op (→) := Hom
@@ -118,7 +118,7 @@ end
 
 """ Theory of categories
 """
-@theory Category(Ob,Hom) begin
+@theory Category{Ob,Hom} begin
   Ob::TYPE
   Hom(dom, codom)::TYPE ⊣ (dom::Ob, codom::Ob)
   @op (→) := Hom
@@ -167,7 +167,7 @@ category_theory = GAT.Theory(types, terms, axioms, aliases)
 
 """ Equivalent shorthand definition of Category theory
 """
-@theory CategoryAbbrev(Ob,Hom) begin
+@theory CategoryAbbrev{Ob,Hom} begin
   @op begin
     (→) := Hom
     (⋅) := compose
@@ -203,12 +203,12 @@ theory = GAT.theory(Category)
 @test GAT.interface(theory) == [accessors; constructors; alias_functions]
 
 # Theory extension
-@signature Semigroup(S) begin
+@signature Semigroup{S} begin
   S::TYPE
   times(x::S,y::S)::S
 end
 
-@signature Semigroup(M) => MonoidExt(M) begin
+@signature MonoidExt{M} <: Semigroup{M} begin
   munit()::M
 end
 
@@ -255,13 +255,13 @@ context = GAT.Context((:X => :Ob, :Y => :Ob, :Z => :Ob,
 
 """ Vectors as an instance of the theory of semigroups
 """
-@instance Semigroup(Vector) begin
+@instance Semigroup{Vector} begin
   times(x::Vector, y::Vector) = [x; y]
 end
 
 @test times([1,2],[3,4]) == [1,2,3,4]
 
-@signature Monoid(M) begin
+@signature Monoid{M} begin
   M::TYPE
   munit()::M
   times(x::M,y::M)::M
@@ -269,12 +269,12 @@ end
 
 # Incomplete instance of Monoid
 # XXX: Cannot use `@test_warn` since generated code won't be at toplevel.
-#@test_warn "not implemented" @instance Monoid(String) begin
+#@test_warn "not implemented" @instance Monoid{String} begin
 #  times(x::AbsStringtractString, y::String) = string(x,y)
 #end
 
 # Complete instance of Monoid
-@instance Monoid(String) begin
+@instance Monoid{String} begin
   munit(::Type{String}) = ""
   times(x::String, y::String) = string(x,y)
 end
diff --git a/test/core/Syntax.jl b/test/core/Syntax.jl
index f71190716..3eb5e0c7a 100644
--- a/test/core/Syntax.jl
+++ b/test/core/Syntax.jl
@@ -13,7 +13,7 @@ using Catlab
 
 """ Theory of monoids.
 """
-@signature Monoid(Elem) begin
+@signature Monoid{Elem} begin
   Elem::TYPE
   munit()::Elem
   mtimes(x::Elem,y::Elem)::Elem
@@ -67,13 +67,13 @@ e = munit(FreeMonoidAssocUnit.Elem)
 @test mtimes(e,x) == x && mtimes(x,e) == x
 
 abstract type MonoidExpr{T} <: GATExpr{T} end
-@syntax FreeMonoidTyped(MonoidExpr) Monoid
+@syntax FreeMonoidTyped{MonoidExpr} Monoid
 
 x = Elem(FreeMonoidTyped.Elem, :x)
 @test FreeMonoidTyped.Elem <: MonoidExpr
 @test isa(x, FreeMonoidTyped.Elem) && isa(x, MonoidExpr)
 
-@signature Monoid(Elem) => MonoidNumeric(Elem) begin
+@signature MonoidNumeric{Elem} <: Monoid{Elem} begin
   elem_int(x::Int)::Elem
 end
 @syntax FreeMonoidNumeric MonoidNumeric
@@ -84,7 +84,7 @@ x = elem_int(FreeMonoidNumeric.Elem, 1)
 
 """ A monoid with two distinguished elements.
 """
-@signature Monoid(Elem) => MonoidTwo(Elem) begin
+@signature MonoidTwo{Elem} <: Monoid{Elem} begin
   one()::Elem
   two()::Elem
 end
@@ -102,7 +102,7 @@ x, y = one(FreeMonoidTwo.Elem), two(FreeMonoidTwo.Elem)
 # Category
 ##########
 
-@signature Category(Ob,Hom) begin
+@signature Category{Ob,Hom} begin
   Ob::TYPE
   Hom(dom::Ob, codom::Ob)::TYPE
 
@@ -147,7 +147,7 @@ f, g = Hom(:f, X, Y), Hom(:g, Y, X)
 # Functor
 #########
 
-@instance Monoid(String) begin
+@instance Monoid{String} begin
   munit(::Type{String}) = ""
   mtimes(x::String, y::String) = string(x,y)
 end