There are also the monoid "laws" (not checked in Haskell):

    empty `smash` x = x -- left identity
    x `smash` empty = x -- right identity
    (x `smash` y) `smash` z = x `smash` (y `smash` z) -- associativity

Your definition doesn't fit any of these. (Edit: you've rewritten to meet the first two; but it is not associative.)

mightybyte didn't state the associativity law in his original definition. As for the left and right identity laws, he did state them, and I did intend my instance to satisfy them (otherwise I wouldn't have special-cased 25, of course), but I messed up. I've fixed my post since.

Just for reference, the laws are stated in full in haskell's docs, https://hackage.haskell.org/package/base-4.10.0.0/docs/Data-....

I was deliberately “acting stupid” to criticize an insufficiently precise definition.

---

> That is usually a terrible idea.

Not at all. Think about the structure of a proof of negation. You make a “silly” assumption and “play along” until you reach a contradiction.

That is usually a terrible idea.

Proofs by contradiction do not require you to play dumb, you can just present them as they are.

I left out associativity because I was focusing on the ELI5 part.

They are not checked in Haskell, but they are definitely relied on by existing code.

For anyone who was wondering, catnaroek was being sarcastic.

I think combining 25 and x should yield x.

Oops, yes, my bad.