Closed jpfairbanks closed 3 years ago
Here's how I implemented order-sorted algebra, on both objects and morphisms, for the Data Science Ontology:
To summarize: I add GAT types for both subobjects (subtypes) and submorphisms (commutative diagrams induced by subtyping). For the subobjects, there is a term constructor coerce
that yields the morphism performing the implicit conversion (or coercion), similarly to your suggested constructor subtype
. The submorphisms define a 2-categorical structure, with notions of vertical and horizontal composition.
If we wanted to model numerical computations in Julia with Catlab, we would need to represent the type hierarchy. My first thought is to add a morphism constructor to the doctrine like
subtype(A::Ob, b::Ob)::Hom(A,B)
which represents the fact that ifA <: B
, then you can cast an instance of A to an instance of B. Is that the best way to mode “order sorted algebras” within Catlab?