问题标签 [hindley-milner]

这个块给

错误：

我想知道let表达式中元组类型检查背后的算法。当左侧有一个变量时，我知道 Hindley-Milney 类型检查算法。我想知道在元组/列表等情况下是否有任何特殊算法。

我正在研究一些秒差距代码。在脚本的底部，有一个 parseFromFile 调用，其中 ParseFromFile 来自 Text.Parsec.String

如果我将此注释掉，我的代码将不再编译，并且会出现许多模棱两可的类型错误：

在流的严格形式和惰性形式之间存在歧义：

parseFromFile 必须消除类型推断的歧义。解决这种歧义的正确方法是什么？包括 parseFromFile 调用将使它编译，但我不想为了这个目的而必须调用它。我可以键入注释所有组合器代码，但这很乱。

我想使用该unification-fd包为 Hindley-Milner 类型系统实现一个简单的类型检查器。这需要多态（“forall”）类型的表示。

表示这些类型的最佳方式是什么？提供的变量unification-fd，即这些UVar东西，是用于统一（元）变量，而不是用于对象语言中的变量。我考虑过的一些可能性：

1. 将类型变量的构造函数添加到表示类型的基本函子中：

   只有zipMatch 统一等于TVars。类型实例化始终将 every 替换UTerm (TVar a)为freeVar.

2. (Ab) 使用s 表示类型变量，并在实例化时UVar将其替换为s。freeVar需要跟踪通用与存在UVar的 s 以了解要替换哪些。

3. 在类型检查期间对单态类型、从外部可见的多态类型以及在对中间绑定变量TVar进行类型检查期间TyF，不使用 , 单独使用。UTerm (TyF tcon) IntVarUTerm (TyF tcon) tvUTerm (TyF tcon) (Either tv IntVar)let

哪个最好？还有其他我没有想到的方法吗？

在 Haskell 中，我们可以编写以下数据类型：

类型变量f有种类* -> *（即它是一个未知的类型构造函数）。因此，Fix有种(* -> *) -> *。我想知道FixHindley Milner 类型系统中是否是有效的类型构造函数。

从我在 Wikipedia 上阅读的内容来看，这似乎Fix不是 Hindley Milner 类型系统中的有效类型构造函数，因为 HM 中的所有类型变量都必须是具体的（即必须具有 kind *）。真的是这样吗？如果 HM 中的类型变量并不总是具体的，那么 HM 会变得不可判定吗？

鉴于这两个程序（用 JavaScript 编写）......

我的问题是如何在不引用实现的情况下推导出comp2的Hindley-Milner 类型 comp

如果我们知道comp的实现，就很容易了……我们可以通过整个求值使用替换模型来得出扩展表达式……

叮叮当当。扩展评估匹配comp2的类型。没有人印象深刻。

但是如果我们只知道它comp的类型而不知道它的实现呢？除了评估代码来确定类型，我是否可以对 ' 的类型执行某种替换/评估comp以最终得到comp2' 的类型？

仅考虑到这一点，问题就变得更加困难……（至少对我而言）

总有办法吧？这不就是代数数据类型的全部意义吗？

让我们看一个简化的例子来澄清我的问题：如果我们有一个类似addand的函数map......

如果我们想定义一个函数 usingmap并且我们可以在不知道or的实现的情况下系统地add找出类型 addmap

这真的很强大，因为它允许您推理您没有编写的代码，而无需深入研究实现（尽可能多）

然而，当试图用这个comp2例子来做这件事时，我很快就被卡住了

HINDLEY MILNER 如何

如果我正确理解 Haskell 中的 ST monad，runST请以巧妙的方式使用 rank-2 类型，以确保在转义 monad 时计算不会引用任何其他线程。

我有一个带有 Hindley-Milner 类型系统的玩具语言，我的问题如下：是否可以使用用于键入应用程序的临时规则扩展 HM 类型系统，runST以便 ST monad 可以安全地逃避，而无需引入等级-2 种？

更准确地说，runST将具有类型forall s a. ST s a -> a（即 rank-1）并且类型化规则将首先尝试以与 HM 在 let 表达式中泛化类型相同的方式泛化计算类型，但如果s发现类型变量被绑定，则会引发类型错误.

与香草 HM 相比，上述内容仅限制了可接受的程序，所以看起来不错，但我不确定。这行得通吗？

在仿射类型系统中，资源最多只能使用一次。

从 Hindley-Milner 类型系统开始，似乎一个简单的方法来强制关联是在使用变量的类型规则时从当前类型上下文中简单地删除一个变量（正如LinearML 上的这些幻灯片所建议的，第 15 页）。

这就是执行亲和力的全部内容吗？还是有什么更复杂的事情要做？

我公开了一个带有两个参数的函数，一个是最小界限，另一个是最大界限。如何使用类型确保例如最小界限不大于最大界限？

我想避免创建一个智能构造函数并返回一个 Maybe，因为它会使整个使用变得更加麻烦。

谢谢

抽象语法树中存在哪些类型信息？AST 如何用于类型推断？当没有节点指示具体类型时，我不明白如何在给定 AST 的情况下派生类型输入和输出。是否仅从树结构推断出类型？例如有一堆IfStatement(Statement)，所以它可能返回一个布尔值？例如，javalang python 模块使用这些 AST 节点：

给定一些玩具代码，它会为函数输出以下 AST：

另外，如果有人可以指出一些关于给定 AST 的类型推断的优秀阅读材料。谢谢。

我读过 Rust 使用 Hindley-Milner 具有非常好的类型推断。Rust 也有可变变量，并且当 HM 算法与可变性一起工作时，AFAIK 必须有一些约束，因为它可能过度概括。以下代码：

不编译，因为在第二行推断出整数并且不能将浮点值分配给整数变量。所以我猜测对于简单的变量，一旦推断出非泛型类型，该变量就会变成单类型并且不能再被泛化。

但是像 Vec 这样的模板呢？例如这段代码：

这再次失败，但最后一行再次失败。这意味着第二行部分推断出类型（Vec），第三行推断出容器类型。

有什么规律？是否有我不知道的价值限制之类的东西？还是我把事情复杂化了，而 Rust 有更严格的规则（就像根本没有概括一样）？