Missing smart constructors in Section 6.1?

[chtenb]

I'm working through the book, and there seems to be something lacking in Section 6.1.

The implementations of our constructors are extremely straightforward, making no attempt whatsoever to simplify the expressions:

always :: InputFilter i
always = Always

never :: InputFilter i
never = Never
...

At the end of the section, the equations found by QuickSpec are listed, such as

never = notF always
always = notF never

However, these equations (as well as some others) don't seem to be true, because Never is not the same algebraic value as Not Always.

Contrast with Section 5.1, where this issue is specifically addressed:

But this one-to-one mapping is not the whole story; it doesn't necessarily satisfy the laws that it is supposed to. For example, "flipH/flipH" statis that flipH . flipH = id, but this is decidedly not true given the definition of flipH. We can force the laws to hold by fiat, simply by performing some pattern matching in the definition of flipH.

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?

[isovector]

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 InputFilters. 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!

[chtenb]

Thanks for the reply! I see, so if I understand correctly, all of the equalities that equate two InputFilters should be interpreted as though they are put through matches, like

matches never = matches (notF always)

[isovector]

Exactly right! Sorry for the confusion :)

[chtenb]

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?