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

Question

我来自 Java 背景，我正在尝试围绕 Haskell 的类型系统进行研究。在 Java 世界中，Liskov 替换原则是基本规则之一，我试图了解是否（如果是，如何）这也是适用于 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 替换原则不适用？

Answer 1

tl;dr：“Haskell 的类型系统是否遵循 Liskov 替换原则？” ——不仅尊重LSP，还强制执行！

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

是的，通常类型类是与 OO 类完全不同的动物（或元动物？）。Liskov 替换原则是关于作为子类型的子类。因此，首先一个类需要定义一个类型，OO 类可以这样做（即使是抽象类/接口，仅对于那些值必须在子类中的类）。但是 Haskell 类根本不会做这样的事情！你不能拥有“类的价值Eq”。您实际拥有的是某种类型的值，而该类型可能是Eq该类的一个实例。因此，类语义与值语义完全分离。

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

• OO：类包含
  • 值（更好地称为对象^？）
  • 子类（其值也是父类的值）
• Haskell：类包含
  • 类型（称为类的实例）
  • 子类（其实例也是父类的实例）

请注意，Haskell 类的描述甚至没有以任何方式提及值。（事实上​​，您可以拥有甚至没有与任何运行时值相关的方法的类！）

所以，现在我们已经在 Haskell 中建立了子类与子类的值无关，很明显 Liskov 原则甚至无法在该级别上制定。您可以为类型制定类似的内容：

• 如果D是 的子类C，则D作为 的实例的类型也可以用作 的实例C

– 这绝对是真的，尽管没有真正谈论过；编译器确实强制执行了这一点。它意味着什么

• 为了给instance Ord T你写一个类型T，你必须首先写一个instance Eq T（当然，它本身同样有效，不管Ord实例是否被定义）
• 如果约束Ord a出现在函数的签名中，那么该函数也可以自动假定该类型a也有一个有效的Eq实例。

对于 Haskell 中的Liskov问题，这可能不是一个真正有趣的答案。

不过，这里有一些让它变得更有趣的东西。我说过 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'

在这里正确解释 Rank-2 类型/通用量化会有点过头，但我的观点是：Haskell 确实允许一种子类型，并且对于它，Liskov 替换原则仅仅是编译器强制执行的“LSP”的必然结果类型类中的类型。

如果你问我，那相当整洁。
^? _{在 Haskell 中，我们不称值为“对象”；对象对我们来说是不同的东西，这就是为什么我在这篇文章中避免使用术语“对象”。}