El ejemplo más simple de necesidad de "unificación" en inferencia de tipo

Question

Estoy tratando de entender cómo se implementa la inferencia de tipo. En particular, no veo dónde/por qué el trabajo pesado de la "unificación" entra en juego.

Daré un ejemplo en "Pseudo C#" para ayudar a aclarar:

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

Supongamos que "analiza" su programa en un árbol de expresión de modo que pueda ejecutarse con:

interface IEnvironment
{
    object lookup(string name);
}

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

Por lo tanto, se podría implementar algo como "multiplicación" 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 tipo, podría 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 así:

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 medio ambiente:

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 "polimorfismo paramétrico"?

¿Cuál es el ejemplo más simple posible en el que se necesita "unificación" para inferir correctamente el tipo de expresión?

Un ejemplo en el esquema sería ideal (es decir, un ejemplo de un programa de esquema muy pequeño donde necesita unificación para inferir correctamente el tipo de expresión S).

Answer 1

public Type inferType(ITypeEnvironment typeEnvironment)
{
    return typeEnvironment.getType(name);
}

¿Qué pasa si simplemente no conoces el tipo de variable? Ese es el objetivo de inferencia de tipo, ¿verdad? Algo muy simple como este (en algún lenguaje de pseudocódigo):

function foo(x) { return x + 5; }

No sabes el tipo de x, hasta que infiera la adición y date cuenta de que debe ser un entero porque se agrega a un entero o algo así.

¿Qué pasa si tienes otra función como esta?

function bar(x) { return foo(x); }

No puedes entender el tipo de x Hasta que haya descubierto el tipo de foo, y así.

Entonces, cuando ve una variable por primera vez, debe asignar algún tipo de marcador de posición para una variable, y luego, cuando esa variable se pasa a algún tipo de función o algo así, debe "unificarlo" con el tipo de argumento del función.

Answer 2

Permítanme ignorar por completo su ejemplo y darle un ejemplo de dónde hacemos la inferencia de tipo de método en C#. (Si este tema le interesa, le animo a que lea el "Tipo de inferencia"Archivo de mi blog.)

Considerar:

void M<T>(IDictionary<string, List<T>> x) {}

Aquí tenemos un método genérico M que toma un diccionario que mapea las cadenas en las listas de T. Suponga que tiene una variable:

var d = new Dictionary<string, List<int>>() { ...initializers here... };
M(d);

Hemos llamado M<T> Sin proporcionar un argumento de tipo, por lo que el compilador debe inferirlo.

El compilador lo hace "unificando" Dictionary<string, List<int>> con IDictionary<string, List<T>>.

Primero determina que Dictionary<K, V> implementos IDictionary<K, V>.

De eso deducimos eso Dictionary<string, List<int>> implementos IDictionary<string, List<int>>.

Ahora tenemos un partido en el IDictionary parte. Unificamos la cadena con String, que obviamente es todo bien, pero no aprendemos nada de ella.

Luego unificamos la lista con la lista y nos damos cuenta de que tenemos que recurrir nuevamente.

Luego unificamos int con t y nos damos cuenta de que int es un límite en T.

El algoritmo de inferencia de tipo se aleja hasta que no puede avanzar más, y luego comienza a hacer más deducciones de sus inferencias. El único límite en t es int, por lo que deducimos que la persona que llama debe haber querido que T fuera int. Entonces llamamos M<int>.

¿Está claro?

Answer 3

Supongamos que tenemos una función

f (x, y)

Donde x podría ser por ejemplo, FunctionOftWofunctionsFinTeger o podría ser FunctionOfInteger.

Supongamos que pasamos

F (G (U, 2), G (1, Z))

Ahora con la unificación, U está vinculado a 1, y Z está vinculado a 2, por lo que el primer argumento es una FunctionOftWofunctions ofInteger.

Por lo tanto, tenemos que inferir que el tipo de X e Y son FunctionOftWofunctionsFinTeger

No estoy demasiado familiarizado con C#, pero con expresiones lambda (o delegados de manera equivalente o lo que sea) esto probablemente debería ser posible.

Para obtener un ejemplo de dónde la infección de tipo es muy útil para mejorar la velocidad de la prueba del teorema, eche un vistazo a "Schubert's Steamroller"

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

Hay un problema del Revista de razonamiento automatizado dedicado a soluciones y formulaciones a este problema, la mayoría de las cuales implican inferencia tipificada en los sistemas de prueba del teorema:

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