Какие законы должны соблюдать стандартные классы типов Haskell?

Хорошо известно, что экземпляры Monad должны подчиняться законам монад. Возможно, менее известно, что экземпляры Functor должны следовать законам функтора. Тем не менее, я бы чувствовал себя достаточно уверенно, написав правило перезаписи GHC, оптимизирующее fmap id == id.

Какие еще стандартные классы имеют неявные законы? Должен ли (==) быть истинным отношением эквивалентности? Должен ли Ord формировать частичный заказ? Полный порядок? Можем ли мы хотя бы предположить, что оно транзитивно? Антисимметричный?

Эти последние несколько, похоже, не указаны в отчете Haskell 2010, и я не чувствую себя уверенно при написании правил перезаписи, использующих их. Однако существуют ли какие-либо общие библиотеки? Насколько патологический экземпляр можно уверенно писать?

Наконец, если предположить, что существует граница того, насколько патологическим может быть такой экземпляр, существует ли стандартный всеобъемлющий ресурс для законов, которые должен соблюдать каждый экземпляр класса типов?

Например, сколько проблем у меня возникло бы, чтобы определить

newtype Doh = Doh Bool
instance Eq Doh where a == (Doh b) = b

это просто сложно понять или компилятор везде неправильно оптимизирует?


interface haskell proof
person J. Abrahamson    schedule 13.02.2013    source источник
comment
Обратите внимание, что довольно много разумно звучащих законов (включая те, которые молчаливо принимаются существующим кодом), которые можно предложить для Ord, Num и родственных классов, будут нарушены экземплярами для Float и Double. Например, использование NaN в качестве ключа прерывает поиск в Data.Map, а проблемы с точностью означают, что сложение с плавающей запятой не является ассоциативным.   -  person C. A. McCann    schedule 13.02.2013
comment
@C.A.McCann, это просто означает, что в прелюдии есть экземпляры, которых не должно быть! Float и Double не должны быть членами Eq   -  person Philip JF    schedule 14.02.2013
comment
@PhilipJF: С одной стороны, я согласен. Но их экземпляр Num немногим лучше, и следование этой аргументации до логического завершения приводит к удалению всех экземпляров, которые могли бы сделать типы с плавающей запятой практически полезными. Между прочим, я продемонстрировал, насколько неисправен их экземпляр Ord в старом сообщении.   -  person C. A. McCann    schedule 14.02.2013
comment
@C.A.McCann Я согласен с экземплярами, пока эти типы ограничены специальными модулями, ориентированными на производительность. Зачем вообще иметь типы с плавающей запятой в Prelude? Если вам действительно нужно число с плавающей запятой (а не отношение или конструктивное число), вы, вероятно, все равно знаете, что делаете.   -  person Philip JF    schedule 14.02.2013
comment
Возможно, стоит отметить, что в стандартном ML действительные числа не являются типами равенства< /а>. Таким образом, по крайней мере еще один язык предпочел правильность полезности. :)   -  person Daniel Lyons    schedule 14.02.2013
comment
Этот вопрос был вызван осознанием того, что вещественные числа не являются (разрешимыми) типами равенства. Re math.andrej.com/2006/03/ 27/ и... комментарий в другом вопросе SO, который я не могу найти прямо сейчас   -  person J. Abrahamson    schedule 14.02.2013

Ответы (3)


arrow_upward
5
arrow_downward

В отчете Haskell упоминаются законы для:

  • Функтор (например, fmap id == id)
  • Монада (например, m >>= return == m)
  • Интеграл (например, (x ‘quot‘ y)*y + (x ‘rem‘ y) == x)
  • Число (abs x * signum x == x)
  • Показать (showsPrec d x r ++ s == showsPrec d x (r ++ s))
  • Ix (e.g. inRange (l,u) i == elem i (range (l,u)))

Это все, что я смог найти. В частности, в разделе об уравнении (6.3.1) не упоминаются никакие законы, как и в следующем разделе об Ord.

person David    schedule 16.02.2013

arrow_upward
4
arrow_downward

Мое собственное мнение о том, какими «должны быть» законы, не подтверждается всеми стандартными примерами, но я думаю,

  • Eq должно быть отношением эквивалентности.
  • Ord должен быть полный порядок
  • Num должно быть кольцом, fromInteger — кольцевым гомоморфизмом, а abs/signum ведет себя очевидным образом.

Большая часть кода будет предполагать, что эти «законы» выполняются, даже если это не так. Это не специфичная проблема Haskell, ранний C позволял компилятору переупорядочивать арифметику в соответствии с алгебраическими законами, и у большинства компиляторов есть возможность повторно включить такую ​​оптимизацию, даже если они не разрешены текущим стандартом и могут изменить результаты ваших программ.

person Philip JF    schedule 13.02.2013
comment
Я в основном согласен с вами, хотя, насколько мне известно, ничто не идет плохо, если эти обозначения нарушаются. Вот суть того, что я хотел бы знать — насколько я не прав? Является ли определение нерефлексивного экземпляра Eq не только сложным, но и оптимизированным, чтобы быть неверным? - person J. Abrahamson; 14.02.2013
comment
@tel Я сомневаюсь, что оптимизация будет неправильной, но, безусловно, многие функции имеют непредсказуемые результаты. - person Philip JF; 14.02.2013
comment
Да, на мой взгляд, есть жесткий сбой, когда правило перезаписи сбивает вас с толку, и мягкий сбой, когда вы идете против преобладающих предположений в языке, и это просто сбивает с толку. Оба плохи, но один хуже. Вероятно, типичным примером будет Eq Double. - person J. Abrahamson; 14.02.2013
comment
@tel, это не просто сбивает с толку. Некоторые функции будут давать неправильные результаты. Рассмотрим поведение Map Float a (где Float может нарушать предположения об упорядочении) или sortBy и nubBy с типами, которые нарушают предположения об упорядочении/равенстве. Вы получите неправильное поведение. Я бы посчитал это серьезным сбоем, хотя это не имеет ничего общего с поведением компилятора. - person John L; 14.02.2013
comment
Я полагаю, на мой взгляд, это просто означает, что вы ожидаете экземпляр, отличный от реализации. Я ожидаю, что nub на [Double] должно удалять дубликаты, но поскольку денотативное Double равенство обычно неразрешимо, это действительно мое внутреннее обозначение того, как работает равенство, которое выходит из строя. Это сильно отличается от правила перезаписи компилятора, такого как forall x. x == x = True, которое определенно правильно, если Eq является рефлективным, но может быть признано недействительным. - person J. Abrahamson; 14.02.2013
comment
@tel: Eq Float имеет больше смысла, если вы думаете об этом как об идентичности, а не о числовом равенстве - подумайте о том, как ссылочное равенство используется в некоторых языках. NaN нарушает интуитивные предположения, но в остальном ведет себя хорошо. С другой стороны, Ord Float полностью нарушает любой разумный стандарт, что можно продемонстрировать, используя compare на NaN. Ссылка в моем комментарии к вопросу демонстрирует последствия этого. - person C. A. McCann; 14.02.2013
comment
Идентичность зависит от некоторого глобального состояния --- мой помешанный на Agda ум говорит, что это означает, что Eq использует доказательство уровня глобального состояния refl :: Eq x x. - person J. Abrahamson; 14.02.2013

arrow_upward
1
arrow_downward

Раньше считалось, что нарушение законов Ix позволит вам сделать что угодно. В эти дни я думаю, что они исправили это. Дополнительная информация здесь: Кто-нибудь знает (или помнит), как нарушение законов о классах может вызвать проблемы в GHC?

person sclv    schedule 28.02.2013