Those abstractions are still leaky, e.g. it's entirely possible that an optimizing compiler could apply correct monoid laws and end up with a program that has vastly different space usage.
Without abstraction it would be difficult to write a proof that your implementation of the monoid laws stay within specified bounds.
It's not "leaky" if the specification doesn't say anything about the space bounds. That's a separate concern from "abstraction" itself.
Update The idea of a monoid is divested of any real-world implementation and that's what makes it useful (and consequently also hard to explain). The important thing is that there are laws to how the operations on monoids compose and relate to one another that must be maintained no matter how they're implemented in an actual computer.
