带有重载的类型推断

Question

我正在研究一种支持重载的类型系统。我对在这种情况下通常如何实现类型推断有一个粗略的想法，但我想知道如何-在类型推断完成后-可以选择重载运算符的正确实现。或者，换句话说，如何将推断的类型传递回语法树给运算符。

对于一个小示例，请考虑表达式 (x + y) + 1 哪里 x :: N | S, y :: a, + :: (N -> N -> N) | (S -> S -> S), 1 :: N. :: 代表 类型的, ，而 a | b 代表类型 a 或 类型 b.

我认为，类型推断现在可以工作的方式是遍历语法树，并为每个节点返回一个类型约束:

(x + y) + 1 => ((N & (N[a=N] | S[a=S])), (N & N) -> N) | ((S & (N[a=N] | S[a=S])), (S & N) -> S) => N[a=N]
  1         => N
  +         => (N -> N -> N) | (S -> S -> S)
  x + y     => ((N & (N | S)), (N & a) -> N) | ((S & (N | S)), (S & a) -> S) => N[a=N] | S[a=S]
    x       => N | S
    y       => a
    +       => (N -> N -> N) | (S -> S -> S)

a & b 在这个例子中代表 统一起来 类型 a 和 b, [a=T, b=U] 是类型变量的一组相等约束。

正如预期的那样，给定表达式的返回类型推断为 N[a=N], ，即 N 类型变量的位置 a 预计将是 N.

因此，在所提供的两个实现中， + 操作员(N -> N -> N, S -> S -> S), N -> N -> N 应使用。在给定的示例中，推断出结果类型，但不推断重载运算符的类型。我的问题是，如果有一个共同的模式，用于通知 + 用的实现的语法树中的节点。

Answer 1

您可以按如下方式组织类型推断。

假设您的输入语法具有类型 Input.定义输出语法 Output 要像 Input 但是对所有变量都有显式的类型注释。类型推断将具有类型

infer : Input -> List (Output * Type)

也就是说，给定一些输入 e, ，它返回可能的答案列表。每个答案都是一对 (e', t) 哪里 e' 是 e 用类型注释的变量，以及 t 是推断的类型 e.

你可以把这看作是在非确定性monad中发生的一切。每当需要推断变量的类型时 x, ，你查找它可能的类型 S | T | ... 并在它们每一个上分支。这样，您就不必将任何信息"传回"给子表达式。相反，每个子表达式已经以所有可能的方式进行了注释。