AlgebraicJulia / AlgebraicJulia/GATlab.jl

Using the same struct as a model for multiple theories

Ouverte
#173 0 commentaires 0 réactions 1 personne assignée Réclamée par @kris-brown Voir sur GitHub
enhancement
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.

Recevez les nouvelles issues par e-mail

Un résumé court des issues GitHub adaptées aux débutants.