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

huangapple go评论35阅读模式
英文:

Does Haskell's type system honor the Liskov Substitution Principle?

问题

I'm coming from a Java background, and I'm trying to wrap my head around Haskell's type system.
在我来自Java背景的情况下,我正在努力理解Haskell的类型系统。

In the Java world, the Liskov Substitution Principle is one of the fundamental rules, and I'm trying to understand if (and if so, how) this is a concept that applies to Haskell as well (please excuse my limited understanding of Haskell, I hope this question even makes sense).
在Java世界中,Liskov替代原则是其中一个基本规则,我正在尝试理解这个概念是否也适用于Haskell(请原谅我对Haskell的理解有限,我希望这个问题有意义)。

For example, in Java, the common base class Object defines the method boolean equals(Object obj) which is consequently inherited by all Java classes and allows for comparisons like the following:
例如,在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);

Unfortunately, due to the Liskov Substitution Principle, a subclass in Java cannot be more restrictive than the base class in terms of what method arguments it accepts, so Java also allows some nonsensical comparisons that can never be true (and can cause very subtle bugs):
不幸的是,由于Liskov替代原则,Java中的子类在接受方法参数方面不能比基类更加严格,因此Java也允许一些毫无意义的比较,这些比较永远不可能为真(并且可能引起非常微妙的错误):

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

Another unfortunate side effect is that, as Josh Bloch pointed out in Effective Java a long time ago, it is basically impossible to implement the equals method correctly in accordance with its contract in the presence of subtyping (if additional fields are introduced in the subclass, the implementation will violate the symmetry and/or transitivity requirement of the contract).
另一个不幸的副作用是,正如Josh Bloch在很久以前的Effective Java中指出的那样,在存在子类型的情况下,基本上不可能正确地实现equals方法,以符合其合同(如果在子类中引入了额外的字段,实现将违反合同的对称性和/或传递性要求)。

Now, Haskell's Eq type class is a completely different animal:
现在,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

Here, comparisons between objects of different types get rejected with an error:
在这里,不同类型的对象之间的比较会被拒绝并产生错误:

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>

While this error intuitively makes a lot more sense than the way Java handles equality, it does seem to suggest that a type class like Eq can be more restrictive with regards to what argument types it allows for methods of subtypes. This appears to violate the LSP, in my mind.
虽然这个错误在直觉上比Java处理相等性的方式更有意义,但它似乎表明像Eq这样的类型类可以对它允许用于子类型的方法的参数类型更加严格。在我看来,这似乎违反了LSP。

My understanding is that Haskell does not support "subtyping" in the object-oriented sense, but does that also mean that the Liskov Substitution Principle does not apply?
我理解Haskell不支持面向对象的意义上的“子类型”,但这是否意味着Liskov替代原则不适用?

英文:

I'm coming from a Java background, and I'm trying to wrap my head around Haskell's type system.
In the Java world, the Liskov Substitution Principle is one of the fundamental rules, and I'm trying to understand if (and if so, how) this is a concept that applies to Haskell as well (please excuse my limited understanding of Haskell, I hope this question even makes sense).

For example, in Java, the common base class Object defines the method boolean equals(Object obj) which is consequently inherited by all Java classes and allows for comparisons like the following:

        String hello = &quot;Hello&quot;;
        String world = &quot;World&quot;;
        Integer three = 3;

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

Unfortunately, due to the Liskov Substitution Principle, a subclass in Java cannot be more restrictive than the base class in terms of what method arguments it accepts, so Java also allows some nonsensical comparisons that can never be true (and can cause very subtle bugs):

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

Another unfortunate side effect is that, as Josh Bloch pointed out in Effective Java a long time ago, it is basically impossible to implement the equals method correctly in accordance with its contract in the presence of subtyping (if additional fields are introduced in the subclass, the implementation will violate the symmetry and/or transitivity requirement of the contract).

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

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

Here, comparisons between objects of different types get rejected with an error:

Prelude&gt; data PersonPlusAge = PersonPlusAge { firstName :: String, lastName :: String, age :: Int } deriving (Eq)
Prelude&gt; james65 = PersonPlusAge {  firstName = &quot;James&quot;, lastName = &quot;Gosling&quot;, age = 65}
Prelude&gt; james65 == james65
True
Prelude&gt; james65 == james

&lt;interactive&gt;:49:12: error:
    • Couldn&#39;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&gt;

While this error intuitively makes a lot more sense than the way Java handles equality, it does seem to suggest that a type class like Eq can be more restrictive with regards to what argument types it allows for methods of subtypes. This appears to violate the LSP, in my mind.

My understanding is that Haskell does not support "subtyping" in the object-oriented sense, but does that also mean that the Liskov Substitution Principle does not apply?

答案1

得分: 19

tl;dr: Haskell的类型系统不仅遵守了Liskov替换原则 - 它还强制执行了这一原则!


现在,Haskell的Eq类型类是完全不同的概念

