Redesign Proposal

[0x0f0f0f]

cc @shashi @willow-ahrens @YingboMa - based on #21 :)

[codecov-commenter]

Codecov Report

Attention: 11 lines in your changes are missing coverage. Please review.

Comparison is base (f43e305) 42.85% compared to head (59da1f7) 57.50%.

Files	Patch %	Lines
src/TermInterface.jl	65.00%	7 Missing ⚠️
src/expr.jl	69.23%	4 Missing ⚠️

❗ Your organization needs to install the Codecov GitHub app to enable full functionality.

Additional details and impacted files

@@             Coverage Diff             @@
##           master      #22       +/-   ##
===========================================
+ Coverage   42.85%   57.50%   +14.64%     
===========================================
  Files           3        2        -1     
  Lines          28       40       +12     
===========================================
+ Hits           12       23       +11     
- Misses         16       17        +1     

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

[willow-ahrens]

I'm happy to review this week, but I don't have time today.

[0x0f0f0f]

I'm happy to review this week, but I don't have time today.

No worries!

[0x0f0f0f]

SU mostly uses => rules where the rhs is evaluated. We also support -> (soft) rules where the RHS of a rewrite rule is a PatTerm (defined in Metatheory.jl) and substituted via a simple traversal.
This was the previous implementation.

function instantiate(left, pat::PatTerm, mem)
  args = []
  for parg in arguments(pat)
    enqueue = parg isa PatSegment ? append! : push!
    enqueue(args, instantiate(left, parg, mem))
  end
  reference = istree(left) ? left : Expr(:call, :_)
  similarterm(reference, operation(pat), args; exprhead = exprhead(pat))
end

Where left is the expression that matched on the LHS pattern, and pat::PatTerm is the RHS of the rule.

You can see that it is rather hacky and defaults to Expr if the matched expression is not a tree.

Patterns for rules have their own term type, so it means that under this redesign they should have their own head type.
This means that (@rule f(~a) -> 1).left == PatTerm(PatHead(:call), :f, [:a]).

If we change the last line of instantiate to maketerm(head(pat), (operation(pat), args...)), then something like @rule(f(~a) -> g(~a))(:(f(2))) will return PatTerm(PatHead(:call), :f, [2]), while the original expression to be matched against was an Expr.

There's no easy solution that comes to my mind, other than adding some machinery to "infer" the head type from a reference.

[0x0f0f0f]

I guess the solution is having some mechanism to connect symtype, head and maketerm, maybe something like promote_head?

In the case @rule(f(~a) -> g(~a))(:(f(2))), if the argument is an Expr we want the result of the rewrite to be an Expr.

If it's a SymbolicUtils.Term, we may want a SymbolicUtils.Term out, but the catch is that if we have something like

r =  @rule ~a + ~b -> f(~a) 
@syms x::Int y::Int
t = x + 2 # should be a SymbolicUtils.Add
r(t) # what do we get out of instantiate?

What should be the call to maketerm in this case?

[0x0f0f0f]

I propose that the provider of a head type should also provide a makehead(::Type{NewHeadType}, ::OldHeadType) function where it can be "casted" from one head type to another. When we want to instantiate the RHS of a pattern to an Expr, we could have maketerm(makehead(ExprHead, pat.head), substituted_args), when we want to instantiate to an SU term, we then could have maketerm(makehead(SUHead, pat.head), substituted_args).

This means that Metatheory/SU/friends should have to implement

