On Friday 08 August 2025 00:49:27 (+02:00), Morgan wrote:
> On 2025-08-08 10:01, Rob Landers wrote:
> > For example, if |A::foo(): int| promises to always return a non-zero
> > integer, and a subclass overrides |foo()| to only return zero, that
> > violates the contract—even though the type signatures match perfectly. This
> > is the sort of semantic guarantee that LSP is about, and it is discussed in
> > nearly every reputable textbook and conference talk on OO design. Languages
> > like PHP can’t enforce these contracts, but the / principle/ is what helps
> > prevent subtle design bugs and behavioural “surprises.”
> > Indeed. Those contracts only become enforceable in the type signature when
> > your type system is robust enough to be able to express them. If you could
> > declare |A::foo(): NonzeroInt| then the signature could prevent an
> > overriding subclass C from returning zero from that function (while still
> > allowing |C::foo(): PositiveInt|, say); the compiler can verify that the
> > type of the expression C::foo() is written to return is of type NonzeroInt
> > (or PositiveInt).
>
> In the absence of being able to declare such constraints in the type system,
> one has to fall back on other documentation about what behaviour is and isn't
> acceptable.
>
That is certainly always useful, especially when it was written down, as it
allows to read both, the fine-print, and between the lines. As you have just
quoted Rob's suggestion while replying to it, allow me the opportunity to
highlight a key sentence for me under the pretext of the earlier quote, and the
much appreciated association with documentation of yours to illustrate that:
> [...] the / principle/ [here, LSP,] is what helps prevent subtle design bugs
> and behavioural “surprises.”
Documentation, e.g. of pre- and postconditions, loop (in)variants, class
invariants, etc, we can already make use of those corner-stones of the LSP to
reason about sub-types, the LSP can inspire us of what or how we document. And
that's what I've learned these days from Rob: Without reasoning about the LSP.
I knew already for what I love Liskov for, but the LSP is so much a loaded
thing in discussions, I had to get a couple of things out of the way first to
only understand Robs reasoning. I came here by the error message, and was
looking for what I was missing with it.
"Oh the types in PHP must do that for us, otherwise my scripts are doomed."
No.
The compiler can only handle the type but not the sub-type, because of the
halting problem.
And while my programs can be doomed because of the halting problem (4. Every
program is a part of some other program and rarely fits.), I as human am still
able to reason about the correctness of my program.
Just my 2 cents
-- hakre
