AlgebraicJulia / GATlab.jl

GATlab: a computer algebra system based on generalized algebraic theories (GATs)
https://algebraicjulia.github.io/GATlab.jl/
MIT License
23 stars 2 forks source link

Runtime check for valid models #91

Open kris-brown opened 11 months ago

kris-brown commented 11 months ago

For example, slice categories:

struct SliceC{ObT, HomT, C<:Model{Tuple{ObT, HomT}}} <: Model{Tuple{SliceOb{ObT, HomT}, HomT}}
  cat::C
  over::ObT
end

@instance ThCategory{SliceOb{ObT, HomT}, HomT} (;model::SliceC{ObT, HomT, C}) where {ObT, HomT, C} begin
...

We want to constrain the C of SliceC to be a type which is not just a Model but a model which implements ThCategory. However, we can only know at runtime if this is the case.

So there should be an overloadable is_valid_instance() method in the @instance declaration that will make calls to implements.