# Used when instantiating patterns to exprs
makehead(::Type{ExprHead}, p::PatHead) = p.head # p.head is a Symbol like :call etc...
# Used when instantiating patterns to SU Terms
makehead(::Type{SUHead}, p::PatHead) =  SUHead()
# Used when convertin SU terms to Expr
makehead(::Type{ExprHead}, p::SUHead =  ExprHead(:call)

We could override Base.convert but maybe it's better to just have a new name for clarity.

[0x0f0f0f]

So it turns out that makehead is not necessary.

In Metatheory we introduced AbstractPat pattern structure to have patterns that are symbolic-type independent (work with Expr, SU Terms, whatever you want).

We need to match against the head! Let's consider Expr(:tuple, :a, :b) and PatTerm(PatHead(:tuple), PatVar(:x), PatVar(:y)).

If we use == for matching (as for literals), then it will check ExprHead(:tuple) against PatHead(:tuple).

My intuition is that we will always need to store some Symbol or value in head types that corresponds to the Julia Expr head.

I will introduce a head_symbol(::Head) function that returns this value

[0x0f0f0f]

I've moved Metatheory.@matchable struct here since it only uses methods from TermInterface and it would better reside here. I've also added some tests with custom structs that better explain the usage.

[0x0f0f0f]

@willow-ahrens @shashi

Ready for review

I've made adjustments for Metatheory.jl in JuliaSymbolics/Metatheory.jl#174

[shashi]

I guess the solution is having some mechanism to connect symtype, head and maketerm, maybe something like promote_head?

> r =  @rule ~a + ~b -> f(~a) 
> @syms x::Int y::Int
> t = x + 2 # should be a SymbolicUtils.Add
> r(t) # what do we get out of instantiate?

It seems what you want is to create a term based on the head type of LHS.

So yeah in MT you can have something like construct_rhs(pattern, lhs) which in turn checks head(lhs).

It makes sense for MT to have a different @rule macro than SU, so it can rewrite RHS as Expr construction when left hand-side expr is MTExprHead, in all other cases just do the default that @rule does.?

[shashi]

I think we should go with head and children instead of tail

As discussed tail is more suitable for linked lists. And head is actually the header part of the node.

[shashi]

Again should not be in this package.

[0x0f0f0f]

While I believe this one should stay in this package.

[willow-ahrens]

This package is used to define an AST interface so that pattern matchers can match against the AST and traverse it. I think it's a little bit of a mistake to introduce @rule with the example of +(~a, ~b), because in many IRs we would want to write this as :call(+, ~a, ~b). Not all ASTs will have something analogous to a function call, and it's unclear what benefit would be derived from standardizing this notion here. operation and arguments should live in packages that define ASTs that can give these functions meaning.

TL;DR: I don't think we can define what the new meaning of operation is supposed to do in a way that captures all of its possible use cases in downstream packages, so I think it should not be in this package.

[0x0f0f0f]

Not all ASTs will have something analogous to a function call

I guess most of what the (old/current) dependents of this package do:

• Metatheory.jl AbstractPat AST for patterns
• Julia Exprs
• SymbolicUtils IIRC terms have function calls and array indexing
• Everything depending on Symbolics
• Most other symbolic mathematics packages.

[0x0f0f0f]

Maybe we can use trait like abstractrees? Will make a larger comment below

[willow-ahrens]

@shashi, do we agree now that function operation end is fine as-is, just adjust the documentation to say that this one is optional?

[0x0f0f0f]

I guess the solution is having some mechanism to connect symtype, head and maketerm, maybe something like promote_head?

> r =  @rule ~a + ~b -> f(~a) 
> @syms x::Int y::Int
> t = x + 2 # should be a SymbolicUtils.Add
> r(t) # what do we get out of instantiate?

It seems what you want is to create a term based on the head type of LHS.

So yeah in MT you can have something like construct_rhs(pattern, lhs) which in turn checks head(lhs).

Heya! Thanks for the quick reply :)

It makes sense for MT to have a different @rule macro than SU, so it can rewrite RHS as Expr construction when left hand-side expr is MTExprHead, in all other cases just do the default that @rule does.?

Hmm, I'm not really sure we have to separate out the @rule macros between MT and SU, I'd be for unifying them again.
MT is not really designed to work on Exprs or its own expression type, the goal is to make its rewrite systems work on every expression type supported by TermInterface.

If you remember from the ideas in https://arxiv.org/pdf/2112.14714.pdf - MT @rule macro is exactly designed on SU's @rule macro (and should be compatible) with a few differences.

• patterns on the LHS are <:AbstractPat (which is a custom TermInterface expression type) and should be able to match on anything that supports TermInterface, Expr, SymbolicUtils.Term and friends.
• There are 4 kinds of rule operators: => which evaluates the RHS, -> that substitutes (RHS <: AbstractPat) and ==/!= which should be bidirectional -> and work with e-graphs.

The point here is to have something such as

