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

Question

        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也允许一些永远不可能为真的无谓比较（并可能导致非常微妙的bug）：

        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，而且执行LSP！

现在，Haskell的eq类型类是一种完全不同的类型

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

null

null

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

-这是绝对正确的，尽管没有真正谈到；实际上，编译器强制执行了这一点。它需要的是

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

别慌,我试着用一个例子来解释那是什么：

{-# 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'