When we have a model of a theory, we need some way of telling Julia what types to use for representing the values in that theory. The point of this is not to be precise, but rather to be able to specialize things for performance.
I.e., when we do FinSet, we want to tell Julia that an Ob is an Int, and a morphism is a Vector{Int}. There are several ways of doing this.
The first way is that each model could have an associated module. I.e. something like
module FinSetImpl
const Ob = Int
const Hom = Int
end
The second way is that when you declare a model, you could subtype Model with parameters given by the types of the type constructors. This could be done with a couple variants.
In the first variant, when you declare a theory you would declare an abstract type for models of that theory, parameterized by the type constructors. For instance:
struct FinSetC <: CategoryModel{Int, Vector{Int}}
end
In the second variant, we'd have an abstract type Model with two parameters, one being the theory, and the other being a Tuple of type parameters. For instance:
struct FinSetC <: Model{ThCategory, Tuple{Int, Vector{Int}}}
end
I'm inclined to this last variant, because it seems like it's the most programmable. That is, we don't need to make up any new names like FinSetImpl or CategoryModel. Additionally, generated structs could look something like
struct Arena{Ob, Hom, T <: Model{ThCartesianCategory, Tuple{Ob, Hom}}}
pos::Ob
dir::Ob
end
struct FullLens{Ob, Hom, T <: Model{ThCartesianCategory, Tuple{Ob, Hom}}}
dom::Arena{Ob, Hom, T}
codom::Arena{Ob, Hom, T}
expose::Hom
update::Hom
end
Interested in hearing the thoughts of @epatters, @kris-brown and @jpfairbanks though.
When we have a model of a theory, we need some way of telling Julia what types to use for representing the values in that theory. The point of this is not to be precise, but rather to be able to specialize things for performance.
I.e., when we do
FinSet
, we want to tell Julia that anOb
is anInt
, and a morphism is aVector{Int}
. There are several ways of doing this.The first way is that each model could have an associated module. I.e. something like
The second way is that when you declare a model, you could subtype
Model
with parameters given by the types of the type constructors. This could be done with a couple variants.In the first variant, when you declare a theory you would declare an abstract type for models of that theory, parameterized by the type constructors. For instance:
In the second variant, we'd have an abstract type
Model
with two parameters, one being the theory, and the other being aTuple
of type parameters. For instance:I'm inclined to this last variant, because it seems like it's the most programmable. That is, we don't need to make up any new names like
FinSetImpl
orCategoryModel
. Additionally, generated structs could look something likeInterested in hearing the thoughts of @epatters, @kris-brown and @jpfairbanks though.