jkc*_*rea 27 functional-programming type-inference ml sml hindley-milner
曾经有人在SML中向我展示了一个小技巧,他们在他们的REPL中写出了大约3或4个函数,最后一个值的结果类型非常长(就像许多页面滚动一样长).
有谁知道什么代码生成这么长的类型,或者是否有这种行为的名称？
And*_*erg 43
如果以正确的方式组合,则由Hindley/Milner类型推断推断出的类型可能会成倍增长.例如:
fun f x = (x, x, x)
val t = f (f (f (f (f 0))))
这里t是一个嵌套的三元组,其嵌套深度对应于调用的数量n f.因此,整体类型的大小为3 ^ n.
然而,这实际上不是最坏的情况,因为该类型具有规则结构并且可以在线性空间中有效地表示图形(因为在每个级别上,所有三种组成类型是相同的并且可以共享).
真正最糟糕的情况是使用多态实例化来打败这个:
fun f x y z = (x, y, z)
val p1 = (f, f, f)
val p2 = (p1, p1, p1)
val p3 = (p2, p2, p2)
在这种情况下,类型再次呈指数级大,但与上面不同,所有组成类型都是不同的新类型变量,因此即使图形表示也呈指数增长(以pN声明的数量).
所以,是的,Hindley/Milner式的推理是最坏情况的指数(在空间和时间上).然而,值得指出的是,指数情况只能在类型呈指数级变大的情况下发生 - 即在情况下,即使没有类型推断也无法实际表达.