问题标签 [hindley-milner]

我试图通过用我常用的语言 Clojure 实现算法 W 来自学 Hindley-Milner 类型推断。我遇到了let推理问题，我不确定我是否做错了什么，或者我期望的结果是否需要算法之外的东西。

基本上，使用 Haskell 表示法，如果我尝试推断它的类型：

我明白了：

但我应该得到这个：

同样，我实际上是在 Clojure 中执行此操作，但我认为问题不是 Clojure 特有的，因此我使用 Haskell 表示法使其更清晰。当我在 Haskell 中尝试时，我得到了预期的结果。

无论如何，我可以通过将 every 转换为函数应用程序来解决该特定问题let，例如：

但后来我失去了let多态性。由于我对 HM 没有任何先验知识，我的问题是我是否在这里遗漏了什么，或者这只是算法的工作方式。

编辑

如果有人有类似的问题并想知道我是如何解决的，我会按照Algorith W Step By Step进行操作。在第 2 页的底部，它说“将Types方法扩展到列表有时会很有用。” 因为这听起来对我来说不是强制性的，所以我决定跳过那部分，稍后再重新审视。

然后我将ftv函数 forTypeEnv直接翻译成 Clojure，如下所示(ftv (vals env))：由于我已经实现ftv为cond表单并且没有seqs 的子句，所以它只是返回nil了(vals env). 这当然正是静态类型系统旨在捕获的那种错误！无论如何，我只是重新定义了与地图ftv相关的条款，并且它有效。env(reduce set/union #{} (map ftv (vals env)))

GHC 说我的函数太笼统而不能作为参数传递。

这是重现错误的简化版本：

这就是错误所说的：

编译器希望我的类型签名更具体，但我不能，因为我需要将参数函数与不同类型的参数一起使用。就像在我的示例中一样，我将它传递给 anAction IO ()和 an Action IO String。

如果我像编译器询问的那样用错误替换调用，(Action IO a -> IO a) -> String -> IO ()因为它输出一个.(Action IO () -> IO ()) -> String -> IO ()readFileIO String

为什么会发生这种情况，我应该怎么做才能将此函数作为参数传递？

我知道如果我只是runAction在我的actionFile函数中使用一切都会正常工作，但在我的真实代码runAction中是一个部分应用的函数，它是从 IO 计算的结果构建的，所以它在编译时不可用。

我希望能够使用定点数据类型和递归方案来制定hindley-milner 类型推理算法。忽略除实际递归部分之外的所有细节：

env该算法在递归遍历树直到到达叶子时构建环境数据结构。然后它在再次构建结果时使用此信息。

如果没有这env部分，这可以很容易地用cata. 这（与env）一般可以使用递归方案来完成吗？

我们有一个 AST 定义：

以及用于类型推断的 F 代数：

我们可以使用以下方法获得运行推理的结果cata：

但是现在我希望结果是带有每个表达式的类型信息注释的原始 AST，所以现在infer' :: Fix Term -> Wrapped (Labeled Term Type)。

1. 我应该使用什么数据结构来注释树（Cofree, Product,Fix带有自定义Label）？
2. 如何在不修改原始w函数的情况下使用递归方案实现这一点？

我目前正在使用 haskell 构建服务器，作为语言的新手，我想尝试一种新的方法 zu Monad 组合。这个想法是我们可以编写库方法，例如

在不知道底层单子的情况下工作。当然，在这个例子中，让 isGetRequest 直接在 (RequestSupport r) monad 上运行就足够了，但我的想法是我的库也可能对 monad 有多个约束。然而，我不想在同一个模块中实现所有这些不同的关注点，也不想将它们分散到不同的模块（孤儿实例！）。这就是为什么 m monad 只实现Supports*类，将真正的关注点委托给其他 monad。

上面的代码应该可以完美运行（对 GHC 进行了一些语言扩展）。不幸的是，我在 CRUD（创建读取更新删除）问题上遇到了一些问题：

不，我得到一个错误：

似乎类型检查器不喜欢该a参数不直接出现在liftCRUD的签名中。这是可以理解的，因为a不能从函数依赖中派生出来。

a我大脑中的类型检查器告诉我，稍后在库方法中执行有关 CRUD 的某些方法时，使用 AllowAmbiguousTypes推断类型应该不是问题。不幸的是，GHC 似乎无法执行此推理步骤，例如

产量

看来我仍然无法推理编译器。我有办法解决这个问题吗？或者至少是一种理解编译器能够推断出什么的方法？

最好的问候， bloxx

为什么是printf "%d\n" 3模棱两可而不是show 3？可以printf重写模块以提供自动消歧吗？大概类似的事情show必须在printf...的较低级别完成，或者和之间是否存在一些关键的区别printf，show这需要消除数字的歧义？

如果printf 可以重写以自动处理数字而无需明确消歧，那么什么是show正确的？如何在不消除歧义的show情况下将数字转换为字符串？:: Intprintf

这是show（没有任何歧义）的正确操作以及printf（有歧义）的正确操作：

这是不消除数字歧义时的歧义变量错误：printf

以下对 compose 函数的 Hindley-Milner 类型签名的尝试是否正确？

所以，我正在尝试编写自己的 Prelude 替代品，并且我已经 (^) 实现了这样的：

（请注意，这里使用的 Integral 是我定义的，而不是 Prelude 中的，尽管它是相似的。此外，它one是一个多态常数，它是 monoidal 操作下的恒等式。）

数字类型是幺半群，所以我可以尝试做，比如 2^3，但是类型检查器给了我：

我知道这是因为 Int 和 Integer 都是 Integral 类型，但是为什么在普通 Prelude 中我可以做到这一点呢？：

即使在我的部分应用程序的签名看起来相同？

我将如何使 2^3 实际上起作用，从而给出 8？

所以我最近才在玩具容量之外遇到了akka，我不禁注意到它和OTP共享动态类型，尽管scala一般偏爱静态类型。我开始深入研究，发现这篇 Wadler 论文描述了一个基于 erlang 进程间通信的 HM 类型系统。也就是说，SO 对这个问题的回答是指 Wadler 和 Marlow 未能交付他们对流程型通信所做的草图。作为参考，我对这样的代码很失望：

我知道在实践中，dialyzer 可以提供真实类型系统的很多好处，但是为什么创建静态验证的参与者系统如此困难呢？仅仅是我们在使用类型系统时倾向于编写Future或Observable/Iteratee库，或者-modeled IO 而不是 actor 系统，还是 Wadler 和 Marlow 遗漏了一个技术难题？Channel

我想导出以下应用于标识函数的人为应用程序的类型。为了实现这一点，我可能必须将第一个参数的类型部分(a -> [b])与以下类型统一id：

这显然是错误的，因为预期的类型是[b] -> [b]. 统一中存在歧义，因为除了 之外，a0不能同时a与 和等价。但是，告诉我用而不是相反的规则来代替，例如我必须这样做的规则是什么。[b]a ~ [b]a[b]ap :: ([a] -> b) -> [a] -> b

我知道这是一个非常具体的问题，抱歉。希望它不会太混乱！