Closed olynch closed 1 year ago
I agree that it is good to distinguish a particular model of the GAT from a struct that specifies many different models at once. I'm not sure about the term "model system" though. Maybe "model family," being short for "a family of models"?
I like model family; family is more specific to the usage of "system" that I had in mind (i.e., analogous to "solar system").
So is model family taking the place of the logician's Model. And model is now referring to the entities in the model family?
I feel like that's not what Owen meant but it's also not clear to me. Is it instead that a model family is going to be a struct such that any instance of the struct is an actual model of the theory, e.g. struct FinSet int n end
is a model family for the GAT of sets?
No, the logician's model corresponds to specific instances of the struct that corresponds to the model family. For instance, we might have a model family
struct SliceCat{Ob, Hom, C<:Model{Category, Tuple{Ob, Hom}} <: Model{Category, Tuple{Tuple{Ob, Hom}, Hom}}
cat::C
over::Ob
end
Each value of SliceCat
corresponds to a specific model. This also says that an object of the slice category consists of an object and morphism in the base category, and a morphism in the slice category is just a morphism in the base category.
Ok so SliceCat is a model family. And then what that type signature says is that each instance of SliceCat is a model of the theory of Categories.
What do we call the structs that will store the objects and morphisms in a particular model (instance of SliceCat)?
Ok so SliceCat is a model family. And then what that type signature says is that each instance of SliceCat is a model of the theory of Categories.
Yes, exactly.
What do we call the structs that will store the objects and morphisms in a particular model (instance of SliceCat)?
Good question, I don't yet have a name for that. Any suggestions?
I propose that we use the term "model system" for what we previously called a "model" of a GAT. Instances of a model system struct are individual models. Some model systems consist of just a single model (i.e. zero field structs), but in general a model system might encompass many values of the struct, and thus many "models".