gpt4 book ai didi

functional-programming - 以 CS101 学生可以理解的方式描述 Damas-Milner 类型推理

转载 作者:行者123 更新时间:2023-12-04 02:06:31 27 4
gpt4 key购买 nike

Hindley-Milner 是一个类型系统,它是许多众所周知的函数式编程语言的类型系统的基础。 Damas-Milner 是一种在 Hindley-Milner 类型系统中推断(推导出?)类型的算法。

Wikipedia给出了算法的描述,据我所知,它只有一个词:“统一”。这就是全部吗?如果是这样,那意味着有趣的部分是类型系统本身而不是类型推断系统。

如果 Damas-Milner 不仅仅是统一,我想要对 Damas-Milner 的描述,其中包括一个简单的示例,理想情况下还有一些代码。

此外,该算法通常被称为进行类型推断。它真的是一个推理系统吗?我以为这只是推断类型。

相关问题:

  • What is Hindley Miller?
  • Type inference to unification problem
  • 最佳答案

    Damas Milner 只是对统一的结构化使用。

    当它递归到一个 lambda 表达式时,它构成了一个新的变量名。当您在子项中发现以需要给定类型的方式使用的变量时,它会记录该变量和该类型的统一。如果它试图将两种没有意义的类型统一起来,比如说一个单独的变量既是一个 Int 又是一个来自 a -> b 的函数,那么它会因为你做了坏事而对你大吼大叫。

    Also, this algorithm is often said to do type inference. Is it really an inference system? I thought it was only deducing the types.



    推断类型是类型推断。检查类型注释对于给定术语是否有效是类型检查。它们是不同的问题。

    If so, that means that the interesting part is the type system itself not the type inference system.



    人们通常说 Hindley-Milner 风格的字体系统是在一个尖顶上平衡的。如果添加更多功能,则无法推断类型。因此,可以在 Hindley-Milner 风格类型系统之上分层而不破坏其推理属性的类型系统扩展,确实是现代函数式语言的有趣部分。在某些情况下,我们混合类型推断和类型检查,例如在 Haskell 中,许多现代扩展无法推断,但可以检查,因此它们需要类型注释来实现高级功能,例如多态递归。

    关于functional-programming - 以 CS101 学生可以理解的方式描述 Damas-Milner 类型推理,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/1109509/

    27 4 0
    Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
    广告合作:1813099741@qq.com 6ren.com