trueagi-io / hyperon-experimental

MeTTa programming language implementation
https://metta-lang.dev
MIT License
141 stars 47 forks source link

Type checking doesn't work for tuples. #669

Open vsbogd opened 5 months ago

vsbogd commented 5 months ago

Describe the bug

Type checking doesn't work for tuples.

To Reproduce

Run the following MeTTa code:

(: (a b) (C D))

(: foo (-> (A B) %Undefined%))
(= (foo $x) succ)

!(foo (a b))

Expected behavior

Type error: (Error (a b) BadType)

Actual behavior

No type error: succ

vsbogd commented 5 months ago

Not that straightforward because in the following example:

(: a T)
(: foo (-> T T))
(= (foo $x) $x)
(= (bar $x) $x)
!(foo (bar a))

bar has no type and (bar a) interpreted as a tuple. As a consequence the type of (bar a) is (%Undefined% T) which is not unified with T required by foo. Thus relaxed type-checking allows using untyped functions in many examples.

For example recursive fact definition also fails with tuple type-checking enabled:

(= (fact $n) (if (== $n 0) 1 (* (fact (- $n 1)) $n)))
!(assertEqual (fact 5) 120)
vsbogd commented 5 months ago

We could check alternative interpretations: