I was reading some articles on type theory when this passage on invariants caught my attention:
“Where a class S is intended to be a behavioural subtype of a class T, it must obey the invariant strengthening rule: S may have a stronger invariant than T, but never weaker; and the behavioural conformance rule: any replacement methods Ri in S must be behavioural subtypes of the corresponding methods Mi in T that they replace.”
This is really the OOP principle of “require no more, promise no less,” also known as the Liskov Substitution Principle. I guess I never made the connection between LSP and type theory, though it seems obvious in retrospect. (Likely this is because I studied OOP and type theory during separate times.)
Basically, this is saying that objects that don’t follow LSP are not proper subtypes. The C++ type system seems so fragile from this angle (something we knew already) – it’d be nice if there was a way to enforce formal pre- and post-conditions.