问题标签 [hindley-milner]

在 C++ 中是否有Damas-Hindley-Milner风格类型推断的实现，最好使用现代 C++ 技术？

我记得在某处读到 Hindley Milner 是对 system-f 的限制。如果是这样的话，有人可以向我提供一些可以在 system-f 中输入但不能在 HM 中输入的术语。

我试图推断以下表达式的类型：

应该给出类型(a -> a) -> a

在使用自下而上算法（在泛化hindley-milner 类型推理算法中描述）并添加以下规则后：

我剩下以下类型：t1 -> t2

以及以下约束：

我看不出这些约束是如何解决的，所以我只剩下 type 了(a -> a) -> a。我希望有人能清楚地看到我是否出错了。

完整的源代码在这里

我正在尝试实现“自下而上”类型推理算法，该算法可在Generalizing Hindley-Milner Type Inference Algorithms中找到

第 6 页解释了隐式约束是如何产生的

t1应该是类型方案的一个实例，它是通过t2关于单态类型变量集的类型泛化获得的M

然而，在第 9 页，在解释如何对隐式约束应用替换时，有人告诉我对这组单态类型变量应用替换。问题是，如果我有替换[t1 := t2 -> t3]，则M不再是一组类型变量。

我在这里有什么误解？

在元编程时，将有关您的程序已知但在 Hindley-Milner 中无法推断的类型的信息传递给 Haskell 的类型系统可能是有用的（或必要的）。在 Haskell 中是否有一个库（或语言扩展等）提供了执行此操作的工具——即编程类型注释？

考虑一种情况，您正在使用异构列表（Data.Dynamic例如，使用库或存在量化实现）并且您希望将列表过滤为沼泽标准、同质类型的 Haskell 列表。你可以写一个函数

并使用手动类型注释调用它。例如，

这foo是清单[1, 2] :: [Int]；这工作得很好，你又回到了 Haskell 的类型系统可以做它的事情的坚实基础上。

现在想象你想做同样的事情，但是（a）在你编写代码时你不知道调用产生的列表的类型dynListToList需要是什么，但是（b）你的程序确实包含弄清楚这一点所需的信息，只有（c）它不是类型系统可以访问的形式。

例如，假设您从异构列表中随机选择了一个项目，并且您希望按该类型过滤列表。使用 提供的类型检查工具Data.Typeable，您的程序拥有执行此操作所需的所有信息，但据我所知——这是问题的本质——没有办法将其传递给类型系统。这是一些伪Haskell，说明了我的意思：

（假设randItem从列表中选择一个随机项目。）

的参数上没有类型注释return，编译器会告诉你它有一个“不明确的类型”并要求你提供一个。但是您不能提供手动类型注释，因为类型在写入时未知（并且可能会有所不同）；然而，该类型在运行时是已知的——尽管它是类型系统无法使用的形式（这里，所需的类型由 value tr, a表示TypeRep——Data.Typeable详情请参阅）。

伪代码:: [<tr>]是我想要发生的魔法。有没有办法以编程方式为类型系统提供类型信息？也就是说，程序中的值中包含类型信息？

基本上，我正在寻找一个具有（伪）类型的函数，??? -> TypeRep -> a它采用 Haskell 的类型系统未知的类型的值和 aTypeRep并说：“相信我，编译器，我知道我在做什么。这东西有价值以此为代表TypeRep。” （请注意，这不是什么unsafeCoerce。）

还是有什么完全不同的东西让我在同一个地方？例如，我可以想象一个允许分配给类型变量的语言扩展，例如启用范围类型变量的扩展的增强版本。

（如果这是不可能的或非常不切实际的——例如，它需要将一个完整的类似 GHCi 的解释器打包到可执行文件中——请尝试解释原因。）

我发誓曾经有一件T 恤出售，上面印着不朽的文字：

哪一部分

你不明白吗？

就我而言，答案是……全部！

特别是，我经常在 Haskell 论文中看到这样的符号，但我不知道它是什么意思。我不知道它应该是什么数学分支。

我当然认识希腊字母表中的字母和诸如“∉”之类的符号（这通常意味着某物不是集合的元素）。

另一方面，我以前从未见过“⊢”（维基百科声称它可能意味着“分区”）。我也不熟悉这里的 vinculum 的使用。（通常，它表示分数，但这里似乎并非如此。）

如果有人至少可以告诉我从哪里开始寻找理解这个符号海洋的含义，那将很有帮助。

PyPy 是否在编译时进行静态类型检查以在编译时捕获类型错误？如果不是，像 HM 类型推断这样的东西是否有助于在编译时捕获这些错误？

我正在阅读有关Hindley–Milner 类型推断的 Wikipedia 文章，试图从中理解。到目前为止，这是我所理解的：

1. 类型分为单型或多型。
2. Monotypes 进一步分为类型常量（如intor string）或类型变量（如αand β）。
3. 类型常量可以是具体类型（如intand string）或类型构造函数（如Mapand Set）。
4. 类型变量（如α和β）充当具体类型（如int和string）的占位符。

现在我在理解多型时有点困难，但是在学习了一点 Haskell 之后，这就是我所做的：

1. 类型本身也有类型。类型的正式类型称为种类（即有不同种类的类型）。
2. 具体类型（如int和string）和类型变量（如α和β）是 kind *。
3. 类型构造函数（如Map和Set）是类型的 lambda 抽象（例如Setis of kind* -> *和Mapis of kind * -> * -> *）。

我不明白的是限定词是什么意思。例如∀α.σ代表什么？我似乎无法对它做出正面或反面，我阅读以下段落的次数越多，我就越困惑：

相反，具有多型∀α.α -> α的函数可以将同一类型的任何值映射到自身，并且恒等函数是该类型的值。另一个例子∀α.(Set α) -> int是将所有有限集映射到整数的函数类型。成员计数是此类型的值。请注意，限定符只能出现在顶层，例如类型∀α.α -> ∀α.α被类型的语法排除，并且单型包含在多型中，因此类型具有一般形式∀α₁ 。. . ∀αₙ.τ。

I have a parameterized type that recursively uses itself but with a type parameter specialized and when I implement a generic operator, the type of that operator is bound too tightly because of the case that handles the specialized sub-tree. The first code sample shows the problem, and the second shows a workaround that I'd rather not use because the real code has quite a few more cases so duplicating code this way is a maintenance hazard.

Here's a minimal test case that shows the problem:

This modified version of Impl.map fixed the problem but introduces a maintenance hazard.

Is there any way to get this to work without duplicating the body of let rec map?

Applying gasche's solution yields the following working code:

我需要一种（快速而肮脏的）方法来获得以字符串形式给出的 Haskell 表达式类型的某种表示。

我目前看到 3 个选项：

• 使用 GHC API——然而，文档很快让我失去了兴趣。
• 使用其他类型推断工具——有人建议我尝试使用 haskell-type-exts，但除了最简单的表达式之外，它无法输入所有内容。我不知道任何其他这样的工具。
• 滚动我自己的 HM 推断器——除非绝对必要，否则我会避免这种情况

我什至不需要一个完整的解决方案，因为可以键入 Haskell 的合理基本子集的库/工具对我来说就足够了。

那么实现这一目标的最简单方法是什么？