Exemple de besoin Simplest pour « unification » dans l'inférence de type

Question

Je suis en train d'obtenir ma tête comment l'inférence de type est mis en œuvre. En particulier, je ne vois pas où / pourquoi le levage de charges lourdes de « unification » entre en jeu.

Je vais vous donner un exemple dans "pseudo C #" pour aider à clarifier:

La façon naïve de le faire serait quelque chose comme ceci:

Supposons que vous « Parse » votre programme dans un arbre d'expression telle qu'elle peut être exécutée avec:

interface IEnvironment
{
    object lookup(string name);
}

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

Alors quelque chose comme "multiplication" pourrait être mis en œuvre avec:

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

Alors à l'inférence de type « mettre en œuvre », vous pouvez simplement faire quelque chose comme:

interface ITypeEnvironment
{
    Type getType(string name);
}

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

Ensuite, l'inférence de type d ' "Multiplication" est peut-être quelque chose comme:

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 et RHS peuvent être des constantes simples, ou « variables » qui sont recherchés dans l'environnement:

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

Mais nulle part dans ce ne nous nous retrouvons avec la nécessité d'un algorithme « d'unification ».

Alors, clairement, mon exemple est pas assez complexe. Est-il besoin des fonctions d'ordre supérieur? Avons-nous besoin « polymorphisme paramétrique »?

Quel est l'exemple le plus simple possible, où « l'unification » est réellement nécessaire pour déduire correctement le type d'une expression.

Un exemple dans le schéma serait idéal (à savoir un exemple d'un très petit programme de régime où vous avez besoin d'unification de déduire correctement le type de s-expression).

Answer 1

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

Que faire si vous ne savez pas le type de la variable? C'est toute la question de l'inférence de type, non? Quelque chose très simple comme celui-ci (dans une langue de pseudo-code):

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

Vous ne connaissez pas le type de x, jusqu'à ce que vous déduisez l'addition, et se rendre compte qu'il doit être un entier parce qu'il est ajouté à un entier, ou quelque chose comme ça.

Que faire si vous avez une autre fonction comme ceci:

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

Vous ne pouvez pas déterminer le type de x jusqu'à ce que vous avez compris le type de foo, et ainsi de suite.

Alors, quand vous voyez d'abord une variable, vous devez simplement attribuer un certain type d'espace réservé pour une variable, puis plus tard, lorsque cette variable est passé à une sorte de fonction ou quelque chose, vous devez « unifier » avec l'argument type de la fonction.

Answer 2

Laissez-moi ignorer complètement votre exemple et vous donner un exemple de ce que nous faisons l'inférence de type de méthode en C #. (Si ce sujet vous intéresse je vous encourage à lire le « inférence de type » archives de mon blog.)

Considérez:

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

Ici, nous avons une méthode générique M qui prend un dictionnaire qui mappe des chaînes sur les listes de T. Supposons que vous ayez une variable:

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

Nous avons appelé M<T> sans fournir un argument de type, de sorte que le compilateur doit la déduire.

Le compilateur fait en Dictionary<string, List<int>> « fédérateur » avec IDictionary<string, List<T>>.

D'abord, il détermine que Dictionary<K, V> implémente IDictionary<K, V>.

A partir de ce que nous déduisons Dictionary<string, List<int>> implémente IDictionary<string, List<int>>.

Maintenant, nous avons un match de la part de IDictionary. Nous unissons la chaîne avec la chaîne, ce qui est évidemment tout bon, mais nous apprenons rien de lui.

Ensuite, nous unissons avec Liste Liste, et se rendre compte que nous devons récursif à nouveau.

Ensuite, nous unissons int avec T, et se rend compte que int est une borne sur T.

L'algorithme d'inférence de type chugs loin jusqu'à ce qu'il puisse faire plus de progrès, et il commence à faire des déductions plus de ses conclusions. La seule limite sur T est un entier, donc on en déduit que l'appelant doit avoir voulu T être int. Nous appelons donc M<int>.

Est-ce clair?

Answer 3

Supposons que nous ayons une fonction

f (x, y)

où x peut être, par exemple FunctionOfTwoFunctionsOfInteger ou il pourrait être FunctionOfInteger.

supposons que nous passons

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

Maintenant, avec l'unification, u est lié à 1, et z est lié à 2, de sorte que le premier argument est un FunctionOfTwoFunctionsOfInteger.

Alors, il faut en déduire que le type de x et y sont à la fois FunctionOfTwoFunctionsOfInteger

Je ne suis pas trop familier avec C #, mais avec des expressions lambda (ou délégués ou autre) de manière équivalente cela devrait probablement être possible.

Pour un exemple de où le type est très utile inférences pour améliorer la vitesse de démonstration automatique, un coup d'oeil à « Steamroller Schubert »

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

Il y a un numéro du Journal de Raisonnement automatisé consacré aux solutions et formulations à ce problème, dont la plupart impliquent tapé dans les systèmes d'inférence prouvant le théorème:

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