9

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

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

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

从我在 Wikipedia 上阅读的内容来看，这似乎Fix不是 Hindley Milner 类型系统中的有效类型构造函数，因为 HM 中的所有类型变量都必须是具体的（即必须具有 kind *）。真的是这样吗？如果 HM 中的类型变量并不总是具体的，那么 HM 会变得不可判定吗？

4

2 回答 2

6

重要的是类型构造函数是形成一阶术语语言（没有类型构造函数表达式的归约行为）还是高阶语言（在类型级别具有 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，在其他情况下，没有最通用的统一符。

于 2016-05-06T07:10:30.070 回答
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 }

可是等等！以上是不正确的，因为 egf Int ~ Either Bool Int必须统一 when 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 在下面指出的那样。）

于 2016-05-06T07:50:44.263 回答