如何推断强制？

Question

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

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

Answer 1

您能否进一步澄清一下您要问的是什么？

我有一个小想法，如果我的想法是对的，那么这个答案应该足以作为我的答案。我相信您是从创建语言的人的角度谈论这个问题的，在这种情况下，您可以以 ActionScript 3 之类的语言为例。在 AS3 中，您可以使用两种不同的方式进行类型转换：1) NewType(object)，或 2) object as NewType。

从实现的角度来看，我认为每个类都应该定义自己的方式来转换它可以转换成的任何类型（数组不能真正转换成整数......或者可以吗？ ）。例如，如果您尝试 Integer(myArrayObject)，而 myArrayObject 没有定义转换为 Integer 的方式，则可以抛出异常或让它发生并简单地传入原始对象，未转换.

我的整个答案可能完全不正确：-D 如果这不是你要找的，请告诉我

Answer 2

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

我还没有阅读您链接到的论文，但听起来很有趣。你有没有看过 Haskell 中的 ad-hoc 多态性（基本上是重载）是如何工作的？ Haskell 的类型系统是 H-M 加上其他一些好东西。这些好东西之一是类型类。类型类提供重载，或者像 Haskeller 所说的，ad-hoc 多态性。

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

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

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

我希望我能提供一个更好的答案！祝你好运。

Answer 3

我的经验是，直观地为每个术语加糖似乎没有吸引力，但值得追求。

对持久存储的兴趣使我绕道而行，以考虑混合表达式和原子值的问题。为了支持这一点，我决定在类型系统中将它们完全分开；因此 Int、Char 等是仅用于整数和字符值的类型构造函数。表达式类型由多态类型构造函数 Exp 构成；例如Exp Int 是指一步减少到 Int 的值。

当我们考虑评估时，就会出现这与您的问题的相关性。在底层，有些原语需要原子值：COND、addInt 等。有些人将此称为强制表达式，我更愿意将其简单地视为不同类型值之间的强制转换。

挑战在于看看这是否可以在不需要明确的归约指令的情况下完成。一个解决方案完全按照您的建议：即将强制视为一种重载形式。

假设我们有一个输入脚本：foo x

然后，加糖后，变成：(coerce foo) (coerce x)

在哪里，非正式地：

coerce :: a -> b
coerce x = REDUCE (cast x) if a and b are incompatible
x                          otherwise

因此 coerce 是身份或 cast 的应用，其中 b 是给定上下文的返回类型。

cast 现在可以被视为类型类方法，例如

class Cast a, b where {cast :: a -> b };
-- ¬:: is an operator, literally meaning: don’t cast
--(!) is the reduction operator. Perform one stage of reduction.

-- Reduce on demand
instance Cast Exp c, c where { inline cast = ¬::(!)(\x::(Exp c) -> ¬::(!)x) };

¬:: 注释用于抑制强制语法糖化。

目的是可以引入Cast的其他实例来扩展转换范围，虽然我没有探索过这个。正如你所说，重叠的实例似乎是必要的。