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

我来自 Java 背景，我正试图围绕 Haskell 的类型系统展开思考。
在 Java 世界中，里氏替换原则是基本规则之一，我试图了解这是否(如果是，如何)这也是适用于 Haskell 的概念(请原谅我对 Haskell 的有限理解，我希望这个问题甚至有意义)。
例如，在 Java 中，公共(public)基类 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方法在存在子类型的情况下正确地按照其契约(Contract)(如果在子类中引入了其他字段，则实现将违反契约(Contract)的对称性和/或传递性要求)。
现在，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 替换原则不适用？

请您参考如下方法:

tl;博士 : Haskell 的类型系统不仅尊重 Liskov 替换原则——它 强制执行 它!

Now, Haskell's Eq type class is a completely different animal

是的，通常类型类是与 OO 类完全不同的动物(或元动物？)。 Liskov 替换原则是关于作为子类型的子类。因此，首先一个类需要定义一个类型，OO 类会这样做(即使是抽象类/接口(interface)，也仅限于这些值必须在子类中)。但是 Haskell 类根本不做这样的事情!你不能有一个“类的值 Eq ”。您实际拥有的是某种类型的值，该类型可能是 Eq 的一个实例。类(class)。因此，类语义与值语义完全分离。
让我们将该段落也表述为并排比较:

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 类型，而是普遍量化的类型。
不要 panic 我会尝试用一个例子来解释这是什么:

{-# LANGUAGE RankNTypes, UnicodeSyntax #-} 
 
type T = ∀ a . Ord a => a -> a -> Bool 
type S = ∀ a . Eq a => a -> a -> Bool 

claim : S是 T 的子类型.
——如果你一直在关注，那么你现在可能在想等等等等，那是错误的方法。毕竟， Eq是 Ord 的父类(super class)，不是子类。但不是， 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 确实允许一种子类型化，对于它来说，里氏替换原则只是编译器强制执行的“LSP”的推论类型类中的类型。

如果你问我，那相当整洁。

★在Haskell中我们不把值称为“对象”；对象是 something different对我们来说，这就是为什么我在这篇文章中避免使用“对象”一词。