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

Question

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

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

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

从我在维基百科上看到的内容来看,它似乎Fix不是Hindley Milner类型系统中的有效类型构造函数,因为HM中的所有类型变量必须是具体的(即必须具有类型*).确实如此吗？如果HM中的类型变量并不总是具体,那么HM会变得不可判断吗？

Answer 1

重要的是类型构造函数是否形成一阶术语(没有类型构造函数表达式的约简行为)或更高阶的语言(在类型级别使用lambdas或类似结构).

在前一种情况下,产生的约束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,在其他情况下,没有最通用的统一者.