AlgebraicJulia / AlgebraicJulia/GATlab.jl
Using the same struct as a model for multiple theories
- Langage dominant
- Julia
- Étoiles
- 43
- Forks
- 4
- Métriques de merge des PR
- Aucune PR mergée en 30 j
Description
In GATlab's present design, one declares a struct to be a possible model (e.g. for `ThCategory`) by saying `struct SetCat <: Model{Tuple{AbstractSet, SetFunction}}` and then putting all the methods in an `@instance` block somewhere.
This prevents one from saying `SetCat` is a model of some _other_ theory (unless we're lucky and they have semantically the same type constructors in the same order). This feels really limiting. The example this is coming up in is we have `ThCategoryWithTerminal <: ThCategory` which adds another type constructor. It would be great to say "by the way, `SetCat` is not merely a category, but it also has this additional structure which I can make explicit by:
```julia
@instance ThCategoryWithTerminal{AbstractSet, SetFunction, TerminalLimit} [model::SetCat] begin
@import id, compose
terminal()::TerminalLimit = ...
delete(T::TerminalLimit, x::AbstractSet)::SetFunction = ...
end
```
But `SetCat` is not a `Model{Tuple{AbstractSet, SetFunction, TerminalLimit}}` - that is fixed! It seems like there will be a huge proliferation of structs and names if the same struct can't be a model of two different theories (which happen to have different type constructors).
This also addresses an issue of repetitiveness of type parameters: one first declares a model subtypes `Model{Tuple{A,B,C,...}}` and then has to write `@instance MyTheory{A,B,C,...}`.
Guide de contribution
Aucun guide de contribution indexé pour ce dépôt
Évaluation
Cette issue n'a pas encore été évaluée.