AlgebraicJulia / GATlab.jl

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

Sugar for models with union types #164

Open kris-brown opened 1 month ago

kris-brown commented 1 month ago

If Ob is implemented by Union{A,B} for some model, then when declaring the model one is forced to write something like

@instance ThCategory{Union{A,B}, ...} [model::MyModel] begin

  id(x::Union{A,B}) = x isa A ? (... some A logic ...) : (... some B logic ...)

  ...
end

A multiple dispatch style approach would be preferred:

id(x::A) = ...
id(x::B) = ...
kris-brown commented 1 month ago

The problem is worse for if Hom were implemented by a union type, since compose would have four possibilities. Hopefully it is not too much of a hassle to handle all the possible cases (including explicit Union types).