c# - 类型推断中需要 "unification"的最简单示例

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 表达式的类型)。

Answer 1

让我完全忽略你的例子，给你一个例子，说明我们在 C# 中进行方法类型推断的地方。 (如果您对这个主题感兴趣，那么我鼓励您阅读我博客的“type inference”存档。)

考虑:

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 上有一个匹配项部分。我们将 string 与 string 统一起来，这显然很好，但我们没有从中学到任何东西。

然后我们统一List和List，意识到又要递归了。

然后我们将 int 与 T 统一，并意识到 int 是 T 上的一个边界。

类型推理算法会突然消失，直到它无法再取得进展，然后它开始从其推理中进行进一步的推论。 T 上的唯一绑定(bind)是 int，所以我们推断调用者一定希望 T 是 int。所以我们调用M<int> .

清楚了吗？