Closed Necr0x0Der closed 7 months ago
One last issue is that
(: is-space (-> Atom Bool))
(= (is-space $atom)
(let* (($type (get-type $atom)) ($space (get-type &self))) (== $type $space)))
doesn't type-check in minimal metta. It seeems that the type of overall let*
expression is reduced to Atom
, because the type of let*
is (-> Expression Atom Atom)
, while the type of (is-space $atom)
is reduced to Bool
, and defining equality between them fails. Indeed, the following code doesn't type-check in minimal metta
(: a Atom)
(: b Bool)
! (= a b)
It can be fixed by changing let*
signature to (-> Expression Atom %Undefined%)
. I'm ok with introducing this change, but it shows some difference with Rust MeTTa.
Hmmm. In fact, I see that
impl Grounded for LetVarOp {
fn type_(&self) -> Atom {
// The first argument is an Atom, because it has to be evaluated iteratively
Atom::expr([ARROW_SYMBOL, ATOM_TYPE_ATOM, ATOM_TYPE_ATOM, ATOM_TYPE_UNDEFINED])
}
That is the return type is really different in two versions. So, I change this in this PR. @vsbogd ?
That is the return type is really different in two versions. So, I change this in this PR. @vsbogd ?
I don't mind. I am not sure if it breaks something.
A few comments:
1) The type of
=
is defined as(: (-> $t $t Atom))
. There could be other options like usingEquality
orType
, both of which have their own merits. However, I preferred to keep the output type loose, so we can define something like (as in test scripts):If
=
would have, say,Equality
return type, then(= $x $x)
would ofEquality
reduced type, and(= (= $x $x) T)
would not type-check overall. Thus, we should be forced to reduce equalities (if we would like to reduce them) to something ofEquality
type as well. This could also be ok, but let's keep things more permissive for now.2) I fixed the unit test for
sealed
, since it contained badly-typed(= ($x $y))
expression. I hope it's ok.3) Adding the type for
=
resulted in such the behavior, when importing badly typed expressions produce type error even without automatic type checking (although only in the test environment; maybe, it enables type-checking by default). I didn't dig into detail, but I have had to fix another unit test with type. I'd count this behavior as a feature.