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

Question

我试图让我的脑袋知道如何实现类型推断。 特别是，我不太清楚“统一”的重要起因在哪里/为什么发挥作用。

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

用简单的方式做这将是这样的：

假设你用“解析”你的程序变成一个表达式树使得它能够与执行：

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 IEnvironment 
{ 
    object lookup(string name); 
} 

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

因此，像“乘法”可能与实现0

再到“实现”类型推断，你可能只是这样做：

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

但远不在此做我们最终需要一个“unificatio n“算法。

所以，显然，我的例子并不够复杂。它需要更高阶的功能吗？我们是否需要“参数多态性”？

什么是最简单的例子，其中“统一”实际上需要正确推断表达式的类型。

Scheme中的一个例子是理想的（即一个非常小的Scheme程序的例子，您需要统一来正确地推断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); } 

，直到你已经想通了的类型foo，等你琢磨不透的x类型。

所以，当你第一次看到一个变量时，你必须为一个变量指定一个占位符类型，然后，当这个变量被传递给某种函数或某个东西时，必须将它“统一”参数类型的函数。

Answer 2

假设我们有一个功能

F（X，Y）

其中x可以是例如FunctionOfTwoFunctionOfInteger 或者它可能是FunctionOfInteger。

假设我们通过在

F（克（U，2），G（1，Z））

与统一

现在，u被绑定到1，和z势必2，所以第一个参数是一个FunctionOfTwoFunctionsOfInteger。

所以，我们推断x和y的类型都是FunctionOfTwoFunctionsOfInteger

我不是太熟悉C＃，但与lambda表达式（或等同的代表或其他）这也许应该是可能的。

对于其中的类型推断是提高定理证明的速度是非常有用的一个例子，看看“舒伯特的压路机”

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

有专门的杂志自动推理的问题溶液和制剂对这个问题，其中大部分是在定理证明系统涉及类型的推理：

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

Answer 3

让我完全忽略你的例子，给你一个我们在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部分有一场比赛。我们用字符串统一字符串，这显然是好的，但我们从中学不到什么。

然后我们统一List与List，并且意识到我们必须再次递归。

然后我们统一用INT T，并且认识到int是对T.

类型推理算法的一班班距离，直到它可以使没有更多的进展绑定，然后它开始从它的推论做进一步的推论。 T上的唯一约束是int，所以我们推断调用者必须要T是int。所以我们打电话M<int>。

这是明确的吗？