haskell - 具有不包含等式/对称性但包含不等式/不对称性的定律的类型类

Question

我遇到的所有类型类，我认为都有通过指定方程来建立对称性的定律。我想知道是否有任何突出的理论甚至实际例子来建立不对称性，即需要缺乏对称性的类型类？通过例如指定 <expr1> /= <expr2>或 < , 或 not somePredicate(a, b) .

我知道不等式可以表示为具有自由变量的等式，即 a > b = a + k = b等等，但我认为引入自由变量本身可能与我强制不对称的想法一致。

这种法律的(理论)应用是什么？是否有任何(可运行的)示例？

或者:如果这不能被认为是 Haskell 足以在 SO 上，这是否应该继续 CS或 CSTheory ?

Answer 1

一般而言，代数定律通常仅根据等式恒等式而非不等式来指定。考虑这个的观点是模型论。一个理论可以被认为是 1) 不同元数的符号集合，因此可以从它们构造句子(即元数 0 我们可能有数字序列，元数 1 我们有否定，而元数 2 我们可以有加法) 和 2) 一组方程，这些方程提供了从这些签名构建的句子之间的关系。

这让我们可以描述各种算术理论、群、环、模等。

现在，理论模型是一组数学对象(数字、函数等)到签名元素的具体分配，以便将句子转换为模型元素时遵守这些等式。

在分类上，我们经常将理论视为由签名生成的所有可能句子的特殊类别。此类别中的箭头是含义——可以通过应用等式恒等式从其他人生成的句子。这反过来又导致在应用等式恒等式下所有相同的句子之间的等价(这产生了“生成器和关系”方法)。反过来，模型只是从该理论到任何其他类别的仿函数，尽管通常是 Set .

这在语法和语义之间产生了非常好的附属。你想要建模的句子集合越大，你能得到的模型就越少，你拥有的模型越多，所有这些都满足的句子集就越小。 (这里我只是勾勒出这个想法，而不是填写许多重要的细节)。

在任何情况下，人们往往忽略的一个后果，但真正有返回的是，在这种情况下，您需要一个“终端模型”，它是所有模型中最少的，就像您想要“初始理论”一样这承认所有模型。终端(又名平凡)模型是将理论中的所有内容发送到空集并映射到空集的仿函数。当您拥有这些东西时，就会出现许多非常好的属性。但请注意——要拥有这样的东西，你必须只有等式的身份，而不是“不同身份”。这样的理论被称为Algebraic Theories.

这一切与 Haskell 有什么关系？好吧，我们可以将类型类的签名视为代数理论的签名，而将它们的定律视为此类理论的方程。这就是 Haskell 中类型类的使用方式以及引入它们的原因——以适应这些情况。

但当然我们不必这样做——我们可以拥有我们想要的任何法律。但是我们在此过程中失去了各种很好的属性——而且实际上经常发现不等式意味着我们的理论将只有很少的模型，并且以奇怪的结构将它们联系起来。由于类型类旨在捕获各种事物之间的共同结构，并且由于非代数理论倾向于修复独特的(ish)模型，因此我们很少会希望在类型类定律中使用不等式关系。事实上，我想不出任何我见过它出现的例子。

这是另一种思考方式——考虑一个既有等式也有不等式的理论，然后消除不等式。剩下的仍然承认所有先前的模型，但也可能有一堆“非预期”的模型。因此，我们不会在重写方面获得额外的推理——我们只是先验排除了某些模型。此外，当人们希望排除“非预期”模型时，这通常是因为我们想要修复特定的“预期”模型。如果我们想修复一个特定的预期模型，问题就会立即出现——为什么不使用那个具体的结构，而不是更通用的类型类？