是的,总的来说,类型类与面向对象类是完全不同的概念(或者说是元概念?)。Liskov替换原则主要关于子类作为子类型。首先,类需要定义一种类型,而面向对象类确实做到了这一点(甚至对于抽象类/接口,仅对这些值而言,它们必须位于子类中)。但是Haskell类完全不具备这方面的功能!你不能拥有“属于Eq类的值”。实际上,你拥有的是某种类型的值,而那种类型可能是Eq类的实例。因此,类的语义与值的语义完全分离。

我们可以将这段话也进行并列对比:

  • 面向对象:类包含
    • 值(更常称为对象
    • 子类(其值也是父类的值)
  • Haskell:类包含
    • 类型(称为类的实例
    • 子类(其实例也是父类的实例)

需要注意的是,Haskell类的描述甚至没有以任何方式提及值。实际上,你甚至可以创建那些与运行时值完全无关的类的方法。

因此,现在我们已经确定了Haskell中的子类化与子类的值无关,很明显Liskov原则甚至无法在这个层次上得以形式化。你可以为类型类似地形式化一些内容:

  • 如果DC的子类,那么任何D的实例也可以被用作C的实例。

这完全是正确的,尽管不常讨论;实际上,编译器强制执行这一点。它包含以下内容:

  • 为了为你的类型T编写instance Ord T,你必须首先编写一个instance Eq T(当然,这个Eq实例本身也是有效的,无论是否定义了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

主张:ST的子类型。

  • 如果你一直关注着,那么现在你可能会认为“等等等等,方向错了”。毕竟,EqOrd超类,而不是子类。但不,S才是子类型!

示例:

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

y :: T
y = x

反过来是不可能的:

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

x' :: S
x' = y'

错误信息:

• 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中,我们不称值为“对象”;在我们看来,对象是另一种东西,这就是为什么我在本文中避免使用“对象”这个术语。

英文:

tl;dr: Haskell's type system not only honors the Liskov Substitution Principle – it enforces it!

<hr>

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

Yes, and in general type classes are a completely different animal (or meta-animal?) from OO classes. The Liskov Substitution Principle is all about subclasses as subtypes. So first of all a class needs to define a type, which OO classes do (even abstract ones / interfaces, only, for those the values must be in a subclass). But Haskell classes don't do anything like this at all! You can't have a “value of class Eq”. What you actually have is a value of some type, and that type may be an instance of the Eq class. Thus, class semantics are completely detached from value semantics.

Let's formulate that paragraph also as a side-by-side comparison:

  • OO: classes contain
    • values (better known as objects<sup>★</sup>)
    • subclasses (whose values are also values of the parent class)
  • Haskell: classes contain
    • types (known as instances of the class)
    • subclasses (whose instances are also instances of the parent class)

Note that the description of a Haskell class does not even mention values in any way. (As a matter of fact, you can have classes that don't have methods that are concerned with any runtime values at all!)

So, now we've established subclassing in Haskell has nothing to do with values of a subclass, it's clear that the Liskov principle can't even be formulated on that level. You could formulate something similar for types:

  • If D is a subclass of C, then any type that's an instance of D can also be used as an instance of C

– which is absolutely true, albeit not really talked about; indeed the compiler enforces this. What it entails is

  • In order to write an instance Ord T for you type T, you must first also write an instance Eq T (which would of course be just as valid on its own, irrespective of whether the Ord instance is defined too)
  • If the constraint Ord a appears in a function's signature, then the function can automatically also assume that the type a has a valid Eq instance too.

That may not be a really interesting answer to the question of Liskov in Haskell.

Here's something that makes it a bit more interesting though. Did I say Haskell doesn't have subtypes? Well, actually it does! Not plain old Haskell98 types, but universally quantified types.

DON'T PANIC I'll try to explain what that is with an example:

<!-- language-all: haskell -->

{-# LANGUAGE RankNTypes, UnicodeSyntax #-}

type T = ∀ a . Ord a =&gt; a -&gt; a -&gt; Bool
type S = ∀ a . Eq a =&gt; a -&gt; a -&gt; Bool

Claim: S is a subtype of T.

–If you've been paying attention then you're probably thinking at this point wait wait wait, that's the wrong way around. After all, Eq is a <i>super</i>class of Ord, not a subclass.<br>But no, S is the subtype!

Demonstration:

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

y :: T
y = x

The other way around is not possible:

y&#39; :: T
y&#39; a b = a&gt;b

x&#39; :: S
x&#39; = y&#39;

<pre><code>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'
</code></pre>

<br>
Properly explaining Rank-2 types / universal quantification would lead a bit too far here, but my point is: Haskell does allow a kind of subtyping, and for it the Liskov Substitution Principle is a mere corollary of the compiler-enforced “LSP” for types in typeclasses.
<br><br>
And that's rather neat, if you ask me.

<hr>
<br>
<sup>★</sup><sub>We don't call values “objects” in Haskell; objects are <a href="https://en.wikipedia.org/wiki/Category_(mathematics)#Definition">something different</a> for us, that's why I avoid the term “object” in this post.</sub>

huangapple
  • 本文由 发表于 2020年8月2日 05:34:55
  • 转载请务必保留本文链接:https://go.coder-hub.com/63210289.html
匿名

发表评论

匿名网友

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen:

确定