如何看待带有子类型的多态性

Question

Liskov替代原则规定：

子类型中必须保留超类型的不变量。

我对这个原理和多态性的交叉点特别感兴趣。但在特定的子类型多态性中，事实上，参数多态性和Haskell类型类似乎就是这种情况。

所以，我知道函数是子类型，当它们的参数是逆变的，它们的返回类型是协变的。我们可以假设方法只是带有隐式“自我”参数的函数。然而，这似乎意味着如果子类重写父类的方法，它就不再是子类型，因为它的一个方法不再是子类型。

例如。获取以下伪代码：

class Parent:
    count : int
    increment : Parent -> ()
    {
        count += 1
    }

class Child inherits Parent:
    increment : Child -> ()
    {
        count += 2
    }

那么回到LSP：我们能不能说Parent.increment（）的属性应该适用于Child.increment（），即使这两个属性不遵守严格的子类型关系？

更一般地说，我的问题是：子类型化规则如何与多态函数的更具体参数相结合，以及将这两个概念结合起来思考的正确方式是什么？

Answer 1

术语“子类型化”在技术上是一个句法问题。所以在语法上，Child

正如维基百科所指出的，利斯科夫原则是关于行为亚型的。它需要语法子类型，但也取决于您对类的不变量和前置/后置条件的定义。因为你没有定义任何，所以谈论违规行为是荒谬的。

如果将增量的后置条件定义为新计数=旧计数1，则存在冲突。

如果将增量的后置条件定义为新计数

一般来说，将后置条件定义为“完全是父代的后置条件”，使得通过定义不可能包含多态性。在多态性有意义的地方，后条件的定义应该放宽。

请注意，类不变量是关于可能的值-对象的快照-并且由于您可以根据父级的增量定义子级的增量，因此它不能违反任何不变量。

Answer 2

引用维基百科关于Liskov替代原理的文章

更正式地说，Liskov替代原则（LSP）是子类型关系的一个特殊定义，称为（强）行为子类型[…]

行为子类型是一个比类型理论中定义的函数的典型子类型更强的概念，它只依赖于参数类型的反方差和返回类型的协方差。行为分型一般来说是微不足道的不可判定的[...]

子类型必须满足许多行为条件：

• 子类型中的前提条件不能加强

因此，LSP是一个更强的子类型定义，它依赖于类型理论之外的特性。

在您的示例中，这在您的不变量上上升和下降。

calling increment will increase count by **exactly 1**

显然，由于不变量被破坏，所以子对象不能用父对象来表示。这不能仅从语法推断。

LSP应该引导您分别定义父级和子级，让它们都继承自具有较弱post条件的Incrementable。