首页 文章

在Hindley-Milner中```推论

提问于
浏览 次
1

我试图通过在我经常使用的语言Clojure中实现算法W来自学Hindley-Milner类型推断 . 我遇到了 let 推理的问题，我做错了，或者如果我期望的结果需要算法以外的东西 .

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

\a -> let b = a in b + 1

我明白了：

Num a => t -> a

但我应该得到这个：

Num a => a -> a

同样，我实际上是在Clojure中这样做，但我不相信问题是Clojure特有的，所以我使用Haskell表示法使它更清晰 . 当我在Haskell中尝试它时，我得到了预期的结果 .

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

\a -> (\b -> b + 1) a

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

EDIT

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

然后我将 TypeEnv 函数直接翻译成Clojure，如下所示： (ftv (vals env)) . 由于我已将 ftv 实现为 cond 表单并且没有 seq 的子句，因此它只返回 nil 为 (vals env) . 这当然正是静态类型系统设计要捕获的那种错误！无论如何，我刚刚将 ftv 中关于 env Map 的子句重新定义为 (reduce set/union #{} (map ftv (vals env))) 并且它有效 .

haskell clojure hindley-milner

1 回答

  • 6

    很难说出什么是错的，但我猜你的概括是错误的 .

    我们手动输入术语 .

    \a -> let b = a in b + 1

    首先，我们将 a 与一个新的类型变量关联起来，比如 a :: t0 .

    然后我们输入 b = a . 我们也得到 b :: t0 .

    但是，这是关键点，我们不应该将 b 的类型概括为 b :: forall t0. t0 . 这是因为我们只能概括在环境中不存在的tyvar：在这里，我们确实在环境中有 t0 ，因为 a :: t0 就在那里 .

    如果你对它进行概括，你会得到一种类似于 b 的通用类型 . 然后 b+1 变为 b+1 :: forall t0. Num t0 => t0 ，并且整个术语获得 forall t0 t1. Num t1 => t0 -> t1 ，因为 a 和 b 的类型不相关（ t0 ，一旦被推广，可以被alpha转换为 t1 ） .

    回复于

相关问题