Merge pull request trueagi-io#675 from trueagi-io/eqtype

adding the type for = to stdlib

lib/src/metta/runner/stdlib.metta

@@ -1,3 +1,12 @@
+(@doc = 
+  (@desc "A symbol used to define reduction rules for expressions.")
+  (@params (
+    (@param "Pattern to be matched against expression to be reduced")
+    (@param "Result of reduction or transformation of the first pattern") )
+  (@return "Not reduced itself unless custom equalities over equalities are added") )
+)
+(: = (-> $t $t Atom))
+
 (@doc if
   (@desc "Replace itself by one of the arguments depending on condition.")
   (@params (

lib/src/metta/runner/stdlib.rs

@@ -2197,11 +2197,11 @@ mod tests {
 
     #[test]
     fn sealed_op_runner() {
-        let nested = run_program("!(sealed ($x) (sealed ($a $b) (=($a $x $c) ($b))))");
-        let simple_replace = run_program("!(sealed ($x $y) (=($y $z)))");
+        let nested = run_program("!(sealed ($x) (sealed ($a $b) (= ($a $x $c) ($b))))");
+        let simple_replace = run_program("!(sealed ($x $y) (= ($y) ($z)))");
 
         assert!(crate::atom::matcher::atoms_are_equivalent(&nested.unwrap()[0][0], &expr!("="(a b c) (z))));
-        assert!(crate::atom::matcher::atoms_are_equivalent(&simple_replace.unwrap()[0][0], &expr!("="(y z))));
+        assert!(crate::atom::matcher::atoms_are_equivalent(&simple_replace.unwrap()[0][0], &expr!("="(y) (z))));
     }
 
     #[test]

lib/src/metta/runner/stdlib_minimal.metta

@@ -1,3 +1,12 @@
+(@doc = 
+  (@desc "A symbol used to define reduction rules for expressions.")
+  (@params (
+    (@param "Pattern to be matched against expression to be reduced")
+    (@param "Result of reduction or transformation of the first pattern") )
+  (@return "Not reduced itself unless custom equalities over equalities are added") )
+)
+(: = (-> $t $t Atom))
+
 (@doc ErrorType (@desc "Type of the atom which contains error"))
 (: ErrorType Type)
 (: Error (-> Atom Atom ErrorType))
@@ -272,11 +281,11 @@
 (= (not True) False)
 (= (not False) True)
 
-(: let (-> Atom %Undefined% Atom Atom))
+(: let (-> Atom %Undefined% Atom %Undefined%))
 (= (let $pattern $atom $template)
   (unify $atom $pattern $template Empty))
 
-(: let* (-> Expression Atom Atom))
+(: let* (-> Expression Atom %Undefined%))
 (= (let* $pairs $template)
   (eval (if-decons-expr $pairs ($pattern $atom) $tail
     (let $pattern $atom (let* $tail $template))

python/tests/scripts/d4_type_prop.metta

@@ -51,19 +51,18 @@
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-; Equality can be typed. If some equality is well-typed,
-; it means that it can be true.
+; Equalities themselves are typed. If some equality is well-typed,
+; it means that it can be true. Equality is of Atom type.
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-(: = (-> $t $t Type))
 !(assertEqual
   (get-type (= SocratesIsMortal (HumansAreMortal SocratesIsHuman)))
-  Type)
+  Atom)
 ; This equality is well-typed, because both its arguments are of `Type`.
 ; It doesn't mean they are both inhabited (true propositions), and
 ; it doesn't mean that the equality itself is true (an inhabited type).
 !(assertEqual
   (get-type (= (Mortal Socrates) (Mortal Plato)))
-  Type)
+  Atom)
 ; Wrong proof
 !(assertEqualToResult
   (get-type (= SocratesIsMortal (HumansAreMortal PlatoIsHuman)))
@@ -90,7 +89,11 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ; Another (MeTTa) way is to have explicit reduction of types to True
 ; (equalities over equalities), although a more practical way would
-; be just to use a dedicated comparison operator
+; be just to use a dedicated comparison operator.
+; Notice that this code works, although T is declared as of Type type,
+; because the type of equality expressions is Atom, which can be
+; matched against any other type. Such permissiveness allows using
+; `=` in custom type systems.
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 (: T Type)
 (= (= $x $x) T)

python/tests/scripts/f1_moduleC.metta

@@ -5,5 +5,5 @@
 (: __g (-> Number))
 (= (__g) 100)
 
-(: g (-> Number Numer))
+(: g (-> Number Number))
 (= (g $x) (+ $x (__g)))