Annotating Decapodes with types

[lukem12345]

Currently, Decapodes are flexible. That is, an object of the type SummationDecapode could represent equations in the 2D Exterior Calculus, or 1D Exterior Calculus, and so on.

Programming with Decapodes would become more well-typed if the Decapode objects had something like a type parameter with the degree of the DEC being used. Compilation steps like type inference could then automatically pick the correct set of inference rules.

The typing system could most likely be improved in other ways, but some brainstorming needs to happen first.

[jpfairbanks]

The easiest thing to implement would be a wrapper struct with 2 fields, the dimension::Int and the current acset struct.

The most category theoretic approach would be to make a decapode for the de Rahm complex for each dimension. Then a decapode with respect to a specific dimensionality would be an ACSet transformation into that de Rahm complex. That fits nicely with the Typed ACSet perspective from the stratification setup and the HypSigma approach used for Wiring Diagrams over a specific SMC. Decapodes are basically DWDs encoded as HypSigma where we are using the attributes to encode the map into the algebraic signature instead of using ACSet Transformations.

[jpfairbanks]

If we do option 2, then we can apply the fundamental theorem of presheaf toposes to convert a typed Decapode into a presheaf where there is a table for each type. Not sure if that is ever useful, but it would be theoretically consistent.

[lukem12345]

@quffaro What do you feel is the fastest way to implement this feature? This is so users do not have to do:

infer_types!(pode, op1_inf_rules1d, op2_inf_rules1d)
resolve_overloads!(pode, op1_res_rules1d, op2_res_rules1d)
gensim(pode, dimension=1)

Would implementing @decapode dimension begin ... end be a headache?

This is the first practical QoL feature that would be gained as we consider adding new types of DiagrammaticEquations, via whatever means.