【发布时间】：2019-02-21 09:17:23
【问题描述】：
有人可以解释（或给我一些例子或过程）为什么这些条件对于终止 Haskell 中的实例解析过程是必要的？或者至少是描述该算法的链接。
例如，我试图找一些关于它的讲座，但我只能找到关于类型推断的东西，而不是这个实例解析过程。
规则如下：
- 帕特森条件：对于上下文中的每个类约束
(C t1 ... tn)
- 没有类型变量在约束中的出现次数比在头部中的次数多
- 约束的构造函数和变量（合起来计算重复次数）比头部少
- 约束没有提到类型函数。类型函数应用程序原则上可以扩展为任意大小的类型，并且 所以被拒之门外
- 覆盖条件。对于类的每个函数依赖，
⟨tvs⟩left -> ⟨tvs⟩右，S(⟨tvs⟩right)中的每个类型变量都必须出现在S(⟨tvs⟩left)中，其中S是替换映射 类声明中的每个类型变量对应的类型 在实例头中。
【问题讨论】：
-
我认为这些条件不是必要，而是足够，即它们意味着终止。您可以编写一组违反 Paterson 条件的实例，但它们会导致终止。此外，考虑迁移到 StackOverflow 以获得更多可见性：那里的 Haskell 社区（包括我自己）经常处理此类问题。
-
确实有人提议用更好的条件替换它们github.com/ghc-proposals/ghc-proposals/pull/114
-
“关于它的讲座”是从用户指南链接的论文：“通过约束处理规则理解 ...”。没有更简单的详细解释。你引用的措辞很清楚，不是吗？您可以使用
UndecidableInstances关闭条件。然后正如@chi 所说，类型推断可能会终止。 （GHC 使用简单的堆栈深度限制来避免无限循环。）有条件确保上下文中的每个约束（以及约束的上下文等）使问题更小。 -
@Li-yau Xia，是的，非常棒。 cmets中有很多例子和讨论。操作“我只能找到关于类型推断的东西”：实例解析就是类型推断；类型推断需要实例解析；因为解析到实例然后使用功能依赖项提供改进的类型。
标签： haskell type-inference type-resolution