function instantiate(left, pat::PatTerm, mem)
  ntail = []
  for parg in tail(pat)
    instantiate_arg!(ntail, left, parg, mem)
  end
  reference_head = istree(left) ? head(left) : ExprHead
  maketerm(typeof(reference_head)(head_symbol(head(pat))), ntail)
end

This currently works in JuliaSymbolics/Metatheory.jl#174

The whole idea was to abstract away the logic required for patterns and rewrite systems from the specific implementation of the symbolic types, LMK what you think.

[0x0f0f0f]

Applied some suggestions. So you'd say that head_symbol, operation and arguments should be out of this package. Nice observation, as I'm also undecided on these points.

First, thanks for the idea, it really simplified a lot of MT logic and makes thing a lot lispier than before.
Will reply to the other points with concrete ideas, but i'll need to think a bit about them. I believe that yeah, having these many methods is a bit messy.

I would still go towards the layered architecture as a high-level goal

1. TermInterface : abstract interface and default implementation for whatever is and will be in Julia Base.
2. Metatheory : general purpose patterns, @rules, combinators and e-graphs for anything that implements TI
3. SymbolicUtils : optimized types for maths, total ordering on the symbolic expressions etc...
   ... and so on

RN there's a lot of code duplication across MT and SU, but that's fine, if we reintegrate this as in the original project it should be broken down in smaller steps.

Some concepts

• MT shoud work with all head types from all packages that support TermInterface.
• MT should pattern match <:AbstractPat with PatHead (constructed from a Julia DSL) against all head types.
• operation is a different concept from head
• operation and head will be likely used in all packages that implement this interface (MT, SU, friends...). if we have a term representing f(x) i think it's a bad idea for any implementer to encode f in the custom head. it should be head(f(x)) => CustomHead() and operation(f(x)) => f. (same tango for arguments/children)
• This CustomHead object should store some notion of "function application" - which is the same concept of :call for Julia Exprs.
• Separating operation and head makes pattern matching on everything that implements TI a lot easier, but operation is still needed around.

If you take a look at JuliaSymbolics/Metatheory.jl#174 in
https://github.com/JuliaSymbolics/Metatheory.jl/pull/174/files#diff-4d29e6d52e6f1fc5ccebff8ccf5fec0adf695a056f60253e5b87e785a65e4509

You can see what i had in mind for the difference between head/operation. It's the pretty much the same code and logic as in SU matchers with some minor differences.

[0x0f0f0f]

@shashi thought a bit about it. It's fine to move head_symbol to Metatheory.jl (still required to define interoperability, conversions between symbolic types and a general purpose matcher), while i believe operation and arguments should stay here. They're mostly universal.

[0x0f0f0f]

@shashi thought a bit about it. It's fine to move head_symbol to Metatheory.jl (still required to define interoperability, conversions between symbolic types and a general purpose matcher), while i believe operation and arguments should stay here. They're mostly universal.

@willow-ahrens what do you think?

[willow-ahrens]

This is a great start! At a high level, I suggest:

1. Remove operation and arguments, but leave documentation about where they went and why.
2. Let's talk about an AST builder macro in a separate PR, I like the idea and might use it myself but it deserves a separate PR.

[willow-ahrens]

This package is used to define an AST interface so that pattern matchers can match against the AST and traverse it. I think it's a little bit of a mistake to introduce @rule with the example of +(~a, ~b), because in many IRs we would want to write this as :call(+, ~a, ~b). Not all ASTs will have something analogous to a function call, and it's unclear what benefit would be derived from standardizing this notion here. operation and arguments should live in packages that define ASTs that can give these functions meaning.

TL;DR: I don't think we can define what the new meaning of operation is supposed to do in a way that captures all of its possible use cases in downstream packages, so I think it should not be in this package.

[willow-ahrens]

x is no longer defined here.

[willow-ahrens]

This is fine, though I wonder if AbstractTrees could help here.

[willow-ahrens]

This approach to building ASTs results in huge slowdowns in compilers, because compilers specialize on each combination of node types. I appreciate the idea of adding an optional AST easy implementation feature, could we add it in a separate PR?

A few ideas:

