haw*_*eye 8 types inference type-inference hindley-milner system-f
根据'什么是Hindley Milner',它说:
Hindley-Milner是System F的限制,它允许更多类型但需要程序员注释.
我的问题是,什么是系统F中可用的类型的例子,在Hindley Milner(类型推断)中不可用？
(假设系统F类型的推断已被证明是不可判定的)
And*_*erg 11
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组合子的简写,这将再次需要(不可预测的)第一类多态性.
是的,JB Wells在Typeability中已经证明系统F类型推断是不可判定的,并且系统F中的类型检查是等效且不可判定的.
HM类型系统仅允许在类型表达式的顶级上使用类型量词.更确切地说,HM区分类型,其中不能包含量词,和类型的模式:
type:= type variable | 类型→类型
type schema:= type | ∀α.类型架构
并且使用类型schemata键入多态表达式.
因此,任何在类型表达式中具有类型量词的类型(特别是在→的左侧部分内)都不能在HM类型系统中表达.
一个例子可以是教堂数字的输入.它们在系统F中的类型是??.(???)?(???),虽然这可以用HM表示,但我们不能表达教堂数字用作参数的类型.例如,如果定义教会数字的取幂
(?mn.nm) : (??.(???)?(???)) ? (??.(???)?(???)) ? (??.(???)?(???))
由于参数中的类型量词,因此不能在HM类型系统中表示此类型.