use*_*807 11 functional-programming type-inference hindley-milner
Hindley-Milner是一种类型系统,是许多众所周知的函数式编程语言的类型系统的基础.Damas-Milner是一种在Hindley-Milner型系统中推断(推导？)类型的算法.
维基百科给出了算法的描述,据我所知,该算法相当于一个单词:"统一".这就是它的全部吗？如果是这样,那意味着有趣的部分是类型系统本身而不是类型推理系统.
如果Damas-Milner不仅仅是统一,我想要一个Damas-Milner的描述,其中包括一个简单的例子,理想情况下是一些代码.
此外,该算法通常被称为类型推断.它真的是一个推理系统吗？我认为这只是推断出类型.
相关问题:
Edw*_*ETT 11
Damas Milner只是统一的结构化使用.
当它递归到lambda表达式时,它组成一个新的变量名.当您在子项中找到以需要给定类型的方式使用的变量时,它会记录该变量和该类型的统一.如果它试图统一两个没有意义的类型,比如说一个单独的变量既是一个Int又是一个来自 - > b的函数,那么它就会因为做坏事而大吼大叫.
此外,该算法通常被称为类型推断.它真的是一个推理系统吗？我认为这只是推断出类型.
推导类型是类型推断.检查类型注释是否对给定术语有效是类型检查.他们是不同的问题.
如果是这样,那意味着有趣的部分是类型系统本身而不是类型推理系统.
人们普遍认为,Hindley-Milner风格的系统在风口浪尖上是平衡的.如果添加更多功能,则无法推断出类型.因此,键入系统扩展,您可以在Hindley-Milner样式类型系统之上进行分层而不破坏其推理属性,这实际上是现代函数式语言的有趣部分.在某些情况下,我们混合类型推断和类型检查,例如在Haskell中,很多现代扩展都无法推断,但可以检查,因此它们需要类型注释用于高级功能,如多态递归.
| 归档时间： |
|
| 查看次数： |
1761 次 |
| 最近记录： |