Опитвам се да разбера как се реализира изводът за тип. По-конкретно, не виждам къде/защо тежкото повдигане на „обединението“ влиза в игра.
Ще дам пример в "pseudo 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-израза).