Алгебраические законы, как правило, обычно определяются только с точки зрения эквациональных тождеств, а не для неравновесности. С точки зрения думать об этом - теория моделей. Теория можно рассматривать как 1) набор символов разных явлений, так что из них могут быть построены предложения (т. Е. Из arity 0 мы могли бы иметь последовательности цифр, arity 1 мы имеем отрицание и arity два - дополнение) и 2) набор уравнений, обеспечивающих отношения между предложениями, построенными из таких сигнатур.
Это позволяет нам описывать такие вещи, как различные арифметические теории, группы, кольца, модули и т.д.
Теперь модель из теории представляет собой набор конкретных заданий математических объектов (чисел, функций и т.д.) к элементам сигнатуры, так что перевод предложений в элементы модели соответствует этим уравнениям.
Категорически мы часто рассматриваем теорию как особую категорию всех возможных предложений, порожденных сигнатурой. Стрелки в этой категории - это импликации - предложения, которые могут быть получены от других посредством применения эквациональных тождеств. Это, в свою очередь, индуцирует эквивалентности между всеми предложениями, которые одинаковы при применении эквациональных тождеств (это дает подход «генераторы и отношения»). И, в свою очередь, модель является просто функтором этой теории для любой другой категории, хотя обычно Set.
Это дает очень приятное дополнение синтаксиса и семантики. Чем больше набор предложений, которые вы хотите моделировать, тем меньше моделей вы можете получить, и чем больше у вас моделей, тем меньше набор предложений, которые будут удовлетворены всеми из них. (Здесь я просто набросал идею, а не заполнял множество важных деталей).
В любом случае, одним из последствий этого является то, что люди склонны игнорировать, но это действительно окупается, заключается в том, что в такой настройке вы хотите, чтобы «конечная модель» была наименее среди всех моделей, так же, как вы хотите «начальная теория», допускающая все модели. Терминальная (ака тривиальная) модель - это функтор, который отправляет все в теории в пустые множества и отображает на пустое множество. Много очень приятных свойств появляются, когда у вас есть такие вещи. Но обратите внимание: для того, чтобы иметь такие вещи, вы должны иметь только экваториальные идентичности, а не «неточности». Такие теории называются Algebraic Theories.
Что все это связано с Haskell? Ну, мы можем думать о подписях типов в точности как подписи алгебраических теорий, а законы их - как уравнения таких теорий.И обычно это то, как используемые в Haskell типы классов и почему они были введены - в соответствии с такими ситуациями.
Но, конечно, у нас нет , для этого необходимо иметь любые законы, которые мы хотим. Но мы теряем всевозможные приятные свойства на этом пути - и часто на самом деле обнаруживаем, что неравномерность означает, что наша теория будет иметь очень мало моделей и со странной структурой, связанной с ними. Так как типы классов предназначены для захвата структуры между различными вещами, а так как неалгебраические теории стремятся исправить уникальные (иш) модели, то оказывается, что редко бывает, что мы хотели бы использовать отношения несоответствия в законах типов. И действительно, я не могу придумать ни одного примера, где я видел, как он появился.
Вот еще один способ подумать об этом - рассмотреть теорию с равенствами и неравномерностями, а затем устранить неравности. То, что по-прежнему допускает все предыдущие модели, но также может иметь кучу «непреднамеренных». Поэтому мы не получаем дополнительных аргументов в отношении переписывания - у нас есть только определенные модели, которые априори исключены. Кроме того, когда мы хотим исключить «непреднамеренные» модели, это обычно происходит потому, что мы хотим исправить конкретную «предназначенную». И если мы хотим исправить определенную предполагаемую модель, возникает вопрос сразу: почему бы просто не использовать эту конкретную структуру, а не более общую модель?
«Я понимаю, что неравенство может быть выражено как равенство со свободной переменной, т. Е.« A> b = a + k = b' ». Как правило, это невозможно. Даже в этом случае он работает только в том случае, если в вашем домене указаны положительные числа. –
Как насчет '| a + k | = | b | 'then или' a + k = b || a - k = b'. но в любом случае этот аспект существенно влияет на точку в моем вопросе? (искренний вопрос) –
Все еще не работает, так как 'k' может быть 0. Для самого вопроса я могу просто сказать, что я не видел никаких примеров этого. –