• enforce symbols or enums to differentiate heads in the AST (runtime not inference time)
• make it clear that head_symbol is not part of the TermInterface interface, it's just part of the easy-mode ast builder.
• add a simplified approach towards types with dynamic field information. Because we would emit types that have the same type for every head, we would need to use dynamic field information.

If we feel like an optimized AST implementation is out of scope, we shouldn't include programming patterns that will inconvenience users later on with performance issues.

[willow-ahrens]

This file seems like the right approach to me

[0x0f0f0f]

Since we came to the point that there are basically two styles of encoding operations (function calls) in ASTs and most downstream packages will use operation and arguments, why don't we define a trait like in https://github.com/JuliaCollections/AbstractTrees.jl/blob/master/src/traits.jl (or JSON3 StructTypes and friends)?

If an AST doesn't encode function calls, then there's no need to define or use such trait or functions, one can just use head and children, but if it does encode funcalls (as most of the packages in Julia for code/symbolics will), then one could more or less define the trait for the function call interface.

This is the trait definition

# First, I would define an `AbstractASTHead` 
abstract type AbstractASTHead end 

# trait def in TermInterface
abstract type CallStyle end

# Provider of expression type has to define CallStyle on `head(x)` how to access the "operation" of `x`
struct OperationInNode <: CallStyle
# Operation is straightforward
struct OperationInFirstChild <: CallStyle

operation(x) = operation(CallStyle(head(x)), x)
operation(::OperationInFirstChild, x) = first(children(x))
# operation(::OperationInNode, x) depends on the expression type
arguments(x) = arguments(CallStyle(head(x)), x)
arguments(::OperationInFirstChild, x) = children(x)[2:end] # or some efficient alternative
arguments(::OperationInNode, x) = children(x)

User definitions

struct ExprHead <: AbstractASTHead 
    head::Symbol 
end
istree(x::Expr) = true
head(ex::Expr) = ExprHead(ex.head)
children(ex::Expr) = ex.args
CallStyle(h::ExprHead) = h.head == :call ? OperationInFirstChild() : OperationInNode() # or better def for macrocall and friends
maketerm(h::ExprHead, children) = Expr(h.head, children...)

# definition of operation(::OperationInFirstChild, ::Expr) and arguments comes for free
operation(::OperationInNode, ex::Expr) = ex.head


# =========================

struct SUHead <: AbstractASTHead 
    operation
end
maketerm(h::SUHead, children; kw...) = h.operation(children...; kw...) # as old similarterm worked
istree(x::Symbolic) = true # replace Symbolic with concrete types that are tree
head(x::Symbolic) = SUHead(directly_access_the_operation(x)) # replace Symbolic with concrete types that are tree
children(x::Symbolic) = ... # directly access the children of concrete types that are tree
CallStyle(h::SUHead) = OperationInNode()

operation(x::Symbolic) = head(x).operation
# definition of arguments comes for free.

Although this seems convoluted, it may solve the problem?

[willow-ahrens]

Could you make a separate optional package that defines an ast for function calls that people can opt in to? What are the upsides to formalize operations and arguments in this package?

[0x0f0f0f]

Could you make a separate optional package that defines an ast for function calls that people can opt in to?

That can be an idea, but then we would have TermInterface + additional packages + Metatheory + SymbolicUtils and it can be too many packages (we had one for rewriters) - changing a little thing in one package required a minor release in downstream. I guess it would be nice to pack this functionality in TermInterface and make it opt-in. This package is incredibly small compared to AbstractTrees

[0x0f0f0f]

Any ideas on how to proceed?

[ChrisRackauckas]

We're going to have a meeting to discuss changing the Symbolics internals. I think making sure things hit the same interface is fine, but what went wrong last time is this depended on metatheory. The interface should have no dependence on any implementation.

@AayushSabharwal

[0x0f0f0f]

We're going to have a meeting to discuss changing the Symbolics internals. I think making sure things hit the same interface is fine, but what went wrong last time is this depended on metatheory. The interface should have no dependence on any implementation.

@AayushSabharwal

Thanks, let me know if it's possible to join the meeting.

I agree that we first have to focus on designing this interface so that it can capture all different styles of term construction in a performant way, abstracting away the implementation details to allow package interoperability. I think maketerm is a good idea, but operation/arguments are still crucial to all the dependents of this interface.

