haskell - Haskell 类型检查的 Paterson 条件

Question

有人可以解释(或给我一些例子或过程)为什么这些条件对于终止 Haskell 中的实例解析过程是必要的吗？或者至少提供描述此算法的链接。

例如，我试图找到一些关于它的讲座，但我只能找到关于类型推断的内容，而没有找到这个实例解析过程。

我引用自Haskell User Guide

The rules are these:

1. The Paterson Conditions: for each class constraint (C t1 ... tn) in the context
   1. No type variable has more occurrences in the constraint than in the head
   2. The constraint has fewer constructors and variables (taken together and counting repetitions) than the head
   3. The constraint mentions no type functions. A type function application can in principle expand to a type of arbitrary size, and so are rejected out of hand
2. The Coverage Condition. For each functional dependency, ⟨tvs⟩left -> ⟨tvs⟩ right, of the class, every type variable in S(⟨tvs⟩right) must appear in S(⟨tvs⟩left), where S is the substitution mapping each type variable in the class declaration to the corresponding type in the instance head.

Answer 1

用于保证实例解析在 FlexibleInstances 扩展下终止的所谓“Paterson 条件”在论文 Understanding Functional Dependencies via Constraint Handling Rules 的第 5 章中有完整记录。 .不幸的是，讨论非常技术性和密集。

我们可以做一些更温和的解释，让我们直观地了解哪些实例是合法的；一段时间以来，我一直在努力解决这个问题，但没有成功。