How to infer coercions?我想知道如何在类型推断期间推断强制(也称为隐式转换)。我使用的是Bastiaan Heeren的"最高质量类型错误消息"中描述的类型推断方案，但我假设总体思想在所有Hindley-Milner风格的方法中都相同。 强制似乎可以被视为重载的一种形式，但是本文中描述的重载方法并未根据上下文对返回类型的要求考虑重载(至少不是我可以遵循的方式)。强制的必须。我还担心这样一种方法可能会使得很难优先考虑身份强制，也难以尊重强制性的传递式封闭。我可以看到将每个可强制表达(例如e)加糖到coerce(e)，但加糖到coerce(coerce(coerce(... coerce(e)...)))的深度等于强制嵌套的最大嵌套似乎很愚蠢，并且还将强制性关系限制为具有有限传递闭包的事物，该闭合闭包的深度与上下文无关，这似乎(不必要地)是限制性的。 我希望您能对此得到一些好的答案。 我尚未阅读您链接的论文，但这听起来很有趣。您是否查看过Haskell中的即席多态性(基本上是重载)是如何工作的？ Haskell的类型系统是H-M加上其他一些东西。这些好处之一是类型类。类型类提供重载，或者像Haskeller所说的那样，提供特殊的多态性。 在使用最广泛的Haskell编译器GHC中，类型类是通过在运行时传递字典来实现的。词典使运行时系统可以从类型到实现进行查找。据说，jhc可以在编译时使用超级优化来选择正确的实现，但我对此表示怀疑，因为它可以处理Haskell可以允许的完全多态情况，而且我不知道有任何形式的证据或论文来证明正确性。 听起来您的类型推断将遇到与其他rank-n多态方法相同的问题。您可能希望在这里阅读一些文章以获取更多背景知识：向下滚动至"关于类型的纸"。他的论文是haskell特有的，但是类型理论对您来说应该是有意义和有用的。 我认为这篇有关Rank-n多态性和类型检查问题的论文应该为您激发一些有趣的想法：http://research.microsoft.com/~simonpj/papers/higher-rank/ 希望我能提供更好的答案！祝好运。 我的经验是，直觉上每个词都没有吸引力，但值得追求。 对持久性存储的兴趣使我走上了circuit回曲折的路线，以考虑将表达式和原子值混合在一起的问题。为此，我决定将它们完全分隔在类型系统中。因此，Int，Char等仅是整数和字符值的类型构造函数。表达式类型由多态类型构造函数Exp形成；例如Exp Int是指一步减小到Int的值。 当我们考虑评估时，这与您的问题相关。在底层层次上，有一些需要原子值的原语：COND，addInt等。有人将其称为强制表达式，我更喜欢将其视为不同类型的值之间的强制转换。 挑战在于查看是否可以在不需要显式减少指令的情况下完成此操作。一种解决方案正是您所建议的：即将强制视为过载的一种形式。
假设我们有一个输入脚本：
然后，加糖后，它变为： 非正式地：
因此，强制是身份或强制转换的应用，其中b是给定上下文的返回类型。 强制转换现在可以视为类型类方法，例如
目的是可以引入 您能否进一步说明您要问的是什么？ 我的想法很简单，如果我的想法正确，那么这个答案就足够了。我相信您是从创建语言的人的角度来谈论这个问题的，在这种情况下，您可以看一下ActionScript 3之类的语言作为示例。在AS3中，您可以使用两种不同的方式进行类型转换：1)NewType(object)，或2)object as NewType。 从实现的角度来看，我想像每个类都应该定义其自己的方法，以将其转换为可以转换为的任何类型(Array不能真正转换为整数...或者可以吗？)。例如，如果您尝试使用Integer(myArrayObject)，而myArrayObject没有定义转换为Integer的方式，则可以引发异常，也可以让它直接传入未经广播的原始对象。 我的整个答案可能完全不对：-D让我知道这是否不是您要的内容 |