I propose that this package should have very little to zero external dependencies (@willow-ahrens), and we should use traits (or something analogous) to abstract away how terms are constructed/accessed. This is to avoid abstraction leaks and the exprhead situation again.

This is not just for Expr/SU.Term/PatTerm situation, but can be important in case we want to introduce fundamental data structure performance improvements (like it was for UniTyper, or how it will happen now with Apter Trees in Metatheory).

In the meanwhile I'll temporarily drop the TermInterface dependency in Metatheory, and use this current version. I have some large overhauls and performance improvements pending, I'l focuse on those and wait until we have consensus on this package to reintegrate TermInterface. I'm aiming to have it perform close to the rust implementation such that we can proceed exploring real world optimizations.

I also agree that we first focused on unifying the rewrite systems instead of real world applications.
The goal of having an unified rule language/pattern matcher will remain Metatheory.jl's priority and it's not urgent to integrate it in SU. Once MT reaches maturity with real world applications, it can then be interesting again to try to unify the architecture.

While it will be possible to rewrite on SU terms in MT, SU rules will not be available to be used in MT and vice-versa, even though => rules will be have almost identical behavior and the pattern language will have the same syntax (it will still be compatible).

---

Summarizing, I propose some concrete goals for the TermInterface redesign proposals:

• Capture all use cases: avoid splitting a very small package in even smaller packages.
• Abstract away the "operation as head vs operation as first child" problem.
• Abstract away the exprhead problem so that Metatheory can still have its generic pattern matcher macro language work on any expr type, and work on SU terms.
• Do not impact performance of SU/MT.
• Abstract away access to different data structures: trees, apter trees, expressions with a centralized hash-consed context, etc...

[shashi]

I'm generally against Making the Symbolics dependency chain include Metatheory.

I think SU and Metatheory should both depend on TermInterface and not on each other. That's kinda the whole point of this package. I support repeating code for @rule macro in both packages. I think it's one of those cases where repeating code is great for reducing headaches, and allowing future improvements. SU pattern matcher has been working for us since it was first written, so I don't want to complicate the situation and confuse who maintains what.

I think the trait situation is fine but we can solve the problem by having both operation and head and within each implementation, having operation fail if it does not make sense for an AST node? I don't want too many features to distract from the core primitives.

[willow-ahrens]

With time, I'll take back the part of my review asking to remove function operation end. I agree with Shashi, function operation end is fine here, and implementations can choose to implement if they like, no traits necessary. Just be sure to specify that it's optional. If we make these minor changes and then remove the @matchable code for a separate PR, I think we're all in agreement then? With those changes, I think that I can move Finch to depending on TermInterface, which is kinda cool.

[0x0f0f0f]

I'm generally against Making the Symbolics dependency chain include Metatheory.

I think SU and Metatheory should both depend on TermInterface and not on each other. That's kinda the whole point of this package. I support repeating code for @rule macro in both packages. I think it's one of those cases where repeating code is great for reducing headaches, and allowing future improvements. SU pattern matcher has been working for us since it was first written, so I don't want to complicate the situation and confuse who maintains what.

@shashi Yeah, I agree now that at the current state of things, maintaining them separate is fine :) - didn't know at the time that it was going to cause headaches, there's still room for lots of performance improvements and Metatheory.jl 's @rule is the right place to experiment in. agree with you here

I think the trait situation is fine but we can solve the problem by having both operation and head and within each implementation, having operation fail if it does not make sense for an AST node? I don't want too many features to distract from the core primitives.

I've just solved the whole "exprhead" issue, and aligned more to your original proposal with a simple trick: an extra function is_function_call(expr) that is true when istree(expr) and it represent a function call. That's it. SU can just set it true for everything that is not an array indexing operation

Thus I have a working version of TermInterface in this branch JuliaSymbolics/Metatheory.jl#185 that has

• istree
• is_function_call
• head (old operation)
• children (old args)
• maketerm(T::Type, children; is_call = true, type=Any, metadata=nothing)

No traits, no exprhead, no definition of Head types. maketerm dispatches on the type of the expression, and that's it. @willow-ahrens it also solved the issue with @matchable defining its Head type.

