Inconvenient to implement `eq` that returns `False` about hyperon-experimental HOT 5 OPEN

-| looks ok. It could be convenient in certain cases. OTOH, if we have multiple type traits (e.g. determinism, totality, etc.), then it might be less convenient. However, we can always make -| just a syntactic sugar...

from hyperon-experimental.

Term equality in pure MeTTa

It's awesome that term equality can be implemented in pure MeTTa, but how does it work? Why the following reduction path

(eq a a) -> (eq-wrap (pure-eq a a)) -> False

using the fourth then third equation, is inhibited?

Type annotation to indicate determinism

I like the idea of enforcing determinism in the type. I was wondering, as an alternative to Det, maybe to use a different application type constructor. For instance to indicate that foo is non-deterministic one could write

(: foo (-| $a $a Bool))

That is -> would still indicate deterministism, symbolizing that every input points to a single value, while -| would be used to indicate non-deterministism, symbolizing that some input may point to many values. Then it brings some concerns such as what to do when combining -> and -| like in

(: foo (-| $a (-> $a Bool))

etc. So not saying it is better than Det, but just a suggestion that crossed my mind. Maybe existing non-deterministic functional programming languages such as https://curry.pages.ps.informatik.uni-kiel.de/curry-lang.org/ could be a source of inspiration. I know nothing of such language so I cannot tell.

from hyperon-experimental.

Why the following reduction path (eq a a) -> (eq-wrap (pure-eq a a)) -> False using the fourth then third equation, is inhibited?

@ngeiswei the reason is that (pure-eq a a) is reduced to True before trying to reduce (eq-wrap (pure-eq a a)). From non-deterministic execution perspective this is not quite correct because interpreter should execute both paths. But this behavior is saved from the very first version and it allows doing tricks like above before this issue is resolved correctly.

from hyperon-experimental.

Using -| to designate non-deterministic paths sounds like an interesting idea. I don't even see any contradiction in constructions like (: foo (-| $a (-> $a Bool)). It can be interpreted as foo is a function which non-deterministically returns deterministic function (-> $a Bool).

It seems that type annotations are also required and using them to designate determinism or non-determinism can be even more simple from the code complexity perspective.

from hyperon-experimental.

From non-deterministic execution perspective this is not quite correct because interpreter should execute both paths.

Well, yes, this is an interesting point. I wonder whether this should be considered a bug or a feature :)
We can describe this as an intended behavior if we wish, but if some examples appear, in which it will be highly desirable to have "full non-determinism", then we can reconsider this. In any case, we shouldn't rely too much on this "feature" now I guess (although I wonder how many unit tests implicitly exploit it).

from hyperon-experimental.