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

rubylouvre 阅读:18 2024-06-03 14:00:57 评论:0

我来自 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 原则甚至不能在那个层面上制定。您可以为类型制定类似的内容:
  • 如果 DC 的子类,然后是 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 : ST 的子类型.
    ——如果你一直在关注,那么你现在可能在想等等等等,那是错误的方法。毕竟, EqOrd 的父类(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对我们来说,这就是为什么我在这篇文章中避免使用“对象”一词。


    标签:java
    声明

    1.本站遵循行业规范,任何转载的稿件都会明确标注作者和来源;2.本站的原创文章,请转载时务必注明文章作者和来源,不尊重原创的行为我们将追究责任;3.作者投稿可能会经我们编辑修改或补充。

    关注我们

    一个IT知识分享的公众号