Hindley-Milner is a restriction of System F, which allows more types but which requires annotations by the programmer.
我的问题是,系统 F 中可用但 Hindley Milner 中不可用的类型示例(类型推断)是什么?
(假设 System F 类型的推断已被证明是不可判定的)
最佳答案
Hindley/Milner 不支持更高级别的多态类型,即通用量词嵌套到某个更大类型中的类型(即任何一流多态性的概念)。
最简单的例子之一是:
f : (∀α. α → α) → int × string
f id = (id 4, id "boo")
众所周知,推断高阶多态性通常是不可判定的。类似的限制也适用于递归:递归定义不能具有多态递归用途。举一个人为的例子:
g : ∀α. int × α → int
g (n,x) = if n = 0 then 0 else if odd n then g (n-1, 3) else g (n-1, "boo")
考虑到上述情况,这并不奇怪,而且事实上,像上面这样的递归定义只是在多态类型上应用高阶 Y 组合器的简写,这再次需要(必然的)一流多态性.
关于types - 系统 F 中的类型示例在 Hindley Milner 类型推断中不可用,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/23995736/