Question regarding types and their understanding

[DaddyWesker]

I've met some issue (probably it is my misunderstanding of how metta works with typed functions though) when adding types to functions. Here is the code and it works fine. It counts leaves of tree as name states.

(= (null? $expr)
    (== $expr ()))

(= (list $expr)
   (if (null? $expr)
       Nil
       (if (== (get-type $expr) Number)
        $expr
        (Cons (list (car-atom $expr)) (list (cdr-atom $expr))))))

(= (count-leaves Nil)
    0)
(= (count-leaves $x)
        (if (== (get-type $x) Number)
            1
            (empty)))
(= (count-leaves (Cons $x $xs))
        (+ (count-leaves $x)
            (count-leaves $xs)))

!(assertEqual
    (count-leaves (list (1 2 3 4)))
    4)
!(assertEqual
    (count-leaves (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)))))
    4)

(= (x) (list ((1 2 3) 3 4)))

!(assertEqual
    (count-leaves (x))
    5)
!(assertEqual
    (count-leaves (Cons (Cons 1 (Cons 2 (Cons 3 Nil))) (Cons 3 (Cons 4 Nil))))
    5)

Problems starts when I'm trying to add types here. They are not actually needed but I was checking Anatoly's suggestion about influence of types on script's performance. Anyway, I've inserted those lines:
(: List (-> $a Type))
(: Nil (List $a))
(: Cons (-> $a (List $a) (List $a)))
(: count-leaves (-> Number Number))
(: count-leaves (-> (List Number) Number))

After this, strange behavior (at least in my understanding) happened.
Launching
!(count-leaves (list (1 2 3 4)))
gives [4,4], not just 4

and launching
!(count-leaves (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)))))
gives [4] which is correct. But i don't understand how is it possible since (list (1 2 3 4)) and (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)))) should be the same. What am i missing?

Almost same goes to the tree example:

(= (x) (list ((1 2 3) 3 4)))
!(count-leaves (x)) ; gives [5,5]
!(count-leaves (Cons (Cons 1 (Cons 2 (Cons 3 Nil))) (Cons 3 (Cons 4 Nil)))) ; [(Error (count-leaves (Cons (Cons 1 (Cons 2 (Cons 3 Nil))) (Cons 3 (Cons 4 Nil)))) NoValidAlternatives)]

Though, once again, (x) and (Cons (Cons 1 (Cons 2 (Cons 3 Nil))) (Cons 3 (Cons 4 Nil))) should be the same. Though it is not true. This one works:

!(assertEqual
    (list (1 2 3 4))
    (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)))))

But this one - not:

!(assertEqual
    (Cons (Cons 1 (Cons 2 (Cons 3 Nil))) (Cons 3 (Cons 4 Nil)))
    (x))

It gives:

Expected: [(Cons (Cons 1 (Cons 2 (Cons 3 Nil))) (Cons 3 (Cons 4 Nil)))]
Got: [(Error 3 BadType)]
Missed result: (Cons (Cons 1 (Cons 2 (Cons 3 Nil))) (Cons 3 (Cons 4 Nil))))]

In case of tree (x) it is probably related to types of List and Cons. So, questions are:

1. It is unclear why (x) is constructed without a problem, but if I'm pasting (Cons (Cons 1 (Cons 2 (Cons 3 Nil))) (Cons 3 (Cons 4 Nil))) as it is it produces an error.
2. Why when I'm introducing types for list, cons, count-leaves it breaks result for !(count-leaves (list (1 2 3 4))) but not for !(count-leaves (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)))))? Why behavior is different for same (as I understand) input?

My opinion is that it can be related to different evaluation sequence with and without types.

Thanks in advance.

[DaddyWesker]

@vsbogd

[vsbogd]

1. It is unclear why (x) is constructed without a problem, but if I'm pasting (Cons (Cons 1 (Cons 2 (Cons 3 Nil))) (Cons 3 (Cons 4 Nil))) as it is it produces an error.

Let's start from situation when only three types are added:

(: List (-> $a Type))
(: Nil (List $a))
(: Cons (-> $a (List $a) (List $a)))

I also replacing (Cons (Cons 1 (Cons 2 (Cons 3 Nil))) (Cons 3 (Cons 4 Nil)))) by (Cons (Cons 1 (Cons 2 (Cons 3 Nil))) (Cons 6 (Cons 4 Nil)))) to make example more demonstrative.
This situation causes type error on last assert when using old interpreter:

[()]
[()]
[()]
[(Error (assertEqual (count-leaves (Cons (Cons 1 (Cons 2 (Cons 3 Nil))) (Cons 6 (Cons 4 Nil)))) 5) 
Expected: [5]
Got: [(Error 6 BadType)]
Missed result: 5)]

The reason is that (Cons (Cons 1 (Cons 2 (Cons 3 Nil))) (Cons 6 (Cons 4 Nil))) expression contains two types of list mixed. Part of the expression (Cons 1 (Cons 2 (Cons 3 Nil))) constructs List Number, and outer Cons is called on (List Number) (List Number) which cannot be casted to the types of the first two arguments $a (List $a), thus this call ends with BadType error. This error happens when second argument tries to construct a list of type (List (List Number)) with arguments 6 (Cons 4 Nil) and fails because 6 is not a (List Number).

Why (list (1 2 3 4)) type checks? In original program list has %Undefined% type. It means that interpreter can cast its value to any type (type-check is not being made). Thus while (Cons (list (car-atom $expr)) (list (cdr-atom $expr))) inside list should return type error it is not returned because of list's type. It also doesn't work if we add a type for list function (: list (-> %Undefined% (List $t))). Because this type has a free variable which is not filled by the interpreter (because we don't have a type inference from a function body). Thus arguments of the Cons effectively have types List $a and List $b and interpreter can cast them one to another.

I should note here that minimal MeTTa behaviour differs. It returns empty result even for (count-leaves (x)):

[()]
[()]
[(Error (assertEqual (count-leaves (x)) 5) 
Expected: [5]
Got: []
Missed result: 5)]

and after adding type for the list even first expression fails (count-leaves (list (1 2 3 4))):

[(Error (assertEqual (count-leaves (list (1 2 3 4))) 4) 
Expected: [4]
Got: []
Missed result: 4)]

I will look at this difference later.

[vsbogd]

2. Why when I'm introducing types for list, cons, count-leaves it breaks result for !(count-leaves (list (1 2 3 4))) but not for !(count-leaves (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)))))? Why behavior is different for same (as I understand) input?

Adding two types for count-leaves means we are introducing non-deterministic results for a function:

(: count-leaves (-> Number Number))
(: count-leaves (-> (List Number) Number))

Now for each call of the count-leaves interpreter has at least two branches: with (-> Number Number) type and with (-> (List Number) Number) type. And it additionally will be multiplied on a number of matched (= (count-leaves ...) definitions.

Usually it is expected that interpreter will cut the branches which has type errors. But in case of your program it doesn't happen because list has %Undefined% type. Thus its result is casted to both Number and (List Number) types. (count-leaves (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))))) on the other hand uses Con which has a return type (List $t) where $t <- Number and thus the extra branch which accepts Number argument is cut.

Adding (: list (-> %Undefined% (List $t))) here fixes the situation for the first two examples because interpreter deduces value of $t <- Number from applying count-leaves to the results of list.