Typed Theories

[jpfairbanks]

I'm definitely out on a limb here, but if I understand the idea of Rewrite.jl and Catlab.jl correctly, they are both building out systems for rewriting in General Algebraic Theories. In the formulation necessary for Category Theory, every term has an objected associated with it and every expression has an two objects associated with it (domain and codomain), which can be thought of as a types. And you are only allowed to build expressions that "typecheck" under the rules of function composition f(::A)::B \circ g(::B)::C = fg(::A)::C

I understand that Rewrite is focused on symbolic algebra for numerical methods, which is done completely in categories with only one object, typically Z, R, or C, but having the ability to include typed expressions would be really helpful for more complex modeling activities.