get rid of the fourth argument of `maketerm`, `type`

[nsajko]

maketerm(T, head, children, type=nothing, metadata=nothing)

Constructs an expression. [...], type is the type of the S-expression.

What is the meaning of the type argument here? "Type of the sexp" means nothing to me, sexps don't have type?

Originally posted by @nsajko in #25 (comment)

The fourth argument, type, seems like it's not generally useful for expressions, and redundant with the next argument, metadata. Is there any reason why it should exist in this interface?

I notice that the in-development version of Metatheory.jl that supports the current TermInterface.jl always ignores both type and metadata, and so will my package. EDIT: actually my package does use metadata for some types.

Was type only introduced to make things slightly more convenient for the SymbolicUtils.jl implementation?

[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.

[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.

[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.

[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.

[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?