compiler-construction - 如何推断强制？

Question

我想知道如何在类型推断期间推断强制转换(又名隐式转换)。我正在使用 Top Quality Type Error Messages 中描述的类型推断方案由 Bastiaan Heeren 撰写，但我认为所有 Hindley-Milner 式方法的总体思路可能相同。

似乎强制可以被视为一种重载形式，但是本文中描述的重载方法并没有考虑(至少不是我可以遵循的方式)基于上下文对返回类型的要求的重载，这是强制执行的必要条件。我还担心这种方法可能会使优先考虑身份强制以及尊重强制的传递闭包变得困难。我可以看到将每个强制表达式加糖，例如 e，以 coerce(e)，但将它加糖到 coerce(coerce(coerce(... coerce(e) ...))) 的某个深度等于强制的最大嵌套看起来很愚蠢，并且还将强制关系限制为具有有限传递闭包的事物，其深度与上下文无关，这似乎(不必要？)有限制。

Answer 1

我希望你能得到一些好的答案。

我还没有读过你链接到的论文，但听起来很有趣。你有没有研究过在 Haskell 中临时多态性(基本上是重载)是如何工作的？ Haskell 的类型系统是 H-M 加上其他一些好东西。这些好东西之一是类型类。类型类提供重载，或者如 Haskeller 所说的，即点多态。

在 GHC(最广泛使用的 Haskell 编译器)中，类型类是通过在运行时传递字典来实现的。字典让运行时系统进行从类型到实现的查找。据说，jhc可以使用 super 优化在编译时选择正确的实现，但我怀疑它处理 Haskell 可以允许的完全多态的情况，我知道没有正式的证明或论文断言正确性。

听起来您的类型推断会遇到与其他 rank-n 多态方法相同的问题。您可能想在这里阅读一些论文以获取更多背景信息:Scroll down to "Papers about types"他的论文是特定于 Haskell 的，但类型理论的东西对你来说应该是有意义和有用的。

我认为这篇关于 rank-n 多态性和类型检查问题的论文应该会给你带来一些有趣的想法:http://research.microsoft.com/~simonpj/papers/higher-rank/

我希望我能提供更好的答案!祝你好运。