Exemplo mais simples de necessidade de "unificação" na inferência do tipo

Question

Estou tentando entender como o tipo de inferência é implementado. Em particular, não vejo bem onde/por que o levantamento pesado de "unificação" entra em jogo.

Vou dar um exemplo em "Pseudo C#" para ajudar a esclarecer:

A maneira ingênua de fazer isso seria algo assim:

Suponha que você "analise" seu programa em uma árvore de expressão de modo que ele possa ser executado com:

interface IEnvironment
{
    object lookup(string name);
}

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

Então, algo como "multiplicação" pode ser implementado com:

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

Então, para "implementar" o tipo de inferência, você pode fazer algo como:

interface ITypeEnvironment
{
    Type getType(string name);
}

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

Então a inferência do tipo de "multiplicação" pode 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 e RHS podem ser constantes simples, ou "variáveis" que são procuradas no 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);
    }
}

Mas em nenhum lugar nisso acabamos com a necessidade de um algoritmo de "unificação".

Então, claramente, meu exemplo não é complexo o suficiente. Precisa de funções de ordem superior? Precisamos de "polimorfismo paramétrico"?

Qual é o exemplo mais simples possível em que a "unificação" é realmente necessária para inferir corretamente o tipo de expressão.

Um exemplo no esquema seria o ideal (ou seja, um exemplo de um programa de esquema muito pequeno, no qual você precisa da unificação para inferir corretamente o tipo de expressão S).

Answer 1

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

E se você simplesmente não souber o tipo de variável? Esse é o ponto principal da inferência do tipo, certo? Algo muito simples como este (em algum idioma pseudocódigo):

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

Você não sabe o tipo de x, até que você deduza a adição e perceba que deve ser um número inteiro porque é adicionado a um número inteiro, ou algo assim.

E se você tiver outra função como esta:

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

Você não pode descobrir o tipo de x até que você tenha descoberto o tipo de foo, e assim por diante.

Portanto, quando você vê uma variável pela primeira vez, você deve atribuir algum tipo de espaço reservado para uma variável e depois depois, quando essa variável é passada para algum tipo de função ou algo assim, você deve "unificá -lo" com o tipo de argumento do argumento do função.

Answer 2

Deixe -me ignorar completamente o seu exemplo e dar um exemplo de onde fazemos a inferência do tipo de método em C#. (Se esse tópico lhe interessar, eu encorajo você a ler o "Digite inferência"Arquivo do meu blog.)

Considerar:

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

Aqui temos um método genérico m que leva um dicionário que mapeia strings em listas de T. Suponha que você tenha uma variável:

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

Nós chamamos M<T> sem fornecer um argumento de tipo, o compilador deve inferir.

O compilador faz isso "unificando" Dictionary<string, List<int>> com IDictionary<string, List<T>>.

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

Daquele que deduzimos isso Dictionary<string, List<int>> implementos IDictionary<string, List<int>>.

Agora temos uma partida no IDictionary papel. Unificamos a string com string, o que é obviamente tudo de bom, mas não aprendemos nada com ela.

Em seguida, unificamos a lista na lista e percebemos que precisamos voltar novamente.

Em seguida, unificamos o INT com T e percebemos que o INT está vinculado a T.

O algoritmo de inferência do tipo se afasta até que não possa fazer mais progresso e, em seguida, começa a fazer mais deduções de suas inferências. O único limite em t é int, então deduzimos que o chamador deve ter desejado t ser int. Então nós chamamos M<int>.

Está claro?

Answer 3

Suponha que tenhamos uma função

f (x, y)

onde x pode ser, por exemplo, functionOftwofunctionsOfInteger ou pode ser functionOfInteger.

Suponha que passamos

f (g (u, 2), g (1, z))

Agora, com a unificação, u está ligado a 1 e z está vinculado a 2, então o primeiro argumento é um functionOftwofunctionsOfInteger.

Então, temos que inferir que o tipo de x e y são ambos functionoftwofunctionsofInterger

Não estou muito familiarizado com o C#, mas com expressões de lambda (ou equivalentemente delegados ou o que quer que seja), isso provavelmente deve ser possível.

Para um exemplo de onde a inferência do tipo é muito útil para melhorar a velocidade do teorema, dê uma olhada no "Schubert's Steamroller"

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

Há uma questão do Journal of Automated Raconing dedicada a soluções e formulações a esse problema, a maioria dos quais envolve a inferência digitada nos sistemas de prova de teoremas:

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