在 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 解决，在其他情况下，没有最通用的统一器。

Answer 2

更高种类超出了基本的 Hindley-Milner 类型系统，但它们可以用相同的方式处理。

非常粗略地说，HM 解析表达式的语法树，将一个自由类型变量关联到每个子表达式，并根据类型规则生成一组涉及类型变量的类型项的等式约束。可以使用更高种类来完成相同的操作。

然后，通过统一解决约束。统一算法中一个典型的步骤是（后面是伪haskell）

(F t1 ... tn := G s1 ... sk) =
  | n/=k || F/=G  -> fail
  | otherwise     -> { t1 := s1 , ... , tn := sn }

（注意这只是统一算法的部分。）

上方F、G是类型构造函数符号，不是变量。在更高种类的统一中，我们需要考虑 F、G 也是变量。我们可以试试下面的规则：

(f t1 ... tn := g s1 ... sk) =
  | n/=k          -> fail
  | otherwise     -> { f := g , t1 := s1 , ... , tn := sn }

但是等等！以上是不正确的，因为例如f Int ~ Either Bool Int必须在f ~ Either Bool时统一。因此，我们还需要考虑 n/=k 的情况。一般来说，一个简单的规则集是

(f t := g s) =
  { f := g , t := s }
(F := G) =      -- rule for atomic terms
  | F /= G    -> fail
  | otherwise -> {}

（同样，这只是统一算法的部分。其他情况也必须处理，正如 Andreas Rossberg 在下面指出的那样。）

在 Hindley Milner 类型系统中，我们可以在构造函数位置设置类型变量吗？

Can we have type variables in constructor position in the Hindley Milner type system?

haskell

functional-programming

ocaml

type-inference

hindley-milner