关于LSP（里氏替换原理）和子类型的问题
LSP 说
如果 q(x) 是关于类型 T 的对象 x 的可证明属性，则 q(y) 对于类型 S 的对象 y 应该为真，其中 S 是 T 的子类型。
我可以将其改写如下：
q(x) 对于 T => 中的任何 x 都成立。 q(y) 对于 T 的任何子类型的任何 y 都成立
现在另一个陈述怎么样？
q(x) 对于 T 的任何 x 都为真，并且 q(y) 对于 S 的任何 y 都为真 => S 是 T 的亚型
这有意义吗？我们可以将它用作subtype的定义吗？
LSP says that
if q(x) is a property provable about objects x of type T then q(y) should be true for objects y of type S where S is a subtype of T.
I can rephrase it as follows:
q(x) is true for any x of T => q(y) is true for any y of any subtype of T
Now what about another statement ?
q(x) is true for any x of T and q(y) is true for any y of S => S is a subtype of T
Does it make sense ? Can we use it as a definition of subtype ?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（3）
答案是否。该表达式的含义是可以定义 S 和 T 的共同超类型 R，然后 LSP（该名称如何成为主流的耻辱）将适用于 T->R 和 S->R。
在类型理论中，存在包含语义的类型，并且存在遵守语义的类型的实现（可能通过继承实现）。
实际上，指定类型语义（
q(x)部分）的唯一合理方法是通过实现，因此我们留下了 形式的无语义签名接口和类为了实现目的而继承，并实现它们喜欢的接口，但无法检查它们是否正确执行。研究人员尝试定义形式语言来指定类型，以便工具可以检查实现是否遵守类型定义，但工作量太大，以至于将形式语言编译为可执行代码一样好。我认为这是一个永远无法解决的第二十二条军规情况。
回到你原来的问题，在允许今天所谓的“鸭子打字”的语言中，答案是不可确定的，因为任何类型的对象都可以传递给任何函数，并且如果实现了正确的签名并且结果是对的。让我解释一下......
在像 Eiffel 这样的语言中，你可以在
List.append()操作后List.length()必须增加。这不是 Perl、JavaScript、Python 甚至 Java 等语言的工作方式。与更严格的类型定义相比，缺乏类型严格性允许更简洁的代码。The answer is No. What the expression means is that a common supertype R of S and T could be defined, and that then the LSP (shame on how that name became mainstream) would hold for T->R and S->R.
In typing theory, there are types, that include semantics, and there are implementations of the types that abide to the semantics, perhaps by inheriting implementations.
In practice, the only reasonable way to specify the semantics of a type (the
q(x)part) is through an implementation, so we are left with semantic-less signatures in the form of interfaces, and classes that inherit for implementation purposes, and implement the interfaces they like, with no way to check if they are doing it correctly.Researches have tried to define formal languages to specify types, so tools can check if an implementation abides to type definitions, but the effort is so large that it would do as good to compile the formal language into executable code. It's a Catch-22 situation that I think will never be solved.
Back to your original question, in languages that allow what today is called "Duck Typing", the answer is undecidable, because an object of any type can be passed to any function, and the typing is right if the correct signatures are implemented and the result is right. Let me explain...
In a language like Eiffel you could place a postcondition on
List.append()thatList.length()must increase after the operation. That is not the way languages like Perl, JavaScript, Python, or even Java work. That lack of type-strictness allows for much more succinct code than stricter type definitions would.这没有道理；使用
and的语句在 S 和 T 中是对称的。但我认为你想说的是以下内容
我更喜欢使用数学逻辑而不是非正式英语，但如果我的定义正确的话，这就是行为子类型，现在通常称为“鸭子类型”。这是一个非常好的子类型原则，并且再次引出了这样的想法：在任何需要
T类型值的上下文中，您可以提供一个S类型值，并且它是好的，因为类型S的值保证满足上下文期望的所有属性。It does not make sense; your statement using
andis symmetric in S and T.But I think you meant to say the following
I would prefer to use mathematical logic rather than informal English, but if I have got the definition right, this is behavioral subtyping, which these days is often called "duck typing." It's a perfectly good subtyping principle and again leads to the idea that in any context that expects a value of type
T, you may instead supply a value of typeS, and it's OK because the value of typeSis guaranteed to satisfy all properties that are expected by the context.我认为不，你不能用它作为定义。此外，如果 q(x) 对于 T 的任何 x 都为真，并且 q(y) 对于 S 的任何 y 都为真
它也可能意味着 T 是 S 的子类型。
要确定哪个是哪个的子类型（假设您知道它们之间存在继承关系），您还必须了解哪个更“通用”
或者哪个比另一个更“专业”。
I think no, you can't use it as a definition. Besides if q(x) is true for any x of T and q(y) is true for any y of S
it could also mean that T is a subtype of S.
To be sure of which is a subtype of which (assuming you know that there is an inheritance relationship between them) you also have to know something about which is more "generic"
or which is more "specialized" than the other.