我想知道如何在类型推断期间推断强制(也称为隐式转换)。我使用的是Bastiaan Heeren的" Top Quality Type Error Messages"中描述的类型推断方案，但我假设总体思想在所有Hindley-Milner风格的方法中都相同。

强制似乎可以被视为重载的一种形式，但是本文中描述的重载方法并未根据上下文对返回类型的要求考虑重载(至少不是我可以遵循的方式)。强制的必须。我还担心这样一种方法可能会使得很难优先考虑身份强制，也难以尊重强制性的传递式封闭。我可以看到将每个可强制表达(例如e)加糖到coerce(e)，但加糖到coerce(coerce(coerce(... coerce(e)...)))的深度等于最大强制嵌套似乎很愚蠢，并且还将强制性关系限制为具有有限传递闭包的事物，该闭合闭包的深度与上下文无关，这似乎(不必要地)是限制性的。

解决方案

回答

我们能否进一步说明我们要问的是什么？

我的想法很简单，如果我的想法正确，那么这个答案就足够了。我相信我们是从创建语言的人的角度谈论此问题的，在这种情况下，我们可以看一下ActionScript 3之类的语言作为示例。在AS3中，我们可以使用两种不同的方式进行类型转换：1)NewType(object)，或者2)object as NewType。

从实现的角度来看，我想像每个类都应该定义它自己的转换为可以转换为任何类型的类型的方式(Array不能真正转换为整数...或者可以吗？)。例如，如果我们尝试使用Integer(myArrayObject)，而myArrayObject没有定义转换为Integer的方式，则可以引发异常，也可以让它直接传入未经广播的原始对象。

我的整个答案可能完全不对：-D让我知道这是否不是我们要的内容

回答

我希望我们能对此得到一些好的答案。

我尚未阅读我们链接的论文，但这听起来很有趣。我们是否查看过Haskell中的即席多态性(基本上是重载)是如何工作的？ Haskell的类型系统是H-M加上其他一些好东西。这些好处之一是类型类。类型类提供了重载，或者像Haskeller所说的那样，提供了特殊的多态性。

在使用最广泛的Haskell编译器GHC中，类型类是通过在运行时传递字典来实现的。字典使运行时系统可以从类型到实现进行查找。据说，jhc可以在编译时使用超级优化来选择正确的实现，但我对此表示怀疑，因为它可以处理Haskell可以允许的完全多态情况，而且我不知道有任何形式的证据或者论文断言这种正确性。

听起来类型推断将遇到与其他rank-n多态方法相同的问题。我们可能希望在此处阅读一些文章以获取更多背景知识：向下滚动至"关于类型的纸"。他的论文是Haskell特有的，但是类型理论对我们来说应该是有意义和有用的。

我认为有关等级n多态性和类型检查问题的本文应该为我们激发一些有趣的想法：http://research.microsoft.com/~simonpj/papers/higher-rank/

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

回答

我的经验是，直觉上每个词都没有吸引力，但是值得追求。

对持久性存储的兴趣使我走了一条circuit回的路线来考虑混合表达式和原子值的问题。为此，我决定将它们完全分隔在类型系统中。因此，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

因此，强制是身份或者强制转换的应用，其中b是给定上下文的返回类型。

现在可以将强制类型转换视为类型类方法，例如

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"实例来扩展转换范围，尽管我没有对此进行探讨。正如我们所说，重叠的实例似乎是必需的。