Models and instances
A model is any julia value m
that satisfies m :: Model
. A model may implement one or more theories; to check if a model m
is implements a theory Th
, one can run implements(m, Th)
, which returns nothing
if m
does not implement Th
, and returns an ImplementationNotes
struct if m
does implement Th
.
When a model m
implements Th
, the following methods should be defined.
For every type constructor
X
inTh
Th.X[m::typeof(m)](x, args...) = ...
This attempts to coerce
x
into a valid element of the type constructorX
applied to argsargs...
, and throws an error if this is not possible.For instance,
ThCategory.Hom[FinSetC()](xs::Vector{Int}, dom::Int, codom::Int)
returnsxs
if and only iflength(xs) == dom
andall(1 .<= xs .<= codom)
, and otherwise errors.This is syntactic sugar (via an overload of
Base.getindex(::typeof(ThCategory.Hom), ::Model)
) for callingThCategory.Hom(TheoryInterface.WithModel(FinSetC()), xs, dom, codom)
. The reason that we do not simply haveThCategory.Hom(FinSetC(), xs, dom, codom)
is a long story; essentially it has to do with maintaining compatibility with Catlab. But one advantage of this is that you can defineHom = ThCategory.Hom[FinSetC()]
, and then use that locally.For each argument
a
to a type constructor (i.e.dom
andcodom
forHom
), an overload ofTh.a[m::typeof(m)](x) = ...
This opportunistically attempts to retrieve the type argument for x. For instance,
ThCategory.dom[FinSetC()]([1,2,3]) = 3
. However, this may return an error, as for instanceThCategory.codom[FinSetC()]([1,2,3])
is uncertain; it could be a morphism into anyn >= 3
. This is because morphisms don't have to know their domain and codomain.For each term constructor
f
inTheory
Th.f[m::typeof(m)](args...) = ...
This applies the term constructor to arguments that are assumed to be a valid type (i.e., they have previously been coerced by the type constructors). For instance,
ThCategory.compose[FinSetC()]([1,3,2], [1,3,2]) == [1,2,3]
Term constructors sometimes need to know the values of elements of their context that are not arguments. For instance,
compose(f::Hom(A,B), g::Hom(B,C))
might need access to the values ofA
,B
orC
, which might not be able to be inferred fromf
andg
. In this case, we support passing a named tuple calledcontext
to provide these additional values, named with their variables names in the theory. So for instance, we would allowThCategory.compose[FinSetC()]([1,3,2], [1,3,2]; (;B=3))
. It is rare that this is needed, however.
In order to make a model implement a theory, one can either manually implement all of the methods, or use the @instance
macro. You can see examples of using the @instance
macro in src/stdlib/models
.