I've tested it and it helped me make Metatheory 15 times faster than the rust implementation, this is big!

I'll soon update this proposal with more motivations and explanations, file is here https://github.com/JuliaSymbolics/Metatheory.jl/blob/db4664de6e22dfa63b72d27c43f5f512210cbef4/src/TermInterface.jl

[willow-ahrens]

I will reiterate that I would like to review the @Matchable macro in a separate PR. Its an unrelated change and deserves discussion and I wouldn't want that to hold this PR up.

I'm fine with an is_function_call trait, provided it specifies that only if true, the user should define operation and arguments.

I'll make a PR to this one with my proposed compromise (just a subset of what's here already), and if people are okay with what I propose I'll test that I can use it with Finch and friends.

[0x0f0f0f]

I will reiterate that I would like to review the @Matchable macro in a separate PR. Its an unrelated change and deserves discussion and I wouldn't want that to hold this PR up.

I'm fine with an is_function_call trait, provided it specifies that only if true, the user should define operation and arguments.

I'll make a PR to this one with my proposed compromise (just a subset of what's here already), and if people are okay with what I propose I'll test that I can use it with Finch and friends.

@willow-ahrens I've pushed my update

[willow-ahrens]

This redesign appears to directly contradict #21 (comment), specifically, that the old arguments(x) is the new tail(x)[2:end] and the old operation(x) is the new arguments[x](1).

[willow-ahrens]

@shashi, do we agree now that function operation end is fine as-is, just adjust the documentation to say that this one is optional?

[willow-ahrens]

This is exactly what this redesign had hoped to avoid! We don't want head to be the function being called. We want it to be :call and we want children(x)[1] to be the function being called.

[0x0f0f0f]

I thought we wanted to avoid the concept of :call as "exprhead".

In my latest commit head is the old operation, and children is the old arguments.

If we add both head,children and operation,arguments Metatheory.jl would just rely on operation and arguments for pattern matching. I guess the same for SU.

But what about SymbolicUtils terms? t = f(a,b) in SU would have operation(t) == f, arguments(t) == [a,b], children(t) = [f,a,b], what about head(t)? Should it be SUHead()?

I kinda dislike the idea that the users should define a struct to define the head of an AST node, all the information required to inspect, manipulate and create new terms is already contained in the type of the term.

[willow-ahrens]

Why not default this to false? If it's an optional interface, why do we require users to define it?

[0x0f0f0f]

I would not make this optional. Defaulting it to false may cause users to forget to set it on specific term types, and thus cause hard to catch bugs as it would propagate through all the rewriting steps (it happened to me and i lost a few hours just to understand i was dispatching on the wrong type and was defaulting to false).

In comparison to the previous state of this redesign, where we had Head types, in this latest version, the provider of a term types T <: AbstractT just has to set is_function_call(<:AbstractT) = true if the whole language is functional, or set it to false if the entire AST does not have function calls

[0x0f0f0f]

@willow-ahrens @shashi - if i rename head and children in this current commit to operation and arguments, the behavior will stay unchanged. The only difference is no more similarterm, but maketerm instead, and how it handles and dispatches expression types.

Together with a mandatory is_function_call(::ExprType)::Bool, this completely solved the issue of exprhead and friends. If we release it in this state, re-integrate it in SU and MT, then I could release an alpha of MT-3.0 and make it usable to rewrite SU terms with e-graphs.

Can we do this redesign gradually?
We could think about the opportunity of adding ExprHead and SUHead in a later MR, as the allocations/creation time of these head objects slowed down Metatheory.
When not using head types, and just using the type of an expression to characterize them, there was a HUGE performance difference, it was much faster (both in SU terms, Expr and custom term types).

[ChrisRackauckas]

Do we need a call to go through the different re-design proposals?

[0x0f0f0f]

Do we need a call to go through the different re-design proposals?

That would be great. I can prepare some notes comparing the proposals. I'm planning to release MT 3.0 before the summer as I'd like to present it at the e-graphs community workshop. This is fundamental for the progress of the project.

[0x0f0f0f]

Just pushed with the latest proposal we agreed in the call