Checking if a model implements a theory leads to MethodNotFound error

[kris-brown]

GATlab's approach to runtime checking if a model implements a theory is to use dispatch on ScopeTags.

F = FinMatC{Float64}()
implements(F, ThCategory) # true
implements(F, ThNat) # MethodNotFound error

A method is created by @instance to return something (not true, but something that's not nothing) for a given model type + ScopeTag (wrapped in a Val) for each scope of the theory.

I believe the line

implements(m::Module, ::Type{Val{tag}}) where {tag} = nothing

was intended to be the catch-all case for when a scope is not implemented. However, this line never gets called (perhaps Module was meant to be Model?) Trying to make a simple fix there causes other problems which will need to be debugged.

[kris-brown]

Even though there is a workaround #175, I suspect that dispatch isn't the best way to check this. I envision a solution like

implements(model::Any, theory::Union{Module,GAT}, x::Ident, types::Vector{Type})

E.g. implements(FinMatC{Int}(), ThCategory, compose, [Int, Matrix{Int}]) which the above function converts into a runtime check whether or not there is a method compose(::WithModel{FinSetC}, ::Matrix{Int}, ::Matrix{Int}).

We can then add sugar which takes a Symbol rather than an Ident(if this is not ambiguous) and uses [Any, Any,...] for the type vector if none is explicitly provided. And not providing a particular ident means the conjunction of checking all the idents in the theory.

This seems nicer than the current approach because

1. it avoids a proliferation of implements methods (for every model type + theory scope pair)
2. it gives you finer granularity to check if particular methods are implemented rather than only checking entire theories (or, at best, scopes)
3. it gives you the argument type granularity to see that FinMatC{Int}() implements compose(::Matrix{Int}, ::Matrix{Int}) but not compose(::Matrix{Float64}, ::Matrix{Float64}).