Named instance type assignments

src/models/ModelInterface.jl

@@ -178,15 +178,30 @@ end
 """
 macro instance(head, model, body)
   # Parse the head of @instance to get theory and instance types
-  # TODO: should we allow instance types to be nothing? Is this in Catlab?
   (theory_module, instance_types) = @match head begin
-    :($ThX{$(Ts...)}) => (ThX, Ts)
+    Expr(:curly, ThX, Expr(:(=), a,b),xs...) => begin
+      theory = macroexpand(__module__, :($ThX.Meta.@theory))
+      nS, nT = length(primitive_sorts(theory)), length(xs)+1 
+      nS == nT || error("$nT types provided ($ThX expected $nS)")
+      ThX => map(nameof.(primitive_sorts(theory))) do psort
+        for x in [Expr(:(=), a,b); xs]
+          x.head == :(=) || error("Unexpected type assignment $x")
+          n, v = x.args
+          n == psort && return v
+        end
+        error("Sort $psort not found in $xs")
+      end
+    end
+    :($ThX{$(Ts...)}) =>  (ThX, Ts) 
     _ => error("invalid syntax for head of @instance macro: $head")
   end
 
   # Get the underlying theory
   theory = macroexpand(__module__, :($theory_module.Meta.@theory))
 
+  nS, nT = length(primitive_sorts(theory)), length(instance_types) 
+  nS == nT || error("$nT types provided ($theory_module expected $nS)")
+
   # A dictionary to look up the Julia type of a type constructor from its name (an ident)
   jltype_by_sort = Dict{AlgSort,Expr0}([
     zip(primitive_sorts(theory), instance_types)..., 

src/syntax/TheoryInterface.jl

@@ -203,7 +203,7 @@ function theory_impl(head, body, __module__)
 end
 
 """
-The Dispatch model defers to type-dispatch: f[Dispatch](a,b,c) == f(a,b,c)
+The Dispatch model defers to type-dispatch
 """
 @struct_hash_equal struct Dispatch
   jltypes::Dict{AlgSort, Type}

test/models/ModelInterface.jl

@@ -27,10 +27,24 @@ end
   dom(f::Vector{Int}) = length(f)
 end
 
+# Error if we label with nonexistent sorts
+@test_throws LoadError @eval @instance ThCategory{Ob=Int, Hume=Vector{Int}} [model::FinSetC′] begin
+  id(::Int) = error("")
+  compose(::Vector{Int}, ::Vector{Int}) = error("")
+end
+
+
+# Error if we have superfluous type assignments
+@test_throws LoadError @eval @instance ThCategory{Ob=Int, Hom=Vector{Int}, Hom2=Matrix{Int}} [model::FinSetC′] begin
+  id(::Int) = error("")
+  compose(::Vector{Int}, ::Vector{Int}) = error("")
+end
+
 # Actual instance
 #----------------
 
-@instance ThCategory{Int, Vector{Int}} [model::FinSetC′] begin
+# Test using the labeled sorts
+@instance ThCategory{Ob=Int, Hom=Vector{Int}} [model::FinSetC′] begin
 Ob(i::Int) = i 
 
   # check f is Hom: n -> m
@@ -187,11 +201,11 @@ end
   h(b::Y)::Y 
 end
 
-@instance T1{Int} begin 
+@instance T1{X=Int} begin 
   h(a::Int) = 1 
 end
 
-@instance T2{Int,Bool} begin 
+@instance T2{X=Int,Y=Bool} begin 
   h(b::Bool) = false 
 end