Open divarvel opened 1 year ago
it also makes sense in the context of unification between facts: if we're matching between facts, and the term we are matching on has different types on both sides, they do not match, but it does not blow up the entire execution
Currently, the haskell and rust implementations (amongst others) produce an error on the following expression:
1 == true
.While this makes sense to refuse this expression in a typed language (the equivalent expression would not type check in rust or haskell), this behaviour is a bit more surprising in an untyped langage where such an expression would usually evaluate to false instead of blowing up.
The specification does not explicitly cover this case, and i think it should.
My preference would go to have heterogeneous equality comparisons to not blow up and evaluate to false for two reasons:
Term
sum type, which defines==
by first comparing the constructors, and then values if the constructors are the same (this is why 2. holds).