Bug regarding superpose remaining unevaluated on empty tuples

[patham9]

Clearly there is no way for the following collapse to have any item:

!(== () (collapse (let* (($L ()) 
                         ($x (superpose $L)))
                        $x)))

Yet: Output: [False] Expected: [True]

MeTTa leaves the let expression unevaluated in this case, which leaves the collapse with a "pseudo-item", an expression with variables, which leads to the comparison to return false even though there cannot be any variable assignment that actually satisfies the let expression.

[Necr0x0Der]

The issue is that let is a grounded function. If we write (let $x (superpose ()) Test), it will just return NoValidAlternatives error instead of returning an empty result. let* is tricker. It doesn't get reduced similar to how (+ 5 my-custom-symbol) also is reduced. OTOH, !(let $x something (superpose ())) successfully returns an empty result. So, this can be considered as a bug in let and let* implementation. But one can argue that trying to assign an empty value to a variable in let is bug in the code that uses let. So, it depends. It can be fixed if needed, but I'm not sure what behavior will Minimal MeTTa have in this case, so I'd propose to fix it now if it is really a blocker. Otherwise, I'd propose to revisit this issue after migration.

[patham9]

Makes sense, no worries it is not a blocker for me.

"But one can argue that trying to assign an empty value to a variable in let is bug in the code that uses let"

Here I agree, except that in many cases it will not be (superpose ()) but (superpose $T) instead in a function, whereby $T is the input to the function which could receive an empty tuple in some cases.

[vsbogd]

Regarding minimal MeTTa, we have Empty symbol there to represent an empty result. Using it we could potentially properly fix superpose to return Empty from (superpose Empty) call. Thus the example above will turn into:

!(collapse (let $L Empty (let $x (superpose $L) $x)))

And collapse will return () in this case. One can "simulate" this on a current version of minimal MeTTa using additional parenthesis:

!(collapse (let $L (Empty) (let $x (superpose $L) $x)))

[vsbogd]

Thus if (superpose $T) is called with $T == Empty it will work. We should also fix collapse to return Empty instead of () to make it complete and allow collapse/superpose chains on Empty results.

[patham9]

I didn't yet get why "Empty" needs to be an explicit value. Either there is a value, which can be an empty tuple () or 42 as a special case, or there is no value, in which case backtracking should occur. What is it for?

[Necr0x0Der]

@patham9 , empty tuple () is not an empty value, it is a unit value. In imperative programming languages like C, when a function returns void, it actually means that the function returns an element from one-element set (from a category-theoretic perspective). It doesn't return nothing, it returns a trivial result. In MeTTa, when a function "returns" a really empty set of results, it means that the function terminates (that is, the function is not defined on this particular imports, that is, it is partial). However, in MeTTa, we may want to perform a meta-analysis, i.e. to be able to capture if a function appeared to be not defined on a certain input. That's why it is preferable to have Empty as an explicit value.

[Necr0x0Der]

I'd add that in dependently-typed languages, Void exists and means an empty set. The function with Void as its return type cannot exist in terms of constructive mathematics. Thus, if one provides a function for Prop -> Void , it is considered as a proof that Prop is false (that is, it is also an empty set , or a non-inhabited type). However, we still want to construct expressions that "return" "nothing" from Void for a declarative non-constructive analysis. Thus, we introduce void as an "element" of Void. Infinity doesn't "exist" (it is a non-constructive concept), but it is a useful abstraction. The same goes for void (or Empty in our case).

[patham9]

@Necr0x0Der Thank you for the detailed explanation, this makes perfect sense. (as I think I also commented in the meeting we had a while ago) Please feel free to close the issue.

[Necr0x0Der]

Maybe, we can close it, but I'd still like to clarify if we are ok with !(let $x (empty) OK) returning NoValidAlternatives or !(let* (($x (empty))) OK) remaining unreduced, or it would make more sense for let to return Empty, when a variable in it is attempted to be assigned to Empty? For example, !(let (A $x) (A B) OK) returns OK, while !(let ($x $x) (A B) OK) returns Empty (since unification fails). It is a little bit different from !(let $x (empty) OK), but semantics of both cases looks close - in the latter case we also cannot unify $x with nothing. I'd revisit this issue after migration to Minimal MeTTa, because it may have other results.

[Necr0x0Der]

If Minimal MeTTa will have another result, which satisfies us, I'd add this to unit tests to declare this behavior as intended.