标签: hindley-milner

我发誓曾经有一件T恤出售,上面写着不朽的话:

什么部分

你不明白吗？

就我而言,答案就是......全部!

特别是,我经常在Haskell论文中看到这样的符号,但我不知道它的含义是什么.我不知道它应该是什么样的数学分支.

我当然认识到希腊字母的字母,以及诸如"∉"之类的符号(通常意味着某些东西不是一组的元素).

另一方面,我以前从未见过"⊢"(维基百科称它可能意味着"分区").我也不熟悉这里使用的vinculum.(通常它表示一个级分,但是这并不出现在这里是这种情况.)

如果有人至少可以告诉我从哪里开始想要理解这个符号海洋的含义,那将会有所帮助.

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

我看过以下帖子:

• Steve Yegge - 动态语言反击
• Steve Yegge - Pinocchio问题
• Daniel Spiewak - 什么是Hindley-Milner？(为什么它很酷？)

但是维基百科中没有单一的条目,通常会给我一个简明的解释.
^{注意 - 现在添加了一个}

它是什么？
哪些语言和工具实现或使用它？
你能提供一个简明的答案吗？

阅读Scala类型系统与Haskell的缺点？我不得不问:具体来说,它使Haskell的类型系统比其他语言的类型系统(C,C++,Java)更强大.显然,即使Scala也不能执行与Haskell类型系统相同的功能.具体来说,是什么让Haskell的类型系统(Hindley-Milner类型推断)如此强大？你能给我举个例子吗？

此代码编译：

#[derive(Debug, Default)]
struct Example;

impl Example {
    fn some_method(&self) {}
}

fn reproduction() -> Example {
    let example = Default::default();
    // example.some_method();
    example
}

如果添加了注释行，则会导致错误：

#[derive(Debug, Default)]
struct Example;

impl Example {
    fn some_method(&self) {}
}

fn reproduction() -> Example {
    let example = Default::default();
    // example.some_method();
    example
}

为什么添加此方法调用会导致类型推断失败？

我看过以下两个问题：

• Rust的类型推断如何在多个语句之间起作用？
• Rust如何从From :: <> :: from（）推断结果类型？

从他们那里，我知道Rust使用的是Hindley-Milner 的（修改的）版本。后一个问题的答案将Rust的类型推论描述为一个方程系统。另一个答案明确指出“ Rust中的类型信息可以倒流”。

使用适用于这种情况的知识，我们可以：

1. example 是类型 ?E
2. ?E 必须有一个称为 some_method
3. ?E 返回
4. 返回类型为 Example

向后工作，很容易使人看到?E …

曾经有人在SML中向我展示了一个小技巧,他们在他们的REPL中写出了大约3或4个函数,最后一个值的结果类型非常长(就像许多页面滚动一样长).

有谁知道什么代码生成这么长的类型,或者是否有这种行为的名称？

在Andrew Koenig的关于ML类型推理的轶事中,作者使用合并排序的实现作为ML的学习练习,并且很高兴地发现"不正确"的类型推断.

令我惊讶的是,编译器报告了一种类型

'a list -> int list

Run Code Online (Sandbox Code Playgroud)

换句话说,这个sort函数接受任何类型的列表并返回一个整数列表.

那是不可能的.输出必须是输入的排列; 它怎么可能有不同的类型？读者肯定会发现我的第一个冲动:我想知道我是否在编译器中发现了一个错误!

在考虑了一些之后,我意识到还有另一种方法可以忽略它的论点:也许它根本没有返回.实际上,当我尝试它时,这正是发生的事情:sort(nil)确实返回nil,但排序任何非空列表将进入无限递归循环.

当翻译成Haskell时

split [] = ([], [])
split [x] = ([x], [])
split (x:y:xs) = (x:s1, y:s2)
  where (s1,s2) = split xs

merge xs [] = xs
merge [] ys = ys
merge xx@(x:xs) yy@(y:ys)
  | x < y     = x : merge xs yy
  | otherwise = y : merge xx ys

mergesort [] = []
mergesort xs = merge …

类型推断的限制是什么？哪种类型的系统没有通用的推理算法？

我正在寻找有关着名的Damas-Hindley-Milner算法的信息, 以便对函数式语言进行类型推断,尤其是有关实现的信息.

我已经知道如何做算法W,但我听说最近基于约束生成器/求解器的新算法而不是通常的统一.但是,我无法找到有关这些新算法实现的任何讨论.

我知道在哪里可以找到有关ML推理的部分信息吗？

我正在阅读有关Hindley-Milner Type Inference的维基百科文章,试图从中找出一些意义.到目前为止,这是我所理解的:

1. 类型分为单型或多型.
2. Monotype进一步分为类型常量(如int或string)或类型变量(如?和?).
3. 类型常量可以是具体类型(如int和string)或类型构造函数(如Map和Set).
4. 类型变量(如?和?)表现为具体类型(如int和string)的占位符.

现在我在理解多类型方面遇到了一些困难,但在学习了一些Haskell之后,我就是这样做的:

1. 类型本身有类型.正式类型的类型称为种类(即,存在不同类型的类型).
2. 具体类型(如int和string)和类型变量(如?和?)都是实物*.
3. 类型构造函数(如Map和Set)是类型的lambda抽象(例如Set,种类* -> *和Map类型* -> * -> *).

我不明白的是限定词表示什么.例如,什么??.?代表？我似乎无法做出它的正面或反面,我阅读下面的段落越多,我得到的就越混乱:

相反,具有多型∀α.α - >α的函数可以将相同类型的任何值映射到其自身,并且该同一性函数是该类型的值.另一个例子是∀α.(Setα) - > int是将所有有限集映射到整数的函数的类型.成员数是此类型的值.注意,限定符只能出现在顶级,即类型 …

请考虑以下示例:

非递归函数

 f x = x
 g y = f 'A'

GHC推断 f :: a -> a

相互递归函数

 f x = const x g
 g y = f 'A'

现在GHC推断f :: Char -> Char,即使类型可能a -> a只是在前一种情况下.

多态递归

 data FullTree a = Leaf | Bin a (FullTree (a, a))

 size :: FullTree a -> Int
 size Leaf = 0
 size (Bin _ t) = 1 + 2 * size t

size除非给出明确的类型,否则GHC无法推断出类型.

因此,看起来Haskell(GHC)不使用多态递归(如Alan Mycroft中描述的:多态类型方案和递归定义 …