Expressions with type tags for GAT type and term

[epatters]

For compatibility with Catlab (#57) and for its own sake, in addition to fully untyped expressions, we should have expressions whose typed are tagged with the GAT type and term constructors. We can then dispatch using that info.

There are many ways to set this up but something like:

module Cat
   Ob() = 1
   Hom() = 2
   compose() = 3
   id() = 4
end

TTerm{Cat.Hom,Cat.compose}

[olynch]

First of all, this should be a module, not a struct.

Secondly, there are some options to consider for how exactly to form these types. One way is to do as in the OP, i.e.

module Cat
Ob() = 1
Hom() = 2
compose() = 3
id() = 4
end

Another way is to instead of functions use singleton structs. The advantage here is that we can encode the integer at the type level. This would look something like

module Cat
struct Ob <: TypCon{1} end
struct Hom <: TypCon{2} end
struct compose <: TrmCon{3} end
struct id <: TrmCon{4} end
end

This has the advantage that we can dispatch on TypCon{i} and TrmCon{j}. However, it has a disadvantage which is that we have to pass around Ob() instead of Ob. The problem is that we then have to be careful when overloading methods to overload with TypCon{1} instead of Ob. This makes writing manual model implementations slightly more annoying.

[olynch]

We also have to be careful with non-symbolic names. I.e., when we declare a theory that has non-symlit names, we must refer to them with something like

struct AnonTypCon{i} <: TypCon{i} end

[olynch]

Also, we can't use TypCon/TrmCon because those are already types in Gatlab. What about TypTag and TrmTag?

[epatters]

Do we need to dispatch on term/type constructors identified by level? That seems like a recipe for unreadable code. We could take the point of view that the dispatch feature is only for symbolic names and is soley a user convenience to integrate typed expressions with Julia dispatch.

[olynch]

The way that models are defined is via dispatch on term/type constructors identified by level. This makes interpreting terms easy:

interpret(m::Model, t::Trm) = ap(m, AnonTrmTag{index(t.head)}(), interpret.(Ref(m), t.args))

(well, in fact it's slightly more complicated than that, but that's the basic idea).

You could also imagine compiling terms based on a similar principle.

[olynch]

Oh, I see the confusion. I liked this proposal so much that I wanted to also use these type tags for organizing the dispatch system for models, instead of just for typed expressions.

[olynch]

Closed by #81