型推論における「統一」の必要性の最も単純な例

StackOverflow https://stackoverflow.com/questions/1133289

質問

タイプの推論がどのように実装されているかを頭に入れようとしています。特に、「統一」の重い持ち上げがどこに登場するのか、なぜどこで作用するのかはよくわかりません。

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

しかし、これのどこにも、「統一」アルゴリズムの必要性が必要になりません。

したがって、明らかに、私の例は十分に複雑ではありません。高次関数が必要ですか？ 「パラメトリック多型」が必要ですか？

式のタイプを正しく推測するために「統一」が実際に必要である最も単純な例は何ですか。

スキームの例は理想的です（つまり、S-Expressionのタイプを正しく推測するために統一が必要な非常に小さなスキームプログラムの例です）。

役に立ちましたか？

解決 

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

変数のタイプがわからない場合はどうなりますか？それがタイプの推論の全体のポイントですよね？このような非常にシンプルなもの（いくつかの擬似コード言語で）：

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

あなたはタイプのタイプを知りません x, 、追加を推測するまで、整数に追加されているため、整数である必要があることに気付くまで。

このような別の関数がある場合はどうなりますか：

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

あなたはタイプを理解することはできません x あなたがタイプのタイプを理解するまで foo, 、 等々。

したがって、最初に変数を表示した場合、変数にプレースホルダータイプを割り当てるだけで、その後、その変数が何らかの機能などに渡されると、引数タイプのタイプで「統合」する必要があります。関数。

他のヒント

あなたの例を完全に無視して、C＃でメソッドタイプの推論を行う場所の例を教えてください。 （このトピックがあなたに興味を持っているなら、私はあなたが読むことをお勧めします」タイプ推論「私のブログのアーカイブ。）

検討：

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

ここには、Tのリストに文字列をマッピングする辞書Mを取得する一般的な方法mがあります。変数があると仮定します。

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

電話をかけました M<T> タイプの引数を提供せずに、コンパイラはそれを推測する必要があります。

コンパイラは「統一」によってそうします Dictionary<string, List<int>> と IDictionary<string, List<T>>.

最初にそれを決定します Dictionary<K, V> 道具 IDictionary<K, V>.

それから私たちはそれを推測します Dictionary<string, List<int>> 道具 IDictionary<string, List<int>>.

これで試合があります IDictionary 部。文字列を文字列で統合しますが、これは明らかにすべて良いことですが、それから何も学びません。

次に、リストを統合し、再び再発しなければならないことを認識します。

次に、TでINTを統合し、INTがTにバインドされていることを認識しています。

タイプの推論アルゴリズムは、これ以上進歩することができなくなるまで追い払われ、その推論からさらなる控除を開始します。 Tの唯一の縛られているのはintなので、発信者がTであることを望んでいたに違いないと推測します。だから私たちは呼びます M<int>.

それは明らかですか？

関数があるとします

f（x、y）

xは、functionoftwofunctionsofintegerである場合、またはfunctionofintegerである可能性があります。

私たちが通り過ぎると仮定します

f（g（u、2）、g（1、z））

統一されていると、uは1に結合し、zは2に結合されるため、最初の引数はfunctionoftwof functionsofintegerです。

したがって、xとyのタイプは両方ともfunctionoftwofunctionsofintegerであると推測する必要があります

C＃にはあまり精通していませんが、Lambdaの表現（または同等に代表者など）については、おそらく可能です。

タイプの推論が定理の速度を改善するのに非常に役立つ場所の例については、「Schubert's Steamroller」をご覧ください

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

この問題の解決策と定式化に専念する自動化された推論のジャーナルには問題があります。そのほとんどは、定理的なシステムでのタイプされた推測を含みます。

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

ライセンス： CC-BY-SA と 帰属
所属していません StackOverflow
scroll top