Haskell的类型系统是否遵守Liskov替换原则？

Question

Haskell的类型系统是否遵守Liskov替换原则？

javahaskelltypesliskov-substitution-principlesubtyping

15

我来自Java背景，现在正在尝试理解Haskell的类型系统。在Java世界中，里氏替换原则是基本规则之一，我想知道这是否也适用于Haskell（请原谅我对Haskell的了解有限，希望我的问题有意义）。

例如，在Java中，通用的基类Object定义了方法boolean equals(Object obj)，因此被所有Java类继承，并允许进行如下比较：

        String hello = "Hello";
        String world = "World";
        Integer three = 3;

        Boolean a = hello.equals(world);
        Boolean b = world.equals("World");
        Boolean c = three.equals(5);

不幸的是，由于 Liskov 替换原则，在 Java 中，子类不能比基类更加限制接受哪些方法参数，因此 Java 也允许一些毫无意义的比较，这些比较永远不可能为真（并且可能导致非常微妙的错误）：

        Boolean d = "Hello".equals(5);
        Boolean e = three.equals(hello);

另一个不幸的副作用是，正如Josh Bloch在很长时间之前在Effective Java中指出的那样，在存在子类型的情况下基本上不可能根据其合同正确实现equals方法（如果在子类中引入了附加字段，则实现将违反合同的对称性和/或传递性要求）。

现在，Haskell的Eq类型类是完全不同的东西：

Prelude> data Person = Person { firstName :: String, lastName :: String } deriving (Eq)
Prelude> joshua = Person { firstName = "Joshua", lastName = "Bloch"}
Prelude> james = Person { firstName = "James", lastName = "Gosling"}
Prelude> james == james
True
Prelude> james == joshua
False
Prelude> james /= joshua
True

这里，不同类型对象之间的比较会被拒绝并报错：

Prelude> data PersonPlusAge = PersonPlusAge { firstName :: String, lastName :: String, age :: Int } deriving (Eq)
Prelude> james65 = PersonPlusAge {  firstName = "James", lastName = "Gosling", age = 65}
Prelude> james65 == james65
True
Prelude> james65 == james

<interactive>:49:12: error:
    • Couldn't match expected type ‘PersonPlusAge’
                  with actual type ‘Person’
    • In the second argument of ‘(==)’, namely ‘james’
      In the expression: james65 == james
      In an equation for ‘it’: it = james65 == james
Prelude>

虽然这个错误比Java处理相等性的方式更直观，但它似乎表明像Eq这样的类型类可以对其子类型的方法允许的参数类型进行更严格的限制。在我看来，这似乎违反了LSP。

我的理解是，Haskell不支持面向对象意义上的“子类型”，但这是否意味着Liskov替换原则不适用？

- raner

6

Liskov替换原则的概念在函数式语言中被称为“逆变性”：https://typeclasses.com/contravariance https://www.fpcomplete.com/blog/2016/11/covariance-contravariance/ - Willem Van Onsem

8

在没有子类型的语言，如Haskell中，我无法准确地看到LSP是什么。对我来说，LSP主要涉及面向对象编程中的对象、它们的不变量以及如何创建一个子类而不破坏不变量，使其可以替代超类。我看不出这如何适用于Haskell。 - chi

@WillemVanOnsem，我不明白你的意思。事实上，面向对象的子类型化可以被描述为协变多态性，这无疑是一些范畴论函子的东西。但是，Haskell的逆变函子类如何提供任何可比较的功能呢？ - leftaroundabout

1

“Typeclass” 这个词对于来自面向对象编程的人们来说可能具有误导性。它们应该被字面理解为 “类型的类”，即 Haskell 中的单参数类型类是类型的集合，而合法的实例则是该类型在集合中的证明；多参数类（MPTC）是类型之间的关系；函数依赖和类型族允许作用于类型的函数。子类是子集（或子关系）：class Eq a => Ord a 表示如果一个类型在 Ord 中，则它也必须在 Eq 中，因此 Ord 是 Eq 的子集。（箭头 => 是逆推符号。） - Jon Purdy

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- leftaroundabout · Accepted Answer

tl;dr: Haskell的类型系统不仅遵循了Liskov替换原则，而且还强制执行它！

现在，Haskell的Eq类型类是一个完全不同的动物

是的，总的来说，类型类与OO类是完全不同的东西（或者说是元动物？）。Liskov替换原则关注的是子类作为子类型。因此，首先一个类需要定义一个类型，这是OO类所做的（即使是抽象类/接口，只有那些值必须位于子类中）。但是Haskell类根本不会做任何这样的事情！你不能拥有“类Eq的值”。实际上你拥有的是某种类型的值，并且该类型可以是Eq类的一个实例。因此，类的语义与值的语义完全分离。

让我们将该段落也作为一个并排比较来表述：

OO：类包含
- 值（更为人所知的是对象^★）
- 子类（其值也是父类的值）
Haskell：类包含
- 类型（称为类的实例）
- 子类（其实例也是父类的实例）

请注意，Haskell类的描述根本没有以任何方式提到值。（事实上，你可以有一些根本不涉及任何运行时值的方法的类！）

因此，现在我们已经确定了Haskell中的子类化与子类的值无关，很明显Liskov原则甚至不能在那个级别上表述。你可以为类型制定类似的东西：

如果D是C的一个子类，则任何作为D实例的类型也可以用作C的实例

这是绝对正确的，尽管并没有真正讨论；确实编译器强制执行这一点。它意味着：

为了写一个你的类型T的instance Ord T，你必须首先写一个instance Eq T（当然，无论是否定义了Ord实例，它本身也是有效的）
如果约束Ord a出现在函数的签名中，则该函数还可以自动假定类型a也具有有效的Eq实例。

这可能不是对于“Liskov在Haskell中”的问题的一个非常有趣的答案。

然而，以下内容可能会让它变得更加有趣。我之前说过Haskell没有子类型吗？实际上它有！不是普通的Haskell98类型，而是“全称量化类型”。

不要惊慌，我会尝试通过一个例子来解释它：

{-# LANGUAGE RankNTypes, UnicodeSyntax #-}

type T = ∀ a . Ord a => a -> a -> Bool
type S = ∀ a . Eq a => a -> a -> Bool

声明： S 是 T 的子类型。

- 如果你一直在关注，那么你可能会认为此时情况是错误的。毕竟，Eq 是 Ord 的超类，而不是子类。
但是，不，S 是子类型！

演示：

x :: S
x a b = a==b

y :: T
y = x

另一种方式是不可能的：

y' :: T
y' a b = a>b

x' :: S
x' = y'

error:
    • Could not deduce (Ord a) arising from a use of ‘y'’
      from the context: Eq a
        bound by the type signature for:
                   x' :: S
      Possible fix:
        add (Ord a) to the context of
          the type signature for:
            x' :: S
    • In the expression: y'
      In an equation for ‘x'’: x' = y'

^★ _{在Haskell中，我们不称值为“对象”；对于我们来说，“对象”是另一回事，这就是为什么我在本篇文章中避免使用“对象”一词的原因。}