Учитывает ли система типов Haskell принцип подстановки Лискова?

Question

Я исхожу из фона Java и пытаюсь осмыслить систему типов Haskell. В мире Java принцип замещения Лискова является одним из фундаментальных правил, и я пытаюсь понять, применима ли (и если да, то как) эта концепция и к Haskell (пожалуйста, извините за мои ограниченные возможности). понимание Haskell, я надеюсь, что этот вопрос имеет смысл).

Например, в 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);

К сожалению, из-за принципа подстановки Лискова подкласс в Java не может быть более ограничительным, чем базовый класс, с точки зрения того, какие аргументы метода он принимает , поэтому Java также допускает некоторые бессмысленные сравнения, которые никогда не могут быть правдой (и могут вызвать очень тонкие ошибки):

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

Другой неприятный побочный эффект состоит в том, что, как указал Джо sh Блох в Действует Java долгое время go, метод equals правильно реализовать в соответствии с его контракт при наличии подтипов (если в подкласс введены дополнительные поля, реализация нарушит требование симметрии и / или транзитивности контракта).

Теперь Haskell s Eq type class - это совершенно другое животное:

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 не поддерживает «подтипирование» в объектно-ориентированном смысле, но означает ли это также, что принцип замещения Лискова не применяется ?

Answer 1

tl; dr : «Учитывает ли система типов Haskell принцип замещения Лискова?» —— Он не только соблюдает LSP, он применяет it!

---

Теперь, Haskell s Eq типовой класс это совершенно другое животное

Да, и вообще типовые классы - это совершенно разные животные (или мета-животные?) от ОО-классов. Принцип замещения Лискова - это подклассы как подтипы . Итак, прежде всего класс должен определить тип, который делают классы OO (даже абстрактные / интерфейсы, только для них значения должны быть в подклассе). Но классы Haskell ничего подобного не делают! Вы не можете иметь «значение класса Eq». На самом деле у вас есть значение некоторого типа, и этот тип может быть экземпляром класса Eq. Таким образом, семантика классов полностью отделена от семантики значений.

Давайте сформулируем этот абзац также как параллельное сравнение:

• OO: классы содержат
  • значения (более известные как объекты ^★ )
  • подклассы (значения которых также являются значениями родительского класса)
• Haskell: классы содержат
  • типов (известные как экземпляры класса)
  • подклассы (чьи экземпляры также являются экземплярами родительского класса)

Обратите внимание, что в описании класса Haskell значения даже не упоминаются. (Фактически, у вас могут быть классы, у которых даже нет методов, связанных с какими-либо значениями времени выполнения!)

Итак, теперь мы установили подклассы в Haskell, не имеющие ничего общего с значений подкласса , ясно, что принцип Лискова даже не может быть сформулирован на этом уровне. Вы могли бы сформулировать что-то подобное для типов:

• Если D является подклассом C, тогда и введите этот экземпляр D также можно использовать как экземпляр C

- что абсолютно верно, хотя и не обсуждается; действительно, компилятор обеспечивает это. Это влечет за собой

• Для того, чтобы написать instance Ord T для вашего типа T, вы должны сначала также написать instance Eq T (что, конечно же, было бы так же действительным само по себе, независимо от того, определен ли также экземпляр Ord)
• Если ограничение Ord a появляется в сигнатуре функции, функция также может автоматически предполагать, что тип a имеет действительный экземпляр Eq тоже.

Это может быть не очень интересный ответ на вопрос Лискова в Haskell.

Вот кое-что, что делает его немного более интересным хотя. Я сказал, что Haskell не имеет подтипов? Что ж, это действительно так! Не обычные старые типы Haskell98, а универсально определенные типы .

НЕ ПАНИ C Я попытаюсь объяснить, что это такое, на примере:

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

Правильное объяснение типов Rank-2 / универсальной количественной оценки привело бы здесь слишком далеко, но моя точка зрения: Haskell действительно допускает своего рода подтипирование, и для него принцип подстановки Лискова является простым следствием принудительного компилятора «LSP» для типов в классах типов.

И это довольно мило, если вы спросите меня.

---

^★ _{Мы не называем значения «объектами» в Haskell; объекты - это что-то другое для нас, поэтому я избегаю термина «объект» в этом посте.}