haskell - 我们可以在 Hindley Milner 类型系统的构造函数位置有类型变量吗？

Question

在 Haskell 中，我们可以编写以下数据类型:

data Fix f = Fix { unFix :: f (Fix f) }

类型变量 f有种 * -> * (即它是一个未知类型的构造函数)。因此， Fix有种 (* -> *) -> * .我想知道是否 Fix是 Hindley Milner 类型系统中的有效类型构造函数。

从我 read on Wikipedia ，似乎 Fix不是 Hindley Milner 类型系统中的有效类型构造函数，因为 HM 中的所有类型变量都必须是具体的(即必须具有类型 * )。真的是这样吗？如果 HM 中的类型变量并不总是具体的，那么 HM 会变得不可判定吗？

Answer 1

重要的是类型构造函数是形成一阶术语语言(没有类型构造函数表达式的归约行为)还是高阶语言(在类型级别具有 lambda 或类似构造)。

在前一种情况下，Fix 产生的约束总是以最一般的方式统一(假设我们坚持 HM)。在每个 c a b ~ t方程，t必须解析为与 c a b 形状相同的具体类型应用程序表达式, 自 c a b不可能简化为其他表达方式。更高种类的参数不是问题，因为它们也只是以静态方式坐在那里，例如 c [] ~ c f由 f = [] 解决.

在后一种情况下，c a b ~ t可能或可能无法解决。在某些情况下，它可以通过 c = \a b -> t 解决，在其他情况下，没有最通用的统一符。