什么是欣德利米尔纳？ [英] What is Hindley-Milner?

问题描述

我遇到了这个术语 Hindley-Milner ，我不确定是否掌握了它的含义。

我已阅读以下帖子：

• Steve Yegge - 动态语言反击


• Steve Yegge - 匹诺曹问题
>

• Daniel Spiewak - 什么是欣德利米尔纳？ （为什么它很酷？）

但是这个词在维基百科里没有单独的条目，一个简明的解释。

^{注意 - 一个 now now}

这是什么？

实现或使用哪些语言和工具


您能否提供一个简洁的答案？

解决方案

Hindley-Milner是类型系统，由Roger Hindley（他正在研究逻辑）和后来的Robin Milner（他正在研究编程语言）独立发现。 Hindley-Milner的优势在于它支持多态功能;它支持多态功能; 例如，一个函数可以为列表的长度提供独立于元素类型的列表长度，或者函数执行与存储在树中的键类型无关的二叉树查找。

有时函数或值可以有多于一个类型，如长度函数的示例：它可以是整数列表整数，字符串到整数的列表，成对的列表到整数等等。在这种情况下，Hindley-Milner系统的信号优势是每个良好类型的术语都有一个独特的最佳类型，它被称为主体类型。列表长度函数的主要类型是对于任何 a ，从 a 到整数列表中的函数。这里 a 是一个所谓的类型参数，它在lambda演算中是显式的，但在大多数编程语言中是隐含的。类型参数的使用解释了为什么Hindley-Milner是一个实现 参数多态性的系统。 （如果你在ML中编写了一个长度函数的定义，你可以看到类型参数：

$ p $ func'a length [ ] = 0
|'a length（x :: xs）= 1 + length xs

一个词有Hindley-Milner类型，那么可以推断出主体类型，而不需要程序员的任何类型声明或其他注释。一个混合的祝福，因为任何人都可以证明谁曾经处理过大量的ML代码而没有注释。） > Hindley-Milner是几乎所有静态类型函数语言的类型系统的基础，这类常用语言包括：

• ML系列（标准ML 和 Objective Caml ）


• Haskell


• 清洁

所有这些语言都扩展了Hindley-Milner; Haskell，Clean和Objective Caml采用雄心勃勃且不同寻常的方式。 （需要扩展来处理可变变量，因为基本的Hindley-Milner可以被颠覆，例如，一个可变单元格包含一个未指定类型的值列表，这些问题由一个名为 value restriction 。）

许多其他基于类型函数语言的次要语言和工具都使用Hindley-Milner。

Hindley-Milner是系统F ，它允许更多的类型，但需要程序员注释。

I encountered this term Hindley-Milner, and I'm not sure if grasp what it means.

I've read the following posts:

• Steve Yegge - Dynamic Languages Strike Back
• Steve Yegge - The Pinocchio Problem
• Daniel Spiewak - What is Hindley-Milner? (and why is it cool?)

But there is no single entry for this term in wikipedia where usually offers me a concise explanation.
^{Note - one has now been added}

What is it?
What languages and tools implement or use it?
Would you please offer a concise answer?

解决方案

Hindley-Milner is a type system discovered independently by Roger Hindley (who was looking at logic) and later by Robin Milner (who was looking at programming languages). The advantages of Hindley-Milner are

• It supports polymorphic functions; for example, a function that can give you the length of the list independent of the type of the elements, or a function does a binary-tree lookup independent of the type of keys stored in the tree.

• Sometimes a function or value can have more than one type, as in the example of the length function: it can be "list of integers to integer", "list of strings to integer", "list of pairs to integer", and so on. In this case, a signal advantage of the Hindley-Milner system is that each well-typed term has a unique "best" type, which is called the principal type. The principal type of the list-length function is "for any a, function from list of a to integer". Here a is a so-called "type parameter," which is explicit in lambda calculus but implicit in most programming languages. The use of type parameters explains why Hindley-Milner is a system that implements parametric polymorphism. (If you write a definition of the length function in ML, you can see the type parameter thus:

   fun 'a length []      = 0
     | 'a length (x::xs) = 1 + length xs
  

• If a term has a Hindley-Milner type, then the principal type can be inferred without requiring any type declarations or other annotations by the programmer. (This is a mixed blessing, as anyone can attest who has ever been handled a large chunk of ML code with no annotations.)

Hindley-Milner is the basis for the type system of almost every statically typed functional language. Such languages in common use include

• The ML family (Standard ML and Objective Caml)
• Haskell
• Clean

All these languages have extended Hindley-Milner; Haskell, Clean, and Objective Caml do so in ambitious and unusual ways. (Extensions are required to deal with mutable variables, since basic Hindley-Milner can be subverted using, for example, a mutable cell holding a list of values of unspecified type. Such problems are dealt with by an extension called the value restriction.)

Many other minor languages and tools based on typed functional languages use Hindley-Milner.

Hindley-Milner is a restriction of System F, which allows more types but which requires annotations by the programmer.

这篇关于什么是欣德利米尔纳？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！