"In quantity equals not one of yours."
-- Shakespeare, Henry IV Part I
Act III, Scene I, Line 93
In The Little Prover we find the following Axioms of Equal:
(dethm equal-same (x)
(equal (equal x x) 't))
(dethm equal-swap (x y)
(equal (equal x y) (equal y x)))
(dethm equal-if (x y)
(if (equal x y
(equal x y)
't)))
I learn best by doing, so I showed myself these axioms in Clojure.
Looking at equal-same we see that if we have something which is the same then those values are equal. Nothing shocking, unless you are using reference equivalence which we are not.
Next we look at equal-swap which states that equivalence is commutative meaning x = y is the same as y = x. Again nothing shocking.
Last we look at equal-if which states that if something is equal once it will be equal again. Note that this assumes that values are immutable which they are (for the most part) in Clojure. This axiom is rather interesting when paired with lazy evaluation, as we see with the following:
(is (true?
(if (= :yep :yep)
(= :yep :yep)
(throw
(IllegalStateException. "How the hell did we get here?")))))
When the statement is evaluated we do not have the Exception thrown! This is a great benefit of the if special form in Clojure. We do see this awesomeness has limits:
(let [x (repeat 42)
y x]
(is (true?
(if (= x y)
(= x y)
false))))
but fails when the infinite sequence is not the same "reference"
(let [x (repeat 42)
y (repeat 42)]
(is (true?
(if (= x y)
(= x y)
false)))))
Despite the second example of comparing with an infinite sequence not finishing, the if special form is awesome and shows the power of the equal-if axiom paired with lazy evaluation.
These axioms are very powerful and I would argue are more useful than tests. If this interests you I would recommend reading The Little Prover or working your way through the flying tour of ACL2.
