Почему у всех классов Haskell есть законы?

Ответ 1

Вы заметите, что почти всегда законы являются алгебраическими законами. Они могут быть выражены системой типов с использованием некоторых расширений, но доказательства были бы громоздкими для выражения. Таким образом, у вас есть непроверенные законы, и потенциальные реализации могут нарушить их. Почему это хорошо?

Причина в том, что шаблоны проектирования, используемые в Haskell, мотивированы (и в большинстве случаев отражены) математическими структурами, как правило, из абстрактной алгебры. Хотя большинство других языков имеют интуитивное представление о некоторых функциях, таких как безопасность, производительность и семантика, мы программисты Haskell предпочитают устанавливать формальное понятие. Преимущество этого заключается в следующем: когда ваши типы и функции подчиняются законам безопасности, они безопасны в смысле лежащей в основе алгебраической структуры. Они действительно безопасны.

В качестве примера возьмем функторы. Функтор Haskell имеет следующие два закона:

fmap f . fmap g = fmap (f . g)
fmap id         = id

Во-первых, это очень важно: функции в Haskell непрозрачны. Вы не можете исследовать, сравнивать или что-то еще. Хотя это звучит как плохо в Haskell, на самом деле это очень хорошо. Функция fmap не может проверить функцию, которую вы передали. В частности, он не может проверить, что вы прошли идентификационную функцию или передали композицию. Короче: он не может обмануть! Единственный способ подчиниться этим двум законам - фактически не вводить никаких собственных эффектов. Это означает, что в надлежащем функторе fmap никогда не будет ничего неожиданного. На самом деле он не может ничего сделать, кроме как сопоставить данную функцию. Это очень простой пример, и я не объяснил все тонкости, почему fmap не может обмануть, но он демонстрирует точку.

Теперь распространите это по всему языку, базовым библиотекам и наиболее разумным сторонним библиотекам. Это дает вам язык, который так же предсказуем, как язык может получить. Когда вы пишете код, вы знаете, что он собирается делать. Это одна из основных причин, почему код Haskell часто работает из коробки. Я часто пишу страницы кода Haskell перед компиляцией. Как только мои ошибки типа исправлены, моя программа обычно работает.

Другая причина, по которой это желательно, заключается в том, что она позволяет создавать более композиционный стиль программирования. Это особенно полезно при работе в команде. Сначала вы сопоставляете свое приложение с алгебраическими структурами и устанавливаете необходимые законы. Например: вы выражаете то, что означает, что что-то является допустимым веб-сервером. В частности, вы устанавливаете формальное представление о составе веб-сервера. Если вы создаете два допустимых веб-сервера, результатом будет действительный веб-сервер. Вы видите, где это происходит? После установления этих законов товарищи по команде идут на работу, и они работают изолированно. Для выполнения своей работы не требуется никакого общения. Когда они снова встречаются, каждый представляет свои действительные веб-серверы, и они просто создают их для создания конечного продукта, веб-сайта. Поскольку отдельные компоненты были действительными веб-серверами, конечным результатом должен быть действительный веб-сервер. Доказуемо.

Ответ 2

Да и нет. Например, класс Show не имеет каких-либо законов, связанных с ним, и это, безусловно, полезно.

Тем не менее, typeclasses выражают интерфейсы. Интерфейс должен удовлетворять больше, чем просто набор функций - вы хотите, чтобы эти функции выполняли спецификацию. Спецификация обычно сложнее, чем то, что может быть выражено в системе типа Haskell. Например, возьмите класс Eq. Он должен только предоставить нам функцию, тип которой должен быть a -> a -> Bool. То, что система Haskell больше всего позволит нам потребовать от экземпляра типа Eq. Однако мы обычно ожидаем большего от этой функции - вы, вероятно, захотите, чтобы это отношение эквивалентности (рефлексивное, симметричное и транзитивное). Итак, вы указываете эти требования как отдельные "законы".

Ответ 3

В классной строке нет законов, но она будет полезна, если она есть. Ожидается, что многие типы моделей будут функционировать определенным образом, законы кодифицируют ожидания пользователей. Законы позволяют пользователям делать предположения о том, как будет работать экземпляр класса. Если вы нарушаете законы о товарных знаках, вас не арестовывает полиция Haskell, вы просто получаете путаные пользователи.