get rid of the fourth argument of `maketerm`, `type` about terminterface.jl

[willow-ahrens]

There's a few ways we could do this:

1. I'm not sure there's a strict rule excluding metadata from considering in the hash
2. We could put types in leaf node constructors, since leaf nodes don't adhere to similarterm/maketerm interface. This is what I do in Finch.
3. We could make a TypeAssert node in the language. Several languages, including C and Julia, put types in the syntax of the language.

[0x0f0f0f]

What's a "typed S-expression"?

if an S-expression is (f x y z) then a typed s-expression can be (typed (f x y z) t) ? I will improve the docs. It makes a bit more sense if instead of s-expressions you think about it as lambda calculi.

[bowenszhu]

In SymbolicUtils.jl, symtype is a parameter of the parametric type typeof. For example,

using SymbolicUtils

@syms x::Complex{Int64}

t = typeof(x)                   # SymbolicUtils.BasicSymbolic{Complex{Int64}}
s = SymbolicUtils.symtype(x)    # Complex{Int64}

here the symbolic object x is of type BasicSymbolic{Complex{Int64}} and its symtype is Complex{Int64}. Calling typeof in SymbolicUtils.jl actually includes the information of symtype, so it is fine to remove the 4th argument type from maketerm(T, head, children, type=nothing, metadata=nothing) as the 1st argument T incorporates the numeric types.

[0x0f0f0f]

It's planned to be supported by Metatheory.jl 3.0, but can also be aggregated with metadata. This needs discussion for the SymbolicUtils.jl implementation. @shashi

[shashi]

Type and metadata have quite specific meanings. Metadata is layered on top of data, the hash of an object for example does not depend on its metadata but depends on the type it's like "data in the shadows". Type is used to represent the typed S-expression.

I'm fine with doing something that makes sense for other packages and also does not make it awkward for SU.

[nsajko]

If type is really useful for expressions in general it should be documented in an understandable way.

the hash of an object for example does not depend on its metadata but depends on the type

Can't you just change that, seems like an implementation detail?

Type is used to represent the typed S-expression.

What's a "typed S-expression"?

[ChrisRackauckas]

Can't you just change that, seems like an implementation detail?

I don't think so? The same expression but of a different type is a different expression.

[willow-ahrens]

Thanks everyone for working to make this package better. I have a few thoughts on this, I hope they help the discussion.

The same expression but of a different type is a different expression.

If this is true, perhaps the type should also be an expression itself, as Alessandro suggests. I think packages that are not SU often just do:

Base.isequal(a::MyTerm, b::MyTerm) = head(a) == head(b) && (!istree(a) || children(a) == children(b))

I've gotten away without the type parameter in https://github.com/willow-ahrens/SyntaxInterface.jl and https://github.com/willow-ahrens/RewriteTools.jl (my simplified forks of SU) and things have been okay.

In many ways, symtype feels like a SU-specific cached analysis of the terms. For example, we could probably write

symtype(x) = promote_op(operation(x), arguments(x)...)

just as we would write

hash(x, s) = hash(head(x), hash(children(x), s))

SU is able to cache the latter analysis without the help of TermInterface.

symtype is really only a useful concept for expressions that represent function calls. We can construct fancy meanings for it outside of that, but I haven't seen any packages actually using those definitions.

If I am writing a generic symbolic transformation, I would just ask whether we really want to define "code that respects the TermInterface" to mean that my transform needs to correctly manipulate symtype over generic expression types?

I think that already there's some confusion about what symtype means. For example, if I define a new term type the default behavior is symtype(x::MyTerm) = typeof(x), which is MyTerm, which feels incorrect against symtype(t::Term) = Number. We also have symtype(1) = Int and symtype(:(1+1)) = Expr.

Another question: Could you help me define symtype for my use case? I do keep track of the types of things, but I am able to do it outside of a symtype interface and my analysis of types does not extend to statement nodes: https://github.com/willow-ahrens/Finch.jl/blob/main/src/FinchNotation/nodes.jl

I'll conclude with a few proposals for alternate ways to handle symtype

1. delete it.
2. delete it and allow arbitrary metatdata kwargs instead of wrapping everything up in one metadata argument, so we can do maketerm(MyTerm, head, children..., type=Int, hash=0x..., etc...)
3. Make symtype only apply when iscall(term) == true

[0x0f0f0f]

Nice ideas @willow-ahrens. 1. and 2. sound OK, but wouldn't the compiler specialize a new method for each kwarg provided? that's likely avoidable. See #35 from @nsajko

I do agree that symtype defaulting to the type of the expression feels wrong. It's not used anymore in Metatheory, and it feels like a fossil from earlier releases.

Moreover, most instances of maketerm in SU all rely on "passing" the metadata and symtype to the appropriate constructor

function TermInterface.maketerm(::Type{<:BasicSymbolic}, head, args, type, metadata)
    basicsymbolic(head, args, type, metadata)
end

Which could just become

struct SymbolicMetadata
symtype::Type
# whatever...
end

function TermInterface.maketerm(::Type{<:BasicSymbolic}, head, args, metadata::Union{Nothing,SymbolicMetadata})
    stype = isnothing(metadata) ? nothing : metadata.symtype
    basicsymbolic(head, args, stype, metadata)
end

[0x0f0f0f]

I mean, that's already what happens in basicsymbolic....

function basicsymbolic(f, args, stype, metadata)
    if f isa Symbol
        error("$f must not be a Symbol")
    end
    T = stype
    if T === nothing
        T = _promote_symtype(f, args)
    end
    if T <: LiteralReal
        Term{T}(f, args, metadata=metadata)
    elseif T <: Number && (f in (+, *) || (f in (/, ^) && length(args) == 2)) && all(x->symtype(x) <: Number, args)
        res = f(args...)
        if res isa Symbolic
            @set! res.metadata = metadata
        end
        return res
    else
        Term{T}(f, args, metadata=metadata)
    end
end

WDYT? I'm in favor of deleting symtype and type args from TermInterface.jl

[ChrisRackauckas]

Is this actually correct? How do you have the type in the hash if it's in the metadata? Since part of the identity of a value is its type, I don't quite see how you can get this correct.

[nsajko]

How do you have the type in the hash if it's in the metadata?

As Willow also says in the first point, I don't see why should metadata be excluded from consideration in isequal/hash of expressions.

[ChrisRackauckas]

What happens when the metadata is modified to add a key after the symbol is constructed, as is common? Won't that change the hash?

[ChrisRackauckas]

Okay if it's already in the type parameters then it's redundant information and the symtype function should just use:

@assume_effects :total __parameterless_type(T)=Base.typename(T).wrapper
parameterless_type(x) = parameterless_type(typeof(x))
parameterless_type(x::Type) = __parameterless_type(x)

I don't quite get why @shashi had it in the values and the parameters then.

[ChrisRackauckas]

Also, please no 0 ver... I'm just going to do the v1.0 release right here so we can maintain this.

[bowenszhu]

1. I'm not sure there's a strict rule excluding metadata from considering in the hash

In SymbolicUtils.jl, the numeric type symtype is not a part of metadata. metadata is mainly used in ModelingToolkit.jl for storing description, bound, unit, etc. See https://docs.sciml.ai/ModelingToolkit/stable/basics/Variable_metadata/

We do exclude metadata from the computation of hash in SymbolicUtils.jl, because

1. hash computation could get expensive when more and more variants of metadata are added
2. in SymbolicUtils.jl, we keep hash equality <==> symbolic expression equivalence (mathematically equivalent expressions of different symtype or symbolic tree structures are not considered equivalent)