Pattern argument of match is reduced before calling while it can return result without being reduced

[noskill]

(:= (Green Sam) True)
(= (Green Tom) False)
!(println! (match &self (:= (Green $who) True) ($who is really green)))

The second line (= (Green Tom) False) changes output
Without it program prints "(Sam is really green)" with it matching fails

[Necr0x0Der]

I'm not sure this should be called a bug. Apparently, when you have (= (Green Tom) False) defined, you specifies a non-total function Green. Substituting it to the query may suppose that you evaluates (Green $who) to False with grounding $who to Tom. OTOH, if we define atom types, and in particular define match type as (-> Space Atom ...), then it should match its first argument without reduction. But maybe you should also define the type of := as (-> Atom ...) in order to avoid reduction of its first argument. So, basically, any behavior can be accepted as valid. What should be the default behavior and how it is better to control this behavior via explicit types is what is being fleshed out right now.

[noskill]

Should such query work then:

(= (Green Sam) True)
(= (Green Tom) False)
!(println! (match &self (= (Green $who) True) ($who is really green)))

?

[Necr0x0Der]

This code works

(: = (-> Atom Atom Any))
(= (Green Sam) True)
(= (Green Tom) False)
(= (x) (match &self (= (Green $who) True) ($who is really green)))
!(println! (x))

There are two questions. One is what to do with = and its type. It is not a normal grounded symbol, because its semantics is defined by the interpreter - not by execute method. But maybe we should have it formally as a grounded symbol with a corresponding type. Or we should just insert its type definition by default in Atomspace. But I'm not sure if introducing the type of = by default won't break the unit tests. It worths some exploration. The second question is why calling match within println! directly doesn't output the result, while wrapping it into a function does... Maybe, it's also the question about match type. I have not yet dig into the novel version of the interpreter. Maybe, @vsbogd has some ideas?

[Necr0x0Der]

One more concern. Why initially I did think that such queries as (match &self (= (Green $who) True) ($who is really green)) should work, so we can always revert =, when we want, but maybe we should keep = for purely functional evaluation, and when we want reversible declarative definitions, we should use another symbol (in OpenCog classic, there is an imperative BindLink and declarative PLN links like Inheritance, Equal or others). It would be really convenient to be able to deal with = declaratively, but if it will appear that there are some nasty problems with this, we can resort to using Eq (or anything else) with inference rules for it defined in MeTTa for the cases, when we do expect backward chaining to be used. I'm not sure if this would be just a fallback strategy, or a preferable less confusing solution.

[Necr0x0Der]

I mean,

(:= (Green Sam) True)
(:= (Green Tom) False)
(= (x) (match &self (:= (Green $who) True) ($who is really green)))
!(println! (x))

works out-of-the-box without specifying a type for :=. Thus, behavior of = inevitably differs from a pure symbol. Of course, it is always up to the programmer whether to define own equality symbol with custom behavior, or to overuse = possibly facing some issues. But "good practices" should come from us. Maybe, introducing types carefully will resolve issues with using =, but something special about this symbol will always remain.

[noskill]

@Necr0x0Der There type issue in such query !(println! (match &self (= (Green $who) True) ($who is really green))) i mean without wrapping the query in (x)

========= MeTTa version 0.0 =========

[2022-06-03T12:39:19Z DEBUG hyperon::metta::interpreter] interpret_as_type_plan: input: (println! (match &self (= (Green $who) True) ($who is really green))), type: Undefined
[2022-06-03T12:39:19Z TRACE hyperon::metta::types] get_reducted_types: atom: println!
[2022-06-03T12:39:19Z TRACE hyperon::metta::types] get_reducted_types: return atom println! types [(-> ? IO)]
[2022-06-03T12:39:19Z DEBUG hyperon::metta::interpreter] current plan:
    return [(-> ? IO)] then form alternative plans for expression (println! (match &self (= (Green $who) True) ($who is really green))) using types
[2022-06-03T12:39:19Z DEBUG hyperon::metta::interpreter] current plan:
    apply "form alternative plans for expression (println! (match &self (= (Green $who) True) ($who is really green))) using types" to "[(-> ? IO)]"
[2022-06-03T12:39:19Z DEBUG hyperon::metta::interpreter] interpret_expression_as_type_op: input: (println! (match &self (= (Green $who) True) ($who is really green))), operation type: (-> ? IO), expected return type: Undefined
[2022-06-03T12:39:19Z DEBUG hyperon::metta::interpreter] interpret_as_type_plan: input: (match &self (= (Green $who) True) ($who is really green)), type: Specific(?)
[2022-06-03T12:39:19Z TRACE hyperon::metta::types] get_reducted_types: atom: match
[2022-06-03T12:39:19Z TRACE hyperon::metta::types] get_reducted_types: return atom match types [(-> Space Any Atom Atom)]
[2022-06-03T12:39:19Z DEBUG hyperon::metta::interpreter] current plan:
    return [(println! (match &self (= (Green $who) True) ($who is really green)))]
    return [(-> Space Any Atom Atom)] then form alternative plans for expression (match &self (= (Green $who) True) ($who is really green)) using types then insert right element as child 1 of left element then interpret each alternative
