如何考虑子类型的多态性

里氏替换原则指出：

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

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

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

例如。采取以下伪代码：

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

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

那么回到 LSP：我们可以说Parent.increment()应该坚持Child.increment()即使这两者不遵守严格的子类型关系？

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

引用维基百科的文章里氏替换原则 http://en.wikipedia.org/wiki/Liskov_substitution_principle

更正式地说，里氏替换原则（LSP）是一个特定的 子类型关系的定义，称为（强）行为的 子类型化 [...]

行为亚型是比典型的子类型更强的概念 类型论中定义的函数，它仅依赖于 参数类型的逆变和返回类型的协变。 一般来说，行为子类型是无法确定的 [...]

该亚型必须满足许多行为条件 见面：

• 无法在子类型中强化先决条件。
• 子类型中的后置条件不能被削弱。
• 超类型的不变量必须保留在子类型中。

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

在你的例子中，它的上升和下降取决于你的不变量。

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

明显地Child不能用以下方式表达Parent因为不变量被打破了。这不能仅从语法推断出来。

LSP 应该引导您分别定义 Parent 和 Child，让它们都继承自Incrementable其后置条件较弱。