Codecov Report

Attention: Patch coverage is 93.65079% with 4 lines in your changes missing coverage. Please review.

Project coverage is 95.43%. Comparing base (be9b7d5) to head (86e6d51).

@@                  Coverage Diff                  @@
##           withmodel_subtype     #172      +/-   ##
=====================================================
- Coverage              95.56%   95.43%   -0.14%     
=====================================================
  Files                     38       38              
  Lines                   2234     2257      +23     
=====================================================
+ Hits                    2135     2154      +19     
- Misses                    99      103       +4     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

This PR's change makes life much easier in many ways, including those in the original description and also things like allowing Models to be subtypes of other abstract types (rather than forcing any type that is used as a Model to be a subtype of GATlab's particular abstract type). But I've realized now that GATlab's getindex trick inadvertently performs type piracy. Something like following code is generated for any theory T and constructor f:

Base.getindex(::typeof(f), m::Any) = args -> f(WithModel(m), args...)

However GATlab doesn't own any of getindex, f (since we may be overloading some external method), or whatever type m is, now that m is not forced to be a Model{Tuple{...}}.

There are a few ways to address this.

1. Require that one index the method name with a WithModel. This makes the sugar less sweet - it's not that much more convenient then just passing in WithModel(m) as the first argument, though it is much more legible how the first parameter is quite different from the rest.
2. Just drop the getindex sugar. We can still use @withmodel to automate the insertion of WithModel arguments. The problem with @withmodel is that it's really only convenient when you have a bunch of different methods all indexed by the exact same model.
3. Reintroduce abstract type Model end but retain this PR's handling of type parameters (so the same model can still be used for many different theories, which is certainly the most important benefit that came from this PR. We should ask ourselves if we ever want to be able to declare such-and-such (arbitrary type) is a model of such-and-such theory (e.g. I declare that Int is a model of ThCategory and my implementation is that of categories generated by path graphs vs I'm forced to create a type struct PathGrphCat <: Model i::Int end and then use that).

I came to this realization because I wanted to write pullback[FinSet()](f, g) in some test file. However, pullback[m] is just sugar for limit[m](Cospan(f,g)), where limit is the name of the term constructor that actually appears in ThCategoryWithPullbacks. So because pullback does not explicitly appear in any theory, there was no getindex method generated for it. So I'd have to write pullback(WithModel(FinSet()), f, g). This surprised me because I hadn't had this problem for product or equalizer etc., but that's because those names have appeared as constructors in some theory (doesn't matter which), thus the getindex(::typeof(product), m) method gets generated. This seemed bad.

What would be nice is to just define once

Base.getindex(any_method, any_model) = args -> any_method(WithModel(any_model), args...)

Which is blatant type piracy that brought this all to my attention.

So, one argument for option 3 above is that we could do this:

Base.getindex(any_method, any_model::Model) = args -> any_method(WithModel(any_model), args...)

Or perhaps with any_method::Function.

I think that requiring a fixed super type for models or methods would really limit the utility of this whole goal. Can we provide a macro that is a thin wrapper around function definition that lets users register the method with the model and generate the right method definition to avoid piracy?

The problem is that we can't overload getindex withour specializing on the type of the model or the type of the function. But if we used a manual opt-in, you would have those types to define specialized methods.

I think you're suggesting a macro that take a function name (e.g. pullback) and defines a method

Base.getvalue(::typeof(pullback), m::WithModel{T}) where T = xs -> pullback(m, xs...)

I agree this is nicer than making some random theory with pullback as a term constructor in order to make @theory do this. One could even do this for specific T's, though I don't see how that could be useful yet.

This doesn't address the problem of needing to sprinkle in WithModel when one calls compose[WithModel(nothing)](nothing, nothing) but I think that's a minor inconvenience. Also I think we should just replace WithModel with Model. Then Model is a wrapper one encases a value in to say "use this as a model" (in particular, when indexing a method name).