在类型推断中需要"统一"的最简单的例子

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);
    }
}

但在这方面,我们最终还是需要一种"统一"算法.

所以,显然,我的例子不够复杂.它需要更高阶的功能吗？我们需要"参数多态"吗？

什么是最简单的可能示例,其中实际需要"统一"来正确推断表达式的类型.

Scheme中的一个例子是理想的(即一个非常小的Scheme程序的例子,你需要统一才能正确地推断出s-expression的类型).

Answer 1

让我完全忽略您的示例,并举例说明我们在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部分.我们用字符串统一字符串,这显然都很好但我们从中学不到任何东西.

然后我们将List与List统一,并意识到我们必须再次递归.

然后我们用T统一int,并意识到int是T的绑定.

类型推断算法逐渐消失,直到它不再有进展,然后它开始从推论中进一步推断.T上唯一的绑定是int,所以我们推断出调用者必须要T为int.所以我们打电话M<int>.

明白了吗？