[2022-06-03T12:39:19Z DEBUG hyperon::metta::interpreter] current plan:
    return [(-> Space Any Atom Atom)] then form alternative plans for expression (match &self (= (Green $who) True) ($who is really green)) using types then return tuple ([(println! (match &self (= (Green $who) True) ($who is really green)))], ?) then insert right element as child 1 of left element then interpret each alternative
[2022-06-03T12:39:19Z DEBUG hyperon::metta::interpreter] current plan:
    apply "form alternative plans for expression (match &self (= (Green $who) True) ($who is really green)) using types" to "[(-> Space Any Atom Atom)]" then return tuple ([(println! (match &self (= (Green $who) True) ($who is really green)))], ?) then insert right element as child 1 of left element then interpret each alternative
[2022-06-03T12:39:19Z DEBUG hyperon::metta::interpreter] interpret_expression_as_type_op: input: (match &self (= (Green $who) True) ($who is really green)), operation type: (-> Space Any Atom Atom), expected return type: Specific(?)
[2022-06-03T12:39:19Z DEBUG hyperon::metta::interpreter] current plan:
    error "Operation returns wrong type: Atom, expected: Specific(?)" then return tuple ([(println! (match &self (= (Green $who) True) ($who is really green)))], ?) then insert right element as child 1 of left element then interpret each alternative

[vsbogd]

One option to change the behaviour is to have both alternatives in interpreter plan:

• matching after reduction: (match &self (:= False True) (Tom is really green)) returns empty result
• matching without reduction: (match &self (:= (Green $who) True) ($who is really green)) returns (Sam is really green) Merging of the results will return [(Sam is really green)].

Should such query work then:

(= (Green Sam) True)
(= (Green Tom) False)
!(println! (match &self (= (Green $who) True) ($who is really green)))

It will not work out of the box because = has special meaning as Alexey said. It is not equality check, it adds the equality which is used by interpreter.

The second question is why calling match within println! directly doesn't output the result, while wrapping it into a function does...

If println! type is changed to (-> Atom IO) it works. At the moment interpreter matches returned type of the function with expected type of the next one. It is added to cut incorrect interpretation paths and make interpretation faster. But at the moment we have a number of types like ? which doesn't type check by internal type checker and it leads to such confusion. We should cleanup such examples using standard type system for MeTTa. One particular thing which is not finished yet is consistent notation for the Undefined type.

[Necr0x0Der]

Hmm... with (-> Atom IO) type, println! just prints the given expression without reducing it (which makes sense for Atom). (println! (match &self (:= (Green $who) True) ($who is really green))) works only when both match and println! have Any as the return type, which is strange, because I'd expect that the argument type of println and the return type of match should coincide (not two return types)... In any case, since we have support for types of grounded symbols, we can start cleaning up the mess with the types of concrete grounded symbols and continue with formalizing the semantics of the interpreter w.r.t. symbols (meta)types.

[vsbogd]

Yes, sorry, with (-> Atom IO) it works but relatively useless. It should work properly with (-> Any IO) but it doesn't work at the moment because Any is not matched against Atom returned from match. It is what I mean when say that we need to define consistent type system here.

[Necr0x0Der]

Hmm.... match should be typed as (-> Space Any $t $t), but with $t being also Atom for the first occurrence (to be not reduced before calling match) and being non-deterministic for the return type. In some cases we may want to get a non-reduced Atom, but of type Int (e.g. arithmetic expression over ints). I don't want to overcomplicate it, but it seems that we may want to define both type and meta-type simultaneously. Maybe, we should think about this... Another note/question: I wonder if we can or should be able to define quote and unquote as identity functions with different type signatures:

(: quote (-> Any Atom))
(: unquote (-> Atom Any))

In both cases, we may want to give more precise types, e.g. (: quote (-> $t (Atom $t)) or something like that...

[vsbogd]

@Necr0x0Der , looks like this old issue is relevant to what we are discussing in #136 : type of pattern argument in match should be Atom

[Necr0x0Der]

Conclusion. Our choice is to consider match input pattern as Atom and do not reduce it. This behavior should be emphasized (in docs, tests, tutorials, etc.), so no one would expect that any subexpression of the pattern would be reduced before match is executed.