哈斯克尔的类型系统是否遵循里氏替换原理？

types java haskell liskov-substitution-principle subtyping

2022-09-03 14:13:33

我来自Java背景，我试图围绕Haskell的类型系统来思考。在Java世界中，Liskov替换原则是基本规则之一，我试图理解这是否（如果是这样，如何）这是一个也适用于Haskell的概念（请原谅我对Haskell的有限理解，我希望这个问题甚至有意义）。

例如，在Java中，公共基类定义了所有Java类继承的方法，并允许进行如下比较：Objectboolean equals(Object obj)

        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处理相等的方式更有意义，但它似乎确实表明，像这样的类型类在允许子类型方法的参数类型方面可以更具限制性。在我看来，这似乎违反了LSP。Eq

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

答案 1

tl;dr：Haskell的类型系统不仅尊重Liskov替换原则 - 它强制执行它！

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

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

让我们把这一段也写成并排比较：

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

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

所以，现在我们已经在Haskell中建立了子类与子类的值无关，很明显，李氏原理甚至不能在这个层面上表述。您可以为类型制定类似的东西：

如果是的子类，则作为实例的任何类型的类型也可以用作的实例DCDC

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

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

对于哈斯克尔的利斯科夫问题，这可能不是一个非常有趣的答案。

不过，这里有一些东西使它更有趣。我说过Haskell没有亚型吗？好吧，实际上确实如此！不是普通的老式Haskell98类型，而是普遍量化的类型。

不要惊慌，我会尝试用一个例子来解释这是什么：

{-# LANGUAGE RankNTypes, UnicodeSyntax #-}

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

声明：是的子类型。ST

如果你一直在注意，那么你可能会在想，在这一点上，等待等待，这是错误的方式。毕竟，是的超类，而不是子类。
但是不，是亚型！EqOrdS

示范：

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中，我们不称值为“对象”;对象对我们来说是不同的东西，这就是为什么我在这篇文章中避免使用术语“对象”。}

答案 2