Я пытаюсь понять, как реализован вывод типов. В частности, я не совсем понимаю, где и почему в игру вступает тяжелый подъем «объединения».
Я приведу пример на «псевдо-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-выражения).
