如何考虑子类型的多态性答案

【问题标题】：How to think about polymorphism with subtyping如何考虑子类型的多态性
【发布时间】：2014-09-17 02:40:22
【问题描述】：

里氏替换原则指出：

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

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

所以，我知道当函数的参数是逆变的并且它们的返回类型是协变的时，函数就是子类型。我们可以假设方法只是带有隐式“self”参数的函数。但是，这似乎意味着如果子类覆盖了父类的方法，则它不再是子类型，因为其中一个方法不再是子类型。

例如。取如下伪代码：

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

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

所以回到 LSP：我们可以说 Parent.increment() 的属性应该适用于 Child.increment()，即使这两个不遵循严格的子类型关系？

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

【问题讨论】：

标签： oop types polymorphism theory liskov-substitution-principle

【解决方案1】：

引用维基百科关于Liskov Substitution Principle的文章

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

行为子类型比典型的子类型更强大的概念类型论中定义的函数，它只依赖于参数类型的逆变和返回类型的协变。行为子类型通常难以确定 [...]

子类型必须具备许多行为条件见面：

先决条件不能在子类型中得到加强。

不能在子类型中削弱后置条件。

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

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

在您的示例中，这取决于您的不变量。

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

显然 Child 不能用 Parent 表示，因为不变量被破坏了。这不能仅从语法推断出来。

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

【讨论】：

我的问题更多是关于论点的语义。 LSP 声明一个不变量适用于子类型当且仅当它适用于超类型。子类型关系表明对于函数a -> b <: c -> d iff c <: a 和b <: d。根据子类型的定义，Child.increment() 不是Parent.increment() 的子类型。那么，为什么要申请 LSP？
正确的思维方式是 LSP 是多态性何时有意义的指南，而不是它的逻辑/数学属性。多态性为您提供汽车。 LSP 说你应该只在路上开车。你在说“嘿，看我在人行道上开车。LSP 坏了”。是吗？
我的理解是 Liskov 本人为该原理提供了非常理论和数学基础。关于这个问题有很多论文。所以，基于这些理由，我不同意你的前提，即 LSP 只是一个指导方针。
好吧，公平地说，您的问题的措辞很容易被解释为哲学问题，而不是核心理论问题。但也许这是我的偏见。我的类型理论课已经有一段时间了，但我从不记得这个理论是“正确的”。无论如何，Liskov substitution principle 回答了您的理论问题：我将编辑我的答案。
谢谢。我的问题并不完全清楚。我认为这个答案非常好。需要澄清一点：它在链接中引用的类型是 class 的类型，而不是类上的方法。例如：increment will increase count 作为方法的属性没有意义，因为它提出了一个问题，什么是计数？一个推论是：Child.increment : Parent -> () 而不是Child.increment : Child -> ()。它们实际上是一种在不同类型下表现不同的方法（从逻辑上讲）。

【解决方案2】：

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

Liskov 原则是关于行为子类型化，如 wikipedia 中所述。它需要句法子类型，但它也取决于您对类的不变量和前置/后置条件的定义。由于您没有定义任何内容，因此谈论违规行为是荒谬的。

如果将increment的后置条件定义为new count = old count + 1，则存在违规。

如果您将increment 的后置条件定义为new count > old count，则没有。

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

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

【讨论】：