我遇到过的所有类型类，我认为都有通过指定方程式建立对称性的定律。我想知道是否有建立类型不对称的类型类的突出理论或实际例子，即那些要求不对称的类型类？通过例如指定<expr1> /= <expr2>或<或not somePredicate(a, b)。
我知道不等式可以表示为与自由变量相等，即a > b = a + k = b等，但是我认为引入自由变量本身可能与我的强制不对称性思想相符。
这种法律的（理论）应用是什么？并且有任何（可运行的）示例吗？
或者：如果不能认为Haskell足以满足SO要求，那么应该在CS或CSTheory上执行吗？
最佳答案
通常，代数定律通常仅根据等式确定，而不是不等式。考虑这一点的观点是模型理论。可以将一种理论视为：1）不同arities的符号集合，以便可以从它们中构造句子（即arity 0时我们可能具有数字序列，arity 1时我们有否定，而arity则我们有2个。有加法）和2）一组方程式，这些方程式提供了由此类签名构成的句子之间的关系。
这使我们能够描述各种算术理论，组，环，模块等。
现在，理论模型是一组数学对象（数字，函数等）对签名元素的具体分配，因此将句子转换为模型元素时，这些方程式就得到了体现。
从类别上讲，我们经常将理论视为签名所产生的所有可能句子的一种特殊类别。此类别中的箭头是暗示–可以通过使用等式恒等从其他句子中生成的句子。反过来，在等式恒等式的应用下，所有句子之间的等效性相同（这产生了“生成器和关系”方法）。反过来，模型通常只是从该理论到任何其他类别的函数，尽管通常是Set。
这在语法和语义之间产生了很好的搭配。要建模的句子集合越多，可获得的模型越少，而模型越多，则所有句子都将满足的句子集越小。 （这里我只是勾勒出这个想法，而不是填写很多重要的细节）。
在任何情况下，人们倾向于忽略但确实有回报的一个结果是，在这种情况下，您需要一个“终端模型”，该模型是所有模型中最少的，就像您想要一个“初始理论”一样。承认所有模型。终极模型（也称为平凡模型）是函子，它将理论上的所有内容发送到空集并映射到空集。当您拥有此类属性时，就会出现许多非常好的属性。但请注意，要拥有这种东西，您必须仅具有方程式恒等式，而不能具有“恒等式”。这样的理论称为Algebraic Theories.
这与Haskell有什么关系？好吧，我们可以将类型类的签名完全视为代数理论的签名，并将它们的定律视为此类理论的等式。通常，这就是在Haskell中使用类型类的方式，以及引入它们的原因-以适应此类情况。
但是，当然我们不必这样做-我们可以拥有所需的任何法律。但是，我们在此过程中失去了各种各样的好特性-实际上，经常发现不等式意味着我们的理论将只有很少的模型，并且具有与之相关的怪异结构。由于类型类旨在捕获各种事物之间的通用结构，并且非代数理论倾向于固定唯一的模型，因此事实证明，在类型类定律中使用不平等关系的情况很少见。的确，我想不出任何例子。
这是思考它的另一种方法-考虑一个同时具有平等和不平等的理论，然后消除不平等。仍然保留所有先前的模型，但也可能有许多“意外”模型。因此，我们不会在重写方面获得其他推理-我们只是拥有某些模型，这些模型已被排除在外。此外，当人们希望排除“意外”模型时，这通常是因为我们要修复特定的“意外”模型。而且，如果我们要修复特定的预期模型，则会立即出现问题-为什么不仅仅使用具体的结构，而不是使用更通用的类型类？