Interop with SymbolicUtils

[olynch]

This is a more-or-less feature-complete conversion between DecaExpr and an equivalent data structure built on SymbolicUtils, but it requires some testing/naming bikeshedding.

[lukem12345]

@GeorgeR227 Looks like this should get rebased onto https://github.com/AlgebraicJulia/DiagrammaticEquations.jl/pull/54 ; there is apparently some redundancy in dicts for typing/ untyping symbols.

[GeorgeR227]

@GeorgeR227 Looks like this should get rebased onto #54 ; there is apparently some redundancy in dicts for typing/ untyping symbols.

I'm not sure because in this case OPERATOR_LOOKUP is taking typed names down to generic names. In that PR we take those typed names down to a single representative which is still typed. It's true that they're similar but their purposes feel different.

[lukem12345]

Yes the rebase is for purposes of grouping together code that accomplishes similar tasks.

[jpfairbanks]

Instead of creating julia functions for the operators of the DEC, could we just create SymbolicUtils function types?

https://github.com/JuliaSymbolics/SymbolicUtils.jl/blob/df8e84d31e60f4dc70f0df2ad88ede91f6f3fd27/src/types.jl#L913

That is what you get when you do:

julia> @syms f(x)::Complex
(f(::Number)::Complex,)

You can construct function types with SymbolicUtils.Sym{SymbolicUtils.FnType{Tuple{Real,Real}, Complex}}(:h) so these are what should come out of registering a new function type and be used to represent the basic DEC operators. That way any code that expects function types will work for our DEC operators.

[codecov[bot]]

Codecov Report

Attention: Patch coverage is 16.20112% with 150 lines in your changes missing coverage. Please review.

Project coverage is 74.90%. Comparing base (55d2972) to head (0a314a8). Report is 7 commits behind head on main.

Files with missing lines	Patch %	Lines
src/SymbolicUtilsInterop.jl	1.38%	71 Missing :warning:
src/deca/ThDEC.jl	1.51%	65 Missing :warning:
src/symbolictheoryutils.jl	65.85%	14 Missing :warning:

Additional details and impacted files

```diff @@ Coverage Diff @@ ## main #64 +/- ## =========================================== - Coverage 86.80% 74.90% -11.90% =========================================== Files 13 16 +3 Lines 894 1068 +174 =========================================== + Hits 776 800 +24 - Misses 118 268 +150 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

[lukem12345]

An implication of Decapode type-inference that seems baked-into this PR is that it is assumed that the choice of primal/ dual is completely inferable based on the types of the parents. However certain operations such as the musical isomorphisms or wedge products can either return a primal or dual form depending on the discrete operator chosen. Note also that for any Decapode, there are multiple means of specifying whether forms are primal or dual. Performing type inference via breadth-first or depth-first traversal at parse-time biases the system towards only representing certain discretizations. In certain cases, choosing a particular discretization for a certain variable or operation may constrain successor operations to certain discretizations, for which CombinatorialSpaces may not yet offer a method. And so a satisfiable model may not be returned, although one may exist.

The appearance of dual complexes leads to a proliferation of the operators in the discrete theory. For example there are primal-primal, primal-dual etc. versions of many operators. This is of course unique to the discrete side.

• Hirani, Discrete Exterior Calculus

Resolving this issue by allowing the Decapode macro to represent any formal combination of terms should simplify parsing logic. As it stands now, some algebraic rules are implicit in the code that parses the body of the macro, and other algebraic laws are (will be) encoded as rewrite rules.

[jpfairbanks]

We can always do dispatch on return type to let you write sharp(Dual, x)

[lukem12345]

Yes but that is still local. The issue I described is not with choosing which functions to emit once types have been decided. It is an issue with deciding types.

[jpfairbanks]

I'm moving a comment from @quffaro from inline reply to top level comment so that it stays here after we change the code and mark that thread resolved:

Tests currently pass with exception to klausmeier. To get it working, @jpfairbanks suggested a @register macro to add function terms. However I'm not sure if I'm understanding completely, so I'm seeking clarification.

Currently (in this PR), for a given operator we define two methods:

1. a Julia function over ThDEC for checking its type. They are aggregated in a OPERATOR_LOOKUP const. This step is analogous to SymbolicUtil's promote_symtype
2. a Julia function over DecaSymbolic, our type for the SymbolicUtils implementation of ThDEC, which calls (1) for validation

we use the OPERATOR_LOOKUP to also check if a model has admissible terms (e.g., Δ), so we want the ability to append the OPERATOR_LOOKUP by @registering new functions.

@register foo(x::Scalar)::Scalar = x + 1
# codegens
foo(s::Scalar) = Scalar
foo(x::BasicSymbolic{T<:DECType}) = begin
    s = foo(Sort(T)) # TYPE CHECKING
    Sym{FnType{Tuple{Number(s)}, Real}(foo)
end

Another example comes with a hazard: PrimalForm{T} is a parameterized type, but PrimalForm::Sort is a function. If we want to continue typechecking with ThDEC types, do our current way of checking signatures, we need to make sure codegen for typechecking supports the engineering task to do this.

@register foo(x::PrimalFormT{1})::PrimalFormT{1}
# codegens
foo(x::Form) = @match x begin
    PrimalForm(1) => PrimalForm(1)
    _ => error
end

The steps:

Suppose we wanted to add foo to the OPERATOR_LOOKUP dictionary. Notice PrimalFormT{1} is the DecaSymbolic type, which accepts parameters.

@register foo(x::PrimalFormT{1})::PrimalFormT{1} = map(x) do val
  val  ^ 2
end

We need to define its (1) type-checking (src/ThDEC), (2) its DecaSymbolic implementaton (src/decasymbolic), and possibly (3) its implementation.

We define the implementation of a function

func(x::PrimalFormT{1})::PrimalFormT{1} = map(x) do val; val ^ 2 end

:question: Where does this live? Does this act on BasicSymbolic terms?

Next, we define it symbolically:

symfunc = Sym{FnType{Args, Real}}(ThDEC.func)

Then, we add it to OPERATOR_LOOKUP (possible haskey validations omitted)

ThDEC.OPERATOR_LOOKUP[op] = func

:question: Currently OPERATOR_LOOKUP is typed as Dict{Symbol, Function}. Is the intent to change Dict{Symbol, SymbolicFunction} and do typechecking by replacing the # TYPE CHECKING (above) line with promote_symtype?

[jpfairbanks]

We define the implementation of a function

func(x::PrimalFormT{1})::PrimalFormT{1} = map(x) do val; val ^ 2 end

❓ Where does this live? Does this act on BasicSymbolic terms?

I am rethinking my idea to define the implementation here. The implementations will often need to refer to parts of the mesh, including vertex coordinates or volumes of a simplex. So we should reserve this syntax for defining a new function symbol and a definition in terms of more primitive functions that could get turned into a rewrite. So that you could register a function like

f, r = @register f(v::PrimalFormT{1},x::PrimalFormT{0})::PrimalFormT{1} = d(Δ(x)) + (v  ∧ x)

and have that expand out to

f, = @syms f(v::PrimalFormT{1},x::PrimalFormT{0})::PrimalFormT{1}
r = @rule f(~v::PrimalFormT{1},~x::PrimalFormT{0})::PrimalFormT{1} => d(Δ(~x)) + (~v  ∧ ~x)

Next, we define it symbolically:

symfunc = Sym{FnType{Args, Real}}(ThDEC.func)

Then, we add it to OPERATOR_LOOKUP (possible haskey validations omitted)

ThDEC.OPERATOR_LOOKUP[op] = func

❓ Currently OPERATOR_LOOKUP is typed as Dict{Symbol, Function}. Is the intent to change Dict{Symbol, SymbolicFunction} and do typechecking by replacing the # TYPE CHECKING (above) line with promote_symtype?

I think that we can create a function for each DEC operator, then create a symbolic function with that function as the head.

function Δ end
Δ, = @syms Δ(x::PrimalFormT{0})::PrimalFormT{0}

If the function symbol we are creating needs to do dispatch, then it should overload promote_symtype to hook that logic into SymbolicUtils the way that it is expected.

[lukem12345]

https://github.com/AlgebraicJulia/DiagrammaticEquations.jl/issues/35

I think using a defintion operator := like that mentioned in this old issue would be nice.