Investigate compositionality of expressions

[ccreeten]

As an example, I had an expression composed of core expressions, in this case gtEqNum(value, predicate). As the name implies, it should check if a value is greater than or equal to the predicate. This expression was implemented as or(gtNum(value, predicate), eqNum(value, predicate)) and it was created in the time when Metal still operated on single values as opposed to lists of values.

Now, with the new list semantics, this perhaps quite natural looking expression behaves a bit unexpected in a way. For example, if we take value: [1, 1] and predicate: [0, 1], the expression will result in a false value. The reason for this is that first, both lists are compared with the greater than expression which results in a false value, as 1 is not greather than 1. Second, both are compared on equality, also evaluating to false, because not all values are equal, i.e. with this expression are evaluating ([1, 1] > [0, 1]) || ([1, 1] == [0, 1]). The overall result of the expression is a false value.

Of course here it boils down to how it is written and there are ways around it (although currently not straightforward, save for just implementing a new class). I'd like to know what we could do about this.

One question I have is, is there a reason expressions do not evaluate to lists? Because what essentialy happens is these lists of values are zipped with a binary expression, and reduced with an and operation. I can not think of really interesting use cases, but I just wanted to throw it out here.

P.S.: feel free to improve the title 😄

[ccreeten]

I was curious so I hacked something together to see the effect of expressions returning lists of booleans. With this, I could actually write the expression as stated above. You can take a look at the branch expression-list-semantics in my fork 😄

[jvdb]

I may end up implementing LtEqNum and GtEqNum, but I'll take another look first!

[ccreeten]

Definitely a valid solution yes 😄

I have thought of an other case I think, concerning the (material) implication. I currently have it implemented as or(not(p),q). Take p = [0, 1] > [0, 0] and q = [0, 1] > [1, 1] for example: currently, first p will be evaluated (and reduced), resulting in a false value because 0 is not greater than 0. In the case of implication, the ultimate result will then be true no matter what.

With list semantics, p will evaluate to a list of two booleans, namely [F, T], and q will evaluate to [F, F]. Pairwise implication will result in a list of [T, F] which reduces to false (at least, when reducing with and).

This is a different result to what currently would be retrieved, if I am not mistaken somewhere. If not, the question I then do have is, are there perhaps more cases like these to be found?