Open chtenb opened 1 year ago
Nice catch! What's missing in the text (but not the code) is https://github.com/isovector/algebra-driven-design/blob/eeab5a07cf0ef8f816c9f88aeb6ca5cabc12bd18/code/Scavenge/InputFilter.hs#L54-L56 --- an instance of Observe
for InputFilter
s. The important bit here is that we're looking at observations of InputFilter
with respect to match
, so the actual constructors need not be clever, since the homomorphism into booleans is "obvious." Admittedly a bad omission though!
Thanks for the reply! I see, so if I understand correctly, all of the equalities that equate two InputFilter
s should be interpreted as though they are put through matches
, like
matches never = matches (notF always)
Exactly right! Sorry for the confusion :)
That leaves one more question: if our QuickSpec properties are always just concerned with observational equality (which makes sense to me), why bother with pattern matching on e.g. FlipH
in Section 5.1 to make the equalities hold?
(...) We can force the laws to hold by fiat, simply by performing some pattern matching in the definition of flipH.
flipH (FlipH t) = t flipH t = FlipH t
Of course algebraic equality implies observational equality, so that's fine in principle. But it seems unnecessary, and I can't find any motivation for it in the book. It seems to me that the properties would also hold if we were to leave the pattern matching out. Is that correct?
I'm working through the book, and there seems to be something lacking in Section 6.1.
At the end of the section, the equations found by QuickSpec are listed, such as
However, these equations (as well as some others) don't seem to be true, because
Never
is not the same algebraic value asNot Always
.Contrast with Section 5.1, where this issue is specifically addressed:
and then proceeds to modify the constructors to be "smart", such that the laws indeed hold algebraically.
Is this part simply missing from Section 6.1?