类型推理中需要“统一”的最简单示例

Question

我正在努力围绕如何实现类型推理。尤其是，我不太了解“统一”的繁重起伏在哪里。

我将在“伪C＃”中举一个例子，以帮助澄清：

幼稚的做法将是这样的事情：

假设您将程序“解析”到表达树中，以便可以执行以下操作：

interface IEnvironment
{
    object lookup(string name);
}

interface IExpression
{
    // Evaluate this program in this environment
    object Evaluate(IEnvironment e);
}

因此，可以通过以下方式实现诸如“乘法”之类的东西：

class Multiply : IExpression
{
    IExpression lhs;
    IExpression rhs;
    // etc.
    public object Evaluate(IEnvironment e)
    {
        // assume for the moment C# has polymorphic multiplication
        return lhs.Evaluate(e) * rhs.Evaluate(e);
    }
}

然后“实现”类型推理，您可以做类似的事情：

interface ITypeEnvironment
{
    Type getType(string name);
}

interface IExpression
{
    //as before
    object Evaluate(IEnvironment e);
    // infer type
    Type inferType(ITypeEnvironment typeEnvironment);
}

然后，“乘法”的类型推理可能只是：

class Multiply : IExpression
{
    IExpression lhs;
    IExpression rhs;

    // ... 
    public Type inferType(ITypeEnvironment typeEnvironment)
    {
        Type lhsType = lhs.inferType(typeEnvironment);
        Type rhsType = rhs.inferType(typeEnvironment);
        if(lhsType != rhsType)
             throw new Exception("lhs and rhs types do not match");

        // you could also check here that lhs/rhs are one of double/int/float etc.
        return lhsType;
    }
}

LHS和RHS可能是简单的常数，也可能是在环境中查找的“变量”：

class Constant : IExpression
{
    object value;
    public Type inferType(ITypeEnvironment typeEnvironment)
    {
        return value.GetType(); // The type of the value;
    }
    public object Evaluate(IEnvironment environment)
    {
        return value;
    }
}

class Variable : IExpression
{
    string name;
    public Type inferType(ITypeEnvironment typeEnvironment)
    {
        return typeEnvironment.getType(name);
    }
    public object Evaluate(IEnvironment environment)
    {
        return environment.lookup(name);
    }
}

但是，在此过程中，我们最终无需使用“统一”算法。

因此，显然，我的榜样还不够复杂。它需要高阶功能吗？我们需要“参数多态性”？

真正需要“统一”才能正确推断表达的类型的最简单示例是什么。

方案中的一个示例将是理想的（即一个非常小的计划程序的示例，您需要统一以正确推断S-表达的类型）。

Answer 1

public Type inferType(ITypeEnvironment typeEnvironment)
{
    return typeEnvironment.getType(name);
}

如果您只是不知道变量的类型怎么办？那是类型推理的全部点，对吗？类似这样简单的东西（在某些伪代码语言中）：

function foo(x) { return x + 5; }

你不知道 x, ，直到您推断出添加并意识到它必须是整数，因为它被添加到整数或类似的东西中。

如果您有这样的另一个函数怎么办：

function bar(x) { return foo(x); }

您无法弄清楚的类型 x 直到您弄清楚 foo, ， 等等。

因此，当您第一次看到变量时，您只需要为变量分配某些占位符类型，然后再将该变量传递给某种函数或其他内容时，您必须将其“统一”与该变量的参数类型“统一”功能。

Answer 2

让我完全忽略您的示例，并为您提供一个在C＃中进行方法类型推理的示例。 （如果您感兴趣这个话题，那么我鼓励您阅读“类型推理“我的博客的档案。）

考虑：

void M<T>(IDictionary<string, List<T>> x) {}

在这里，我们有一个通用方法m，该方法将字典映射到T列表中。假设您有一个变量：

var d = new Dictionary<string, List<int>>() { ...initializers here... };
M(d);

我们已经打电话 M<T> 如果不提供类型的参数，因此编译器必须推断出来。

编译器通过“统一”来做到这一点 Dictionary<string, List<int>> 和 IDictionary<string, List<T>>.

首先，它决定了 Dictionary<K, V> 工具 IDictionary<K, V>.

从中我们推断出来 Dictionary<string, List<int>> 工具 IDictionary<string, List<int>>.

现在我们在 IDictionary 部分。我们将字符串统一，这显然是不错的，但我们从中学到什么也没学。

然后，我们将列表统一，并意识到我们必须再次重复。

然后，我们将int统一，并意识到int是对T的绑定。

类型的推理算法会消失，直到它无法取得进展为止，然后开始从其推论中进一步推论。唯一对T的界限是INT，因此我们推断出来者必须希望t是int。所以我们打电话 M<int>.

明白了吗？

Answer 3

假设我们有一个函数

F（x，y）

x可能是eg functionOftwofunctionsofinteger，或者它可能是functionofinteger。

假设我们经过

f（g（u，2），g（1，z））

现在，通过统一，u绑定到1，而z绑定到2，因此第一个参数是functionoftwofunctionsofinteger。

因此，我们必须推断x和y的类型都是functionoftwofunctionsofinteger

我对C＃不太熟悉，但是对于Lambda表达式（或等效的委托或其他），这可能是可能的。

对于一个示例，在哪里推理对于提高定理的速度非常有用，请看一下“舒伯特的Steamroller”

http://www.rpi.edu/~brings/pai/schub.steam/node1.html

存在着专门针对该问题的解决方案和配方的自动推理杂志的问题，其中大多数涉及在定理证明系统中键入推断：

http://www.springerlink.com/content/k1425x112w6671g0/