The following

!(== 'A' "A")
!(get-type 'A')
!(get-type "A")
!("A")

outputs

[False]
[%Undefined%]
[String]
[('A')]

Indicating that even though "A" is displayed as 'A', the latter is neither a String nor a Char.

There are several fixes for that, the first one being to displaying "A" as "A". In addition I would suggest to introduce a Char primary type that would be parsed with single quotes like traditional functional programming languages such as Haskell, Idris and Racket.

If you agree to that I don't mind taking care of it.

MeTTa code heavily uses matching of atoms. Let's say we have two atoms: (A $x $x) and (A B $y). Result of the matching is a set of variable bindings or variable values (for both sides) which makes the given expressions equal. For the example above it is { $x = $y = B }. There is a special data structure to represent variable bindings: hyperon::atom::matcher::Bindings. The implementation of the Bindings was recently changed to represent both variable-to-value mappings and variable-to-variable equalities. But to restrict the volume of the change the API was almost untouched. In fact the API should also be changed. Current API doesn't take into account a fact that Bindings can be divided on few instances when a variable is being assigned a value or new variable equality is added.

For example lets look at the process of the matching of the atoms ( { (A B) (A C) } (A $x) ) and ( $s $s ) (I used the curly brackets to designate the atomspace with two pairs of atoms inside). At the first step the atomspace { (A B) (A C) } is assigned as a value of the variable $s: { $s = { (A B) (A C) } }. At the second step matcher assigns the (A $x) value to the $s. $s already has a value so { (A B) (A C) } is matched with (A $x) in order to find if they are compatible. Matching an atom with an atomspace means executing a query on an atomspace. For our example the query is (A $x). This query brings two results { $x = B } and { $x = C }. After merging the returned results to the previous one ({ $s = { (A B) (A C) } }) we have two different results which both are result of the matching of the original atoms: { s = { (A B) (A C) }, $x = B } and { s = { (A B) (A C) }, $x = C }.

The logic of the second step is implemented by the Bindings::add_var_binding function:

Bindings is an important part of the atom matcher implementation. And first part of the issue is fix the logic to handle the cases when Bindings are divided after adding a value of a variable or a variable equality. This change affects two functions in the public API of the Bindings: add_var_bindings() and merge(). Bindings::merge:

To restrict the volume of the change I would suggest temporary introduce the second version of the each public function affected. First version will keep old behavior and second one will introduce the correct behavior. Old version of the function should clearly assert on the condition when Bindings is expected to be divided but it is impossible to represent it in API. New version of the functions should be used in the matcher module to implement the matching algorithm properly and fix the unit tests introduced in #256. Old version of the functions should be used outside of matcher module to reduce the size of the change.

After the first part of the change is done we could revisit the external usages of Bindings API and fix them by using the new API instead of the old one.

The following metta program

(P Q)
(= (foo) P)
!(match &self ((foo) $Q) $Q)

outputs

[]

instead of

[Q]

as it should.

When replacing the match query by

!(match &self (P $Q) $Q)

it outputs

[Q]

as expected, indicating that the problem comes from the combination of reduction and matching.

For the program

(implies (Frog $x) (Green $x))
(implies (Frog $x) (Eats-flies $x))
(Frog Sam)
(Robot Sophia)

the result of the query

!(match &self
  (, (Frog $x)
     (implies (Frog $x) $y))
  $y)

is correct ([(Green Sam), (Eats-flies Sam)]).
However, if the query expressions are swapped

!(match &self
  (, (implies (Frog $x) $y)
     (Frog $x))
  $y)

then the output is [(Green $x-23), (Eats-flies $x-24)].

Also, the query

!(match &self
    (, (implies ($P $x) (Green $x))
        (implies ($P $x) (Eats-flies $x)))
    ($x is definitely $P))

returns [($x-73 is definitely Frog)], which is not incorrect, because $x remains unbound, but could the final result of match restore original variables? There are tricky situations, e.g.

(equals $x $x)
!(match &self
    (equals $y $z)
    ($y $z))

should not return ($y $z). Ideally, it should return ($y $y). Now, it returns ($x-96 $x-96), which is ok, but not always convenient. Possibly, this is connected with the main issue, but if not, we can leave it as is for now.

(= (append Nil $x1 $x1) True) 
 
(= (append (Cons $X1 $Y) $Z (Cons $X1 $W)) 
  (append $Y $Z $W) 
)

Working prints True

!(println! (append (Cons a2 Nil) (Cons b1 Nil) $W2222)) 

not working

!(println! (append (Cons a2 Nil) (Cons b1 Nil) $W))

In

:: is used to define the type of term. However in (as well as in the rest of the tests)

: is used.

1. Was : meant to be used in d1_custom_types.metta instead of :: (i.e. it's a typo)?
2. Or, :: or : can be used interchangeably because MeTTa doesn't ultimately care.

If the answer to 1. is true then I suppose this file should be fixed, to minimize confusion. And if the answer to 2. is true then a comment in d2_auto_types.metta explaining that would be good. I can take care of that but I need your feedback first.

Regardless of what is true, I suppose : would still remain the most popular convention and should be preferred for future use, correct me otherwise.

The following unit test fails:

    #[test]
    fn metta_execute_non_expression() {
        let program = "!3";

        let metta = Metta::new(Shared::new(GroundingSpace::new()), Shared::new(Tokenizer::new()));
        metta.set_setting("type-check".into(), "auto".into());
        let result = metta.run(&mut SExprParser::new(program));
        assert_eq!(result, Ok(vec![vec![expr!({Number::Integer(3)})]]));
    }

But it passes when 3rd line is replaced by:

        let program = "! 3";

It is a confusing behavior, see #297 (comment)
The root cause is explained here #297 (comment)

Working with the Dependent types, I unintentionally assigned two types for a given term and MeTTa didn't catch it as a type error, instead I got multiple results. Consider the following code, p has assigned of two different types,

!(pragma! type-check auto)
(: = (-> $t $t Type))
(: implies (-> $p $r Type))
(: testDTL (-> $p $r (implies $p $r)))
(: PR_prf (-> (implies P R)))
(: p P)
(: p X)
(: r R)
(: q Q)
(= (PR_prf) (testDTL p r))
!(PR_prf)

The code executes fine and I got two results [(testDTL p r), (testDTL p r)].

But, if we exchange the order of the line for (: p P) and (: p X),

....
(: p X)
(: p P)
....

then we got a type error at (= (PR_prf) (testDTL p r)) and that's expected because the left and right side of the equality don't have the same type. That means, even if p has assigned the correct type during the second type definition, it has not been updated (I think it shouldn't be) but why did I get two results in the first example? I think it is a bug.

Any of the following

!(get-type Bool)
!(get-type String)
!(get-type Number)
!(get-type (-> String Bool))
!(get-type ->)
!(get-type :)
!(get-type Atom)
!(get-type Type)

returns

[%Undefined%]

In comparison, in idris the type (obtained via :t in the REPL) of Bool, String, (-> String Bool) and Type would be Type, while that of -> or : would be undefined.

The following code

;; Define TruthValue type
(: TruthValue Type)
(: PrCnt (-> Float Float TruthValue))

;; Define a formula
(= (formula True False) (PrCnt 0.0 1.0))

;; Test the formula
!(formula True False)

outputs

[(formula True False)]

meaning (formula True False) is not properly reduced. However removing the type definition yields the desired result:

;; Define a formula
(= (formula True False) (PrCnt 0.0 1.0))

;; Test the formula
!(formula True False)

outputs

[(PrCnt 0.0 1.0)]

This is a tracking issue for some work that ought to be done.

#284 (comment)

Also, in the process, we should add an abstract iterator method for atoms within a space.

#284 (comment)

And we should update the interpreter bindings while we're at it.

#284 (comment)

from hyperon import *

def test():
        program = '''
            (X Y)
            (Y Z)
            (Y W)
            (Z W)
            (!println (match &self (, ($x $y) ($y $z) ($y $w) ($z $w)) (add-atom &self ($y $x))))
        '''
        runner = MeTTa()
        result = runner.run(program)

        print(runner.space().get_atoms())

test()

stacktrace:

log.txt

Building the latest revision 9c8aa55 fails at the cmake .. command.

The complete list of commands to compile is given below

cd ./lib
cargo build
cargo test
cargo doc
cd ..

cargo install --force cbindgen
python -m pip install -e ./python[dev]

cd build
cmake -DCMAKE_C_COMPILER=gcc ..      # <- FAILURE
make
make check
cd ..

And the full error message can be found attached.
cmake-error.txt

this code crashes metta interpreter

from hyperon import *

def test():
        program = '''
(1 2)
(2 3)
(2 4)
(3 4)
(= (add $a) 
   (add-atom &self
                                    ($y $x)
   True)

!(println! (match &self (, ($x $y)
                           ($y $z)
                           ($y $w)
                           ($z $w))

                           (nop (process (add-atom &self
                                    ($y $x)))
                              (process (remove-atom &self
                                  ($x $y))))))
        '''
        runner = MeTTa()
        result = runner.run(program)

        print(runner.space().get_atoms())

test()

stacktrace:
log.txt

All lines are commented out but the interpreter still prints some result

;(:= (length Nil) 0)
;(:= (length (Cons $a $m))
;    (+ 1 (length $m))
;)

; !(println! (match &self (:= (length Nil $W) True) (+ 1 $W) )                )

expected result: interpreter doesn't print result of match query

The following

(= x 1)
!(println! x)

prints

x

Thus does not beta-reduce x. Wrapping parentheses around x yields the desired result.

(= (x) 1)
!(println! (x))

prints

1

I guess the question is, do we want to make parentheses optional?

Overview

Some metta file imports lead to extraneous non-determinism.

How to reproduce

Unpack the following archive

folder.tar.gz

which contains a folder called folder with A.metta, B.metta, C.metta, D.metta and E.metta under it.

A.metta contains the definition of a function foo, while B.metta to E.metta contains various ways to import A.metta and call foo.

B.metta and C.metta are just here to show that import! works as expected. Then D.metta fails, seemingly because of a convoluted import path of A.metta. E.metta also fails, possibly for a different reason.

What should normally be expected

In D.metta and E.metta, !(foo 41) should output only one result, [42].

What is observed instead

D.metta and E.metta outputs the result multiple times [42, 42, 42, 42, 42, 42, 42, 42], indicating redundancy in the non-deterministic interpretation.

(:= (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

There are different cases, when it is desirable to indicate the type or meta-type of a symbol (especially, variable) in a concrete expression.

1. Some examples come from dependent type usage, e.g. Idris definition Refl : (x : a) -> Equal x x supposes that we have a variable of type a, and the output type is defined by this variable. Refl 42 is of type Equal 42 42. In MeTTa, we specify only types. For (: Refl (-> a (Equal a a))) , (Refl 42) will be of type (Equal Int Int). In type definitions, we are lacking the possibility to use the argument value passed to the constructor. There is a possible workaround, which partly works, if we define: (: (Refl $x) (=== $x $x)). !(get-type (Refl 42)) returns [(%Undefined% Number), (=== 42 42)]. The problem is also that the type of Refl itself is %Undefined%. Whether we should allow (and interpret in a special way) in-place definitions like (: $x $a) or should support definitions like (: (Refl $x) (=== $x $x)) more cleanly, is the question to be discussed.

2. In equalities, we are lacking the possibility to specify the type of the argument (or bind it to a variable). For example, one may want to return the type of the argument, e.g. (= (type (: $x $t)) $t). It should be noted that we may need to specify a type (e.g., (: $x $t) instead of just $x), which is normally missing, while in type definitions we may need to specify the argument (e.g., (: $x $a) instead of just $a), which is normally missing. The example of using the type of the argument can be worked around with get-type grounded function: (= (type $x) (get-type $x)).

2b) We may want to use types of arguments as additional restrictions / conditions. For example, if we have a generic fmap type definition
(: fmap (-> (-> $a $b) ($F $a) ($F $b)))
it's tempting to define
(= (fmap $f $C0) $C0)
to handle (: Nothing (Maybe $t)) or (: Nil (List $t)). Unfortunately, the pattern (fmap $f $C0) will be matched against any expression to be bound to $C0. We may want to restrict $C0 meta-type to be Symbol. Something like

(= (fmap $f $C0)
   (if (== (get-meta-type $C0) Symbol)
       $C0
       (superpose ())))

may work, but looks cumbersome. It would be much more convenient to be able to write (= (fmap $f (: $C0 Symbol)) $C0).
The same is true for the type definition of fmap. We may want to indicate that $F should be of Functor type (the problem, however, is that if we write (: $F Functor) in type definition, it might mean that $F is the argument value).

3. We may want to have type restrictions in pattern matching in general (to make it more efficient). For example, we may want to retrieve all true relations, (match &self (= ($R $x $y) True) (related $x $y), but only about humans, e.g. (: $x Human), (: $y Human). We may imagine a composite query

(match &self (, (: $x Human)
                (: $y Human)
                (= ($R $x $y) True))
    (related $x $y))

but if the pattern matcher tries to satisfy conditions independently and then intersects them, then it will be very inefficient. Also, the query (: $x Human) may not work for derived types (only for explicit statements in the knowledge base?). Type restrictions might be more efficient to have inside one query (match &self (= ($R (: $x Human) (: $y Human)) True) ...). If match supports this form of restrictions, it might help to automatically solve (2) as well. More generally, such patterns as (match &self (= ($R (: $x $t) (: $y $t)) True) ...) are also desirable.

If we allow in-place type definitions, typing expressions will be treated specially. E.g., (match &self (: $x Human) $x) will search not for records like (: Plato Human), but for individual symbols (stored in Atomspace) with the corresponding type restriction. Then, the question will arise putting (: Plato Human) into Atomspace should result in putting Plato there together with its type, or one needs to put both (: Plato Human) and Plato into Atomspace in order for (match &self (: $x Human) $x) to retrieve the result. Thus, we either need to syntactically distinguish between in-place type restrictions and general type definitions (e.g., (match &self (:: $x Human) $x)) or to treat : uniformly on the level of implementation (e.g., it attaches a type to a symbol instance, and each symbol instance has its own set of types).
In the former case, it will be possible to distinguish between the desire to declare the type (which can be non-deterministic) and to check the type, e.g. with (: (Refl $x) (=== $x $x)), one can write (: (Refl MyTrue) (=== MyTrue MyFalse)), if MyTrue and MyFalse are both of MyBool type, because this is a (part of non-deterministic) type declaration. However, if one writes (:: (Refl MyTrue) (=== MyTrue MyFalse)) it will not work, because (Refl MyTrue) has (=== MyTrue MyTrue)) type.
In turn, ascribing individual types to symbol instances might be convenient in its own ways.
Thus, syntactic and semantic aspects should be analyzed together to support in-place type declarations and/or restrictions.

A simple program synthesis experiment reveals the need for a form of Just-In-Time type checking.

The following metta code tries all possible ways to serially compose two unary functions f and g:

;; Define composition operator
(: . (-> (-> $b $c) (-> $a $b) (-> $a $c)))
(= ((. $g $f) $x) ($g ($f $x)))

;; Define functions to compose
(: f (-> Number String))
(= (f $x) (if (== $x 42) "42" "Not-42"))
(: g (-> String Bool))
(= (g $x) (== $x "42"))

;; Test composition via superpose
!(. (superpose (f g)) (superpose (f g)))

However, although only one composition is valid (. g f), it outputs

[(. f f), (. f g), (. g f), (. g g)]

Moving superpose outside of the composition operators makes it clear that the it is due to the lack of dynamicity of the type checker. For instance, the following

!(superpose ((. f f) (. f g) (. g f) (. g g)))

outputs

[(Error f BadType), (Error g BadType), (. g f), (Error g BadType)]

which is what we want.

Replacing superpose with non-determinism via over-definition leads to the same result. For instance:

(= (fns) f)
(= (fns) g)
!(. (fns) (fns))

outputs

[(. f f), (. f g), (. g f), (. g g)]

Finally, although that might be a separate issue, one may notice that

!((. g f) 42)

outputs

[(g '42')]

instead of

True

After closing #273, one more thing to do is to handle parsing error results in C API, Python API and MeTTa console interpreter.
At the moment they are also lead to the panic because of unwrapping Result in C API layer:

Currently observers are registered with spaces using the trait method Space::register_observer. This means each space implementation is responsible for keeping track of all observers, notifying each individually, and making sure they are correctly unregistered if they've been dropped (RefCount reached 0), etc.

We propose centralizing this logic to reduce code duplication and cut down on the possibility of errors / inconsistent treatment of observers.

#284 (comment)

Also, implement #284 (comment) at the same time.

Additionally, we probably want to support Clone for the new common space object. However, that object should not clone the observers. #284 (comment)

Finally, on the C side, we should implement space_observer_get_payload(). After the Rust changes are made, the API could be refactored so that that space_observer_new doesn't exist, and space_register_observer() takes the arguments currently given to space_observer_new. Then space_register_observer() would return a space_observer_t which could implement the space_observer_get_payload() function. #284 (comment) for reference.

The code

(: if (-> Bool Atom Atom Atom))
(= (if True $then $else) $then)
(= (if False $then $else) $else)
(= (plus $atom)
  (if (== $atom ())
      0
      (+ (car-atom $atom) (plus (cdr-atom $atom)))))
!(plus (1 2 3 4))

doesn't work now. But it works if we change the type of CarAtomOp from Atom::expr([ARROW_SYMBOL, ATOM_TYPE_EXPRESSION, ATOM_TYPE_ATOM]) to Atom::expr([ARROW_SYMBOL, ATOM_TYPE_EXPRESSION, ATOM_TYPE_UNDEFINED]) (in stdlib.rs).
It is not a bug per se, but it is not convenient. It can also be worked around:

(: if (-> Bool Atom Atom Atom))
(= (if True $then $else) $then)
(= (if False $then $else) $else)
(: as-number (-> Atom Number))
(= (as-number $x) $x)
(= (plus $atom)
  (if (== $atom ())
      0
      (+ (as-number (car-atom $atom)) (plus (cdr-atom $atom)))))
!(plus (1 2 3 4))

So, it is really a minor issue. However, as-number looks hacky/unsafe, e.g. !(+ (as-number "S") 2) raises an exception. We may want to be able to specify the type of car-atom in such a way that the type of (car (1 2 3)) would be Number. Also, we may want to disallow (: as-number (-> Atom Number)) (or we may want the type-checker to be able to validate correctness of (as-number 1) or (as-number (car-atom (1 2))), and to detect incorrectness of (as-number "S") at least at runtime).

The following code doesn't work

(: ≞ (-> $event $tv Type))
(: TruthValue Type)
(: Bl (-> Bool TruthValue))
(≞ (P 42) (Bl True))

(= (idi_formula $r1 $r2)
   (Bl True))    

(= (idi_match $kb)
   (let* (($prem1 (≞ ($p $a) $patv))
          ($prem2 (≞ ($q $a) $qatv))) 
     (match $kb
       ;; Premises
       (, $prem1 $prem2)  
       ;; Conclusion
       (≞ (→ $p $q) (idi_formula $prem1 $prem2)))))

!(idi_match &self)

If I were to change (: ≞ (-> $event $tv Type)) by (: ≞ (-> Atom Atom Type)), I got the following result
[(≞ (→ P P) (idi_formula (≞ (P 42) (Bl True)) (≞ (P 42) (Bl True))))]
But, the idi_formula function doesn't get reduced.

assertEqualToResult expects Atom arguments.
The code

(: T Type)
(: eq (-> $t $t Type))
(= (eq $x $x) T)

!(assertEqualToResult
   (eq Z (S Z))
  ((eq Z (S Z Z))))

correctly raises exception. If we add type definitions for S and Z, the exception is not risen:

(: T Type)
(: eq (-> $t $t Type))
(= (eq $x $x) T)

(: Z Nat)
(: S (-> Nat Nat))

!(assertEqualToResult
   (eq Z (S Z))
  ((eq Z (S Z Z))))

The problem is that (S Z Z) is badly typed, and assertEqualToResult doesn't get evaluated. If we change the assert expression to

!(assertEqualToResult
   (eq Z (S Z))
  ((eq (S Z) (S Z))))

the exception will be risen correctly. Interestingly,

!(assertEqualToResult
  (eq Z (S Z))
  (eq Z (S Z Z)))

raises exception (in the typed case as well.
The following

!(assertEqualToResult
  (eq Z (S Z Z))
  ((eq Z (S Z))))

also raises exception, while

!(assertEqualToResult
  ((eq Z (S Z Z)))
  ((eq Z (S Z))))

doesn't. So, wrapping the expression into additional parentheses influences whether assertEqualToResult gets evaluated or not.

This unconventional use of :

; Define homogenous type equality
(: === (-> $a $a Type))
(: Refl (-> $x (=== $x $x)))

;; Term42 is a witness of 42
(: Term42 42)

;; Define foo, converts some equality proof to True
(: foo (-> (=== 42 42) Bool))
(= (foo $prf) True)

;; Test foo
!(foo (Refl Term42))

crashes the MeTTa interpreter with the error message

Thread '<unnamed>' panicked at 'GroundedAtom is not expected at type's place: $x-8, 42', /home/nilg/Work/TrueAGI/hyperon-experimental/lib/src/metta/types.rs:186:60
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
fatal runtime error: Rust panics must be rethrown
Aborted

The following code:

(= (inc $x) (+ $x 1))
(= (dec $x) (- $x 1))
!($x 2)

returns [1, 3]. This is fun, and doesn't contradict to evaluation via equality queries. However, I'd prefer to

1. be able to specify expressions like ($x $y) without automatic reduction;
2. force to explicitly match functional symbols if needed, e.g.

!(match &self (= ($func 2) $r) $r)
!(match &self (= ($func $x) $r) ($func 2))

both work.
Thus, I propose to consider variables as non-operational if this doesn't require considerable refactoring and breaks no tests.

Problem

Importing a metta file that itself imports another metta file raises the exception

[(Error (import! &self B.metta) Exception caught:
AttributeError: 'list' object has no attribute 'catom')]

How to reproduce

1. Create empty A.metta file
2. Create B.metta file with content !(import! &self "A.metta")
3. Create C.metta file with content !(import! &self "B.metta")
4. Running metta.py C.metta raises the exception, while neither A.metta nor B.metta does.

There are different cases, when we want some symbols (especially, functional) to be overloaded, that is, to have different behavior for different types. Two prominent examples are comparisons and fmap. Let us consider

(: Maybe (-> $a Type))
(: Nothing (Maybe $a))
(: Just (-> $a (Maybe $a)))

We may want to have fmap : ($a -> $b) -> $F $a -> $F $b for any functor $F.

(= (fmap $f (Just $x)) (Just ($f $x)))
(= (fmap $f Nothing) Nothing)

We can have another definition for List or another container. Thus, more equalities to the same fmap will be added. MeTTa supports this, and one may hope that wrong equalities will not be applied due to pattern-matching against particular constructors (e.g. (Cons 1 Nil) will not be confused with (Just 1) or Nothing), but one may want to define (= (fmap $f $any) Nothing), but only for (: $any (Maybe ())) or anything else weird (e.g. to define a particular fmap for particular $a). Thus, we cannot be sure that a desirable definition of fmap will be selected due to constructors. In any case, there is a natural desire to group equalities for fmap by implementations per type. This can be done explicitly, e.g.

(: fmap-maybe (-> (-> $a $b) (Maybe $a) (Maybe $b))
(= (fmap-maybe $f (Just $x)) (Just ($f $x)))
(= (fmap-maybe $f Nothing) Nothing)
(= (fmap $f $xs) (fmap-maybe $f $xs))

Thus, if we pass (fmap f (Cons 1 Nil)) it will not go to fmap-maybe, because types will not match. Another option would be not to introduce fmap-maybe, but to have means to indicate that fmap in certain equalities is restricted to certain types. One may propose different syntactic representation for this, but the fundamental question here is whether we want symbol to have one global type or each instance of a symbol may have its own (specialized) type, which is a different issue to discuss, but which may influence our approach to symbol overloading (well, types of symbol instances is also about symbol overloading, but cases can be different).
If we consider comparisons, they will have similar issues. For example,

(= (< (Just $x) (Just $y)) (< $x $y))
(= (< (Just $x) Nothing) False)
(= (< Nothing (Just $x)) True)

could work if < wouldn't have a predefined type. However, the problems are similar (and even more prominent, because we may want to redefine the output type, e.g. to have a ternary logic for Maybe- (= (< (Just $x) Nothing) Unknown), as well as to have grounded comparison operations for grounded types). Here, we may want to have a type for < as (-> $a $a $t) with certain restrictions for $a and $t (e.g. $a should be Ord, which can be done by introducing conditions on types or utilizing subtyping or via higher-order types, or some ad hoc constructions). This also may or may not be related to interfaces, typeclasses, OOP-like polymorphism, etc. Automatic type conversion is also of possible relevance.
Apparently, a principled way of overloading operations with type-based dispatching or an idiomatic way to deal with such cases is of interest.

In this code match returns empty result, at the same time evaluating the expression directly works and prints True []

(= (append Nil $x1 $x1) True)
  
(= (append (Cons $C1 $Y) $Z (Cons $C1 $W))
  (append $Y $Z $W)
)

!(println! (match &self (= (append (Cons a2 Nil) (Cons b1 Nil) $W) True)  $W ))
!(println! (append (Cons a2 Nil) (Cons b1 Nil) $W ))

(lst1 (Cons a1 (Cons b2 b3)))
(lst2 (Cons a2 (Cons b3 b4)))
(Concat $x1 $x2 $x3)

!(println! (match &self
                       (, (lst1 $l1)
                          (lst2 $l2)
                          (Concat $l1 a2 a3))
                       ($l2) )
                        )

Logs:

[2022-04-25T09:51:31Z DEBUG hyperon::metta::interpreter] execute_op: (match &self (, (lst1 $l1) (lst2 $l2) (Concat $l1 a2 a3)) ($l2))
[2022-04-25T09:51:31Z DEBUG hyperon::space::grounding] single_query: pattern: (lst1 $l1)
[2022-04-25T09:51:31Z DEBUG hyperon::space::grounding] single_query: push result: (lst1 (Cons a1 (Cons b2 b3))), bindings: {$l1: (Cons a1 (Cons b2 b3))}
[2022-04-25T09:51:31Z DEBUG hyperon::space::grounding] single_query: pattern: (lst2 $l2)
[2022-04-25T09:51:31Z DEBUG hyperon::space::grounding] single_query: push result: (lst2 (Cons a2 (Cons b3 b4))), bindings: {$l2: (Cons a2 (Cons b3 b4))}
[2022-04-25T09:51:31Z DEBUG hyperon::space::grounding] single_query: pattern: (Concat $l1 a2 a3)
[2022-04-25T09:51:31Z DEBUG hyperon::space::grounding] single_query: push result: (Concat $x1 $x2 $x3), bindings: {$l1: $x1}
[2022-04-25T09:51:31Z DEBUG hyperon::metta::interpreter] current plan:
    interpret alternatives for (match &self (, (lst1 $l1) (lst2 $l2) (Concat $l1 a2 a3)) ($l2)):
      > return []
     (or return [((match &self (, (lst1 $l1) (lst2 $l2) (Concat $l1 a2 a3)) ($l2)), {})]) then reduct next arg in (println! >(match &self (, (lst1 $l1) (lst2 $l2) (Concat $l1 a2 a3)) ($l2))<) (or return [((println! (match &self (, (lst1 $l1) (lst2 $l2) (Concat $l1 a2 a3)) ($l2))), {})])

As the result this query gives empty result;
expected result is (Cons a2 (Cons b3 b4))

For the following code:

; Curried plus
(: plus (-> Number (-> Number Number)))
(= ((plus $x) $y) (+ $x $y))
; Define inc as partial evaluation of plus
(: inc (-> (-> Number Number)))
(= (inc) (plus 1))

we will get the following results of evaluation of some expressions:

!((plus 1) 2)    ; --> 3 [correct]
!(inc)    ; --> (plus 1) [correct]
!((inc) 2)    ; --> ((inc) 2) [incorrect, remains unreduced]
!(get-type (inc))    ; --> (-> Number Number) [correct]
!(get-type ((inc) 2))    ; --> Number [correct]
!(let $f (inc) ($f 2))    ; --> 3 [correct]

It looks strange that ((inc) 2) is not reduced.

Without type definition, inc works:

(: plus (-> Number (-> Number Number)))
(= ((plus $x) $y) (+ $x $y))
(= (inc) (plus 1))
!((inc) 2)     ; --> 3 [correct]

So, there is an issue with type-checking.

A direct way to implement equality comparison function in MeTTa is (= (eq $x $x) True). However, for non-equal arguments it will just remain unreduced, while returning False would be desirable. If we add (= (eq $x $y) False), then it will return both True and False for (eq x x), because cases are not mutually exclusive. An inconvenient way to implement eq would be:

(= (pure-eq $x $x) True)
(= (eq-wrap True) True)
(= (eq-wrap (pure-eq $x $y)) False)
(= (eq $x $y) (eq-wrap (pure-eq $x $y)))

!(eq a a)
!(eq a b)

which works. Thus, this is not a strong limitation of the current design/implementation. However, there are other related use cases, which would look nicer with the possibility either to declare that the cases are mutually exclusive or to provide one "otherwise" case.
There are various ways to implement this (both conceptually and syntactically).

• Use some type annotation to indicate that the function is deterministic (and thus only one case should be taken), e.g. (: eq (-> $t $t (: Bool Det)) or (Det Bool). Two cases (eq $x $x) and (eq $x $y) (somehow prioritized) should then work.
• Introduce %else% keyword, e.g. (= (eq %else%) False). There is also some need for the version of match that has an output pattern for cases, when no matches are found, e.g. (match &self something Matched Not-Matched). Basically, if there is %else% case for a function, this case can be used as a "non-matched" output pattern for this version of match.
• one can introduce case grounded function with mutually exclusive cases and else case (precisely like in Scheme):

(= (eq $x $y)
    (case (Pair $x $y)
          ((Pair $x $x) True)
          (else False)))

While implementation of eq via case is not too elegant, case may be generally useful, and distinguishing it from function cases (which order in Atomspace is not guaranteed) to represent mutually exclusive cases also makes sense.

Background

Hyperon has the core written in Rust and it has C binding and Python binding, which allows developers to use the library in C/C++ and Python projects.

The current pipeline to build the python binding is:

Rust core → (cbindgen) → C API → (pybind11) → Python package

This pipeline uses cbindgen to generate C binding from Rust code, which then is used to create Python binding using pybind11.

Issue

Building and maintaining the Python package turned out to be harder than it is supposed to be.

Alternative

Rust core → (PyO3) → Python package

Pros

• PyO3 provides a more direct and efficient way of generating Python bindings from Rust code, without the need for an intermediate C binding step.
• It also supports running with Python code from within a Rust binary.

Cons

• One downside to consider is that completely rewriting the Python bindings will be required.
• It may require some additional setup and refactoring of existing code

Conclusion

Like anything else, there are pros and cons to consider. On one hand, the use of PyO3 can potentially lead to a more streamlined and efficient process for creating and maintaining Python bindings. It also opens up the possibility of running Python code within a Rust binary. On the other hand, it is important to consider the downside of having to completely rewrite the Python bindings and potentially refactor existing code.

So, the decision to switch from pybind11 to PyO3 should be carefully considered based on the specific needs and goals of this project.

As a side note, due to the popularity of Python, particularly in AI, creating a Python package backed by a Rust core is a great combination. It can provide both execution performance and a large user base in AI. It appears to me less critical to maintain a C API, although it could potentially enable Hyperon to run on an embedded device.

(see also comments in https://github.com/trueagi-io/hyperon-experimental/blob/main/python/tests/scripts/d3_deptypes.metta)
Hedra's example

;; Define TV
(: TruthValue Type)
(: PrCnt (-> Number Number TruthValue))
(: ≞ (-> $ev $tv Type))

;; Formula returns the default TV for now
(= (ded_formula ($pqtv $qrtv)) (PrCnt 1 0))

;; Rule
(: ImplicationDeduction
    (-> (≞ (→ $p $q) $pqtv)
        (≞ (→ $q $r) $qrtv)
        (≞ (→ $p $r) (ded_formula ($pqtv $qrtv)))))

;; Test
!(pragma! type-check auto)
(: = (-> $t $t Type))

;; KB
(: Predicate Type)
(: → (-> Predicate Predicate Type))
(: P Predicate)
(: R Predicate)
(: Q Predicate)
(: pq (≞ (→ P Q) (PrCnt 1 0.5)))
(: qr (≞ (→ Q R) (PrCnt 1 0.5)))

;; Assign TV to the prf
(: pr_prf (-> (≞ (→ P R) (PrCnt 1 0))))

!(assertEqual (get-type (pr_prf)) (get-type (ImplicationDeduction pq qr)))

;; But, this also gives me a type error
(= (pr_prf) (ImplicationDeduction pq qr))

The problem is that (pr_prf) and (ImplicationDeduction pq qr) seem to be of the same type, but type-checking of their equality fails. The reason is that (ImplicationDeduction pq qr) is really of (≞ (→ P R) (ded_formula ((PrCnt 1 0.5) (PrCnt 1 0.5)))) type, and it is reduced to (≞ (→ P R) (PrCnt 1 0)) not by type-checking, but by evaluation (based on equality for ded_formula). Type-checking doesn't apply equalities for symbols in type definitions. It doesn't evaluate expressions. On the one hand, this may seem as a limitation of the type system. On the other hand, if the type system is unrestricted (calculus of constructions), there is no real border between types and terms, and types can be considered as ordinary custom symbols introduced on top of untyped lambda calculus. We also don't want to perform full evaluation of expressions in type-restricted pattern matching queries. Thus, the built-in type-checking should really not perform MeTTa code execution. If one wish to go beyond this restriction, a custom type system implementation (either in MeTTa or in a reference language) should be done. Thus, this should not be considered a bug. Nevertheless, we may want to do something about this (e.g., introduce a special symbol that forces the type checker to evaluate some expression, raise a warning if a type definition contains a functional call, for which equality is defined, or something else).

I am using Python 3.10 and trying to run hyperon test. During make check I got the following error

Traceback (most recent call last):
  File "/home/hedra/SNET/hyperon-experimental/venv/bin/nosetests", line 8, in <module>
    sys.exit(run_exit())
  File "/home/hedra/SNET/hyperon-experimental/venv/lib/python3.10/site-packages/nose/core.py", line 118, in __init__
    unittest.TestProgram.__init__(
  File "/usr/lib/python3.10/unittest/main.py", line 100, in __init__
    self.parseArgs(argv)
  File "/home/hedra/SNET/hyperon-experimental/venv/lib/python3.10/site-packages/nose/core.py", line 179, in parseArgs
    self.createTests()
  File "/home/hedra/SNET/hyperon-experimental/venv/lib/python3.10/site-packages/nose/core.py", line 193, in createTests
    self.test = self.testLoader.loadTestsFromNames(self.testNames)
  File "/home/hedra/SNET/hyperon-experimental/venv/lib/python3.10/site-packages/nose/loader.py", line 481, in loadTestsFromNames
    return unittest.TestLoader.loadTestsFromNames(self, names, module)
  File "/usr/lib/python3.10/unittest/loader.py", line 220, in loadTestsFromNames
    suites = [self.loadTestsFromName(name, module) for name in names]
  File "/usr/lib/python3.10/unittest/loader.py", line 220, in <listcomp>
    suites = [self.loadTestsFromName(name, module) for name in names]
  File "/home/hedra/SNET/hyperon-experimental/venv/lib/python3.10/site-packages/nose/loader.py", line 431, in loadTestsFromName
    return self.loadTestsFromModule(
  File "/home/hedra/SNET/hyperon-experimental/venv/lib/python3.10/site-packages/nose/loader.py", line 359, in loadTestsFromModule
    return self.suiteClass(ContextList(tests, context=module))
  File "/home/hedra/SNET/hyperon-experimental/venv/lib/python3.10/site-packages/nose/suite.py", line 461, in __call__
    return self.makeSuite(tests, context, **kw)
  File "/home/hedra/SNET/hyperon-experimental/venv/lib/python3.10/site-packages/nose/suite.py", line 511, in makeSuite
    suite = self.suiteClass(
  File "/home/hedra/SNET/hyperon-experimental/venv/lib/python3.10/site-packages/nose/suite.py", line 189, in __init__
    super(ContextSuite, self).__init__(tests)
  File "/home/hedra/SNET/hyperon-experimental/venv/lib/python3.10/site-packages/nose/suite.py", line 57, in __init__
    super(LazySuite, self).__init__()
  File "/usr/lib/python3.10/unittest/suite.py", line 22, in __init__
    self._tests = []
  File "/home/hedra/SNET/hyperon-experimental/venv/lib/python3.10/site-packages/nose/suite.py", line 109, in _set_tests
    if isinstance(tests, collections.Callable) and not is_suite:
AttributeError: module 'collections' has no attribute 'Callable'

Its due to the incompatibility issue of Nose and as a work around, I replaced collections.Callable by collections.abc.Callable and it works for now, but I don't think that's the right solution.

Do I have to use previous Python versions to work with Hyperon?

MeTTa code heavily uses matching of atoms. Let's say we have two atoms: (A $x $x) and (A B $y). Result of the matching is a set of variable bindings or variable values (for both sides) which makes the given expressions equal. For the example above it is { $x = $y = B }.

There is a special data structure to represent variable bindings: hyperon::atom::matcher::Bindings. Matching is a fundamental part of the atoms processing so Bindings structure is a part of C API. For example it is used in c/src/space.rs module to return results of a query to the caller.

Most of the structures from the Hyperon core library are represented in C API by thin wrappers. For example atom_t is a wrapper of the Atom. All public functions of Atom are represented by atom_... functions in c/src/atom.rs. It is not a case for Bindings. It is represented by totally another kind of structure bindings_t. Which is a vector of pairs variable name/atom. This was done to simplify C API and provide more natural C interface. But at the moment Bindings API is going to be changed. It is the reason why it is better to replace bindings_t by simple wrapper of Bindings as it is done for most of other structures.

The task is to replace current bindings_t implementation by thin wrapper of the hyperon::atom::matcher::Bindings. It requires replacing the bindings_t implementation in the Hyperon library C API and adding bindings_... functions for each public Bindings function. It is also required to add C++ proxy calls into python/hyperonpy.cpp file. And using this calls to represent Bindings by class in Python API. Finally all C and Python API unit tests need to be fixed to support new API.

I'm trying to implement a function in MeTTa to insert an element in a sorted list but fails (on revision 067d627).

Let's first check that conditional works

;; Implement conditional
(= (if True $x $y) $x)
(= (if False $x $y) $y)

;; Test conditional
!(println! (if True 42 0))
!(println! (if False 42 0))

It outputs

42
0

as it should.

Then let's test if insert works (using the previously implemented conditional)

;; Declare List data structure
(: List (-> $a Type))
(: Nil (List $a))
(: Cons (-> $a (List $a) (List $a)))

;; Implement insert element in a presumably sorted list
(= (insert $x Nil) (Cons $x Nil))
(= (insert $x (Cons $head $tail)) (if (< $x $head)
                                      (Cons $x (Cons $head (Cons $tail)))
                                      (Cons $head (insert $x $tail))))

;; Test insert
!(println! (insert 1 Nil))
!(println! (insert 1 (insert 2 Nil)))

It outputs

(insert 1 Nil)
(insert 1 (insert 2 Nil))

which is not correct.

I should mention that this used to work on revision 280d231.

PyPi version of the Nosetests test runner is not compatible with Python 3. Moreover Nosetests is not maintained anymore (see nose-devs/nose#1099 and #106). This issues is to migrae Python part of the Hyperon project to the new test runner. The possible options are:

• unittest;
• nose2;
• pytest;
• anything else

The following MeTTa code

;; Declaration of List data structure
(: List (-> $a Type))
(: Nil (List $a))
(: Cons (-> $a (List $a) (List $a)))

!(println! ("========= Test equality ========="))
!(println! (== True True))
!(println! (== True False))
!(println! (== Nil Nil))
!(println! (== 1 1))
!(println! (== (Cons 1 Nil) (Cons 1 Nil)))

prints

("========= Test equality =========")
True
False
True
[]
[]
[]
[]
[]
[]

If the type declarations of List, Nil and Cons are removed, then it prints

("========= Test equality =========")
True
False
(== Nil Nil)
True
(== (Cons 1 Nil) (Cons 1 Nil))
[]
[]
[]
[]
[]
[]

What does that mean?

Generally speaking should I overload == for non primary data types?

Last and least, what do the []s mean?

I'm trying to build MeTTa's C API, but fail at the cmake .. command from https://github.com/trueagi-io/hyperon-experimental/blob/main/README.md#c-and-python-api with the following error

ERROR: libcheck/0.15.2: 'settings.compiler' value not defined
CMake Error at c/CMakeLists.txt:4 (include):
  include could not find load file:

    /home/nilg/Work/TrueAGI/hyperon-experimental/build/c/conanbuildinfo.cmake


CMake Error at c/CMakeLists.txt:5 (conan_basic_setup):
  Unknown CMake command "conan_basic_setup".

Not sure it is a feature or a bug, but I noticed that strings inside metta are printed differently if they contain whitespaces or not. For instance

!(println! ("alpha"))
!(println! ("alpha omega"))

outputs

(alpha)
("alpha omega")

Also, another issue, the following

!(println! "alpha")

prints nothing. Again, I don't know if it's a feature or a bug.

Main usecase is logging to one file from both python and rust code. Currently rust logs are separate from python logs.

Currently parsing an invalid expression like (Q 2 raises something like

thread '<unnamed>' panicked at 'Unexpected end of expression', /home/adamv/PycharmProjects/hyperon-experimental/lib/src/metta/text.rs:129:9
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
fatal runtime error: Rust panics must be rethrown

From @vsbogd (in code review)

BindingsSet::single in matcher means that two atoms are equal, and BindingsSet::empty means they cannot be matched. Thus I don't see the use-case for such semantics of _empty() yet. And if this semantics is not used then name can be confusing because one may think it returns true iff no Bindings instances are inside.

I don't feel like this conceptual difference is adequately communicated by the words "empty" and "single".

Maybe "unconstrained" and "fully_constrained"? Those are clumsy to write and probably not accurate. Any other ideas?

Context: I'm seeing this as a teeny tiny step towards laying the foundation to support infinite, explosive, lazily evaluated, or otherwise unbounded bindings. I still don't have a picture of what that needs to look like, but this seems like the beginnings of building up that conceptual framework.

To reproduce the problem place the following

!(import! &self bug.metta)
!(42)

in file bug.metta. Then run bug.metta via <HYPERON-EXPERIMENTAL>/python/tests/metta.py.

The observed result is a segmentation fault. What should be expected is an error or a warning that cyclic import should be forbidden. Or perhaps MeTTa could detect it and automatically disable the importing.

Building on the CSpace, allow Python code to define a new Space.

This can be considered as intended, but can also add some confusion.
If we don't use !(pragma! type-check auto), badly typed expressions can be added to Atomspace. We consider this as valid, because type definitions can be modified at runtime, and MeTTa agents may "want to reason" about wrong/counterfactual propositions, etc. If such expressions are added, we may want to be able to query them as well (otherwise they will be inaccessible, and adding them to Atomspace will make no sense). That is, the program:

(: p P)
(: r R)
(: Test (-> P R))
(Test r)
!(match &self (Test $x) $x)

will retrieve r for incorrectly typed (Test r) (although !(match &self (Test $x) (Test $x)) will not be reduced, because the resulting (Test r) will be badly typed. Thus, some type-checking is performed at runtime, which is necessary for non-deterministic types, e.g.

(: Test1 (-> Number Bool))
(= (Test1 $x) True)
(: Test2 (-> String Number))
(= (Test2 $x) 10)
(= (Test $x) (Test1 $x))
(= (Test $x) (Test2 $x))
!(Test "Hello")

will return only 10 (not True), because (Test1 "Hello") doesn't type-check.
However, this introduces some asymmetry between initial code, which can be added to Atomspace while being badly typed, and expressions constructed at runtime (which will be evaluated to an empty set if they are badly typed). What is confusing is that badly typed equalities can produce results, which are not badly typed by themselves, e.g.

(: = (-> $t $t Type))
(: Test (-> Number Bool))
(= (Test $x) 10)
!(Test 5)

will produce 10 although the expected result is of Bool type. Apparently, (= (Test $x) 10) is badly typed and shouldn't be added to Atomspace (and it will not be added with !(pragma! type-check auto)). But if it is nonetheless added, the equality query (match &self (= (Test 5) $x) $x) will be successful. As discussed above, such query (at least constructed explicitly) should be successful, but it is not obvious if the interpreter should check types of results of such queries constructed by itself. One may say - just don't add such expressions to Atomspace, and if you add them intentionally, then you can also explicitly check that types of the expression to be evaluated and the result of its evaluation are equal. Nevertheless, if automatic type checking is off by default, this causes confusions.

The following expression !(let $f $x (let $f f $x)) being executed should return [f] but it returns [$f#1] instead.

To calculate the result property we should apply the equality of variables stated on the outer let ({ $x = $f }) to the nested let expression. Thus the nested let becomes (let $x f $x) or (let $f f $f) and finally evaluated to f.

The root cause is that let is implemented as a grounded operation. Grounded operation doesn't return Bindings and thus can only return values of the variables in the atoms. It does it applying { $x = $f } to the (let $f f $x) but the result is (let $x f $f) because Bindings returns $x as a value for $f and $f as a value for $x. I omitted variable renaming here which leads to $f becomes $f#1. Finally (let $x f $f) is evaluated to $f because $f is absent in the pattern $x.

I would suggest fixing it through introducing a proper let implementation as a part of minimal interpreter implementation.

Related to #188 , but a cleaner problem. The code

(: inc (-> Number Number))
(= (inc $x) (+ $x 1))
!(inc 1)

works as expected, but

(: inc (-> Number Number))
(: inc (-> Number Number))
(= (inc $x) (+ $x 1))
!(inc 1)

produces 4 (!) identical results. With equality non-determinism, the number of results multiplies. The interpreter works correctly, if the argument type doesn't match the (non-deterministic) type signature, e.g.

(: inc (-> Number Number))
(: inc (-> String Number))
(= (inc $x) (+ $x 1))
!(inc 1)

produces only one result. We don't have a settled semantics for non-deterministic types that match one equality. For example,

(: inc (-> Number Number))
(: inc (-> Atom Number))
(= (inc $x) (+ $x 1))
!(inc 1)

produces 2 results. There can be tricky cases, when we do want to use same equality interpreting its arguments as being of different types, and one may claim that getting 2 results in the latter case is OK (to be discussed and decided, I'd say; maybe, it would still be preferable to use the equality once, but to keep track of different possible types of its argument). But why there are 4 results for the duplicated type definition case?