Open jpfairbanks opened 4 years ago
Sounds good to me.
In the @theory
macro, could we generate an abstract type representing maps between instances of the theory that only made you define the map on generators?
Alternatively, we could write a @theory_map macro that took in a theory and a name for the theory map (i.e. Category and AbstractFunctor) and made AbstractFunctor
into an abstract type with implementations for the operations of the theory.
That would be really cool!
Well, don't get too excited; I'm working out Functors and MonoidalFunctors now, and we'll see how that goes before I attempt that.
Totally agreed about storing Function
instead of Symbol
for term constructors like compose
and id
. This should allow us to eliminate complicated reflection machinery in invoke_term
and also get a performance boost by going through Julia's standard dispatch mechanism.
Why don't we create an abstract type Functor that has the API:
The idea being that the functor type creator just has to specify what happens on the generators of the theory and the term constructors. Then the
MonoidalFunctor <: AbstractFunctor
would have the following additional method definitions:In this setting, in order to make a functor, you would just have to define a type
MyFunctor<:MonoidalFunctor
which supplies the action on the generators. We could supply aPresentedMonoidalFunctor
which works like the current implementation by storing a dictionary mapping the generators to their images under the functor.I think we could simplify a lot of this code if we store the GATExprs with the operation as a
Function
instead of aSymbol
. The current implementation looks like:Instead of storing
head(ex) == :otimes
we could store the functionotimes
, this would allow a single abstract functor type with the idea that the codomain category will support all the term constructors of the domain category so that you can implement arbitrary GAT functors: