El ejemplo más simple de la necesidad de “unificación” en la inferencia de tipos.

Estoy tratando de entender cómo se implementa la inferencia de tipos. En particular, no veo exactamente dónde / por qué entra en juego el pesado levantamiento de la “unificación”.

Daré un ejemplo en “pseudo C #” para ayudar a aclarar:

La forma ingenua de hacerlo sería algo como esto:

Supongamos que “analiza” su progtwig en un árbol de expresión tal que puede ejecutarse con:

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

Así que algo como “Multiplicación” podría implementarse con:

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

Luego, para “implementar” la inferencia de tipos, puedes hacer algo como:

 interface ITypeEnvironment { Type getType(string name); } interface IExpression { //as before object Evaluate(IEnvironment e); // infer type Type inferType(ITypeEnvironment typeEnvironment); } 

Entonces la inferencia de tipo de “Multiplicación” podría ser algo como:

 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 y rhs pueden ser constantes simples o “variables” que se buscan en el entorno:

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

Pero en ninguna parte de esto terminamos con la necesidad de un algoritmo de “unificación”.

Entonces, claramente, mi ejemplo no es lo suficientemente complejo. ¿Necesita funciones de orden superior? ¿Necesitamos el “polymorphism paramétrico”?

¿Cuál es el ejemplo más simple posible donde se necesita realmente la “unificación” para inferir correctamente el tipo de una expresión?

Un ejemplo en Esquema sería ideal (es decir, un ejemplo de un progtwig de Esquema muy pequeño en el que se requiere la unificación para inferir correctamente el tipo de la expresión-s).