Най-простият пример за необходимост от унификация в извода на типа

Опитвам се да разбера как се реализира изводът за тип. По-конкретно, не виждам къде/защо тежкото повдигане на „обединението“ влиза в игра.

Ще дам пример в "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);
    }
}

Но никъде в това не стигаме до необходимостта от алгоритъм за "обединяване".

Така че, очевидно, моят пример не е достатъчно сложен. Има ли нужда от функции от по-висок ред? Имаме ли нужда от "параметричен полиморфизъм"?

Кой е най-простият възможен пример, при който всъщност е необходимо „обединяване“, за да се изведе правилно типа на израз.

Пример в Scheme би бил идеален (т.е. пример за много малка програма Scheme, където се нуждаете от унификация, за да изведете правилно типа на s-израза).


person Paul Hollingsworth    schedule 15.07.2009    source източник
comment
Преди да отговоря, генеричните C# не са ли достатъчни? Те осигуряват извод за тип време на компилация.   -  person Dykam    schedule 15.07.2009
comment
Пример за схема би бил идеален. Както в маркирания пример, мисля, че просто поддържащите функции са достатъчно сложни: (ламбда (x) (+ x 5)) като израз, не ми позволява просто да попитам средата на типа типа на x. Така че всяка функция в езика, със своите обвързващи ограничения, причинява проблема.   -  person Paul Hollingsworth    schedule 16.07.2009


Отговори (3)


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

Ами ако просто не знаете типа на променливата? Това е целият смисъл на извода за тип, нали? Нещо много просто като това (на някакъв език на псевдокод):

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

Не знаете типа на x, докато не направите извод за добавянето и не разберете, че трябва да е цяло число, защото се добавя към цяло число или нещо подобно.

Ами ако имате друга функция като тази:

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

Не можете да разберете типа на x, докато не разберете типа на foo и т.н.

Така че, когато за първи път видите променлива, трябва просто да присвоите някакъв тип контейнер за променлива и след това, когато тази променлива бъде предадена на някакъв вид функция или нещо подобно, трябва да я „унифицирате“ с типа аргумент на функция.

person newacct    schedule 15.07.2009
comment
А, разбирам - функциите са достатъчни. Не знаете типа на x, но тогава x+5 означава, че x трябва да е 5... - person Paul Hollingsworth; 16.07.2009
comment
предполага, че x трябва да е int, което трябва да каже - person Paul Hollingsworth; 16.07.2009
comment
Не съвсем - това просто предполага, че x трябва да е нещо, за което има двоичен оператор +, за което rhs е int (или нещо, за което има имплицитно преобразуване от int, ако езикът има такива). С тази голяма гъвкавост можете просто да дефинирате bar като общ метод, bar<T>(T x) където T има ограничение, че трябва да поддържа оператор + с цяло число (компилаторът извежда ограничението от това как сте го използвали в bar). Така че няма нужда да обвързвате типа x, когато компилирате bar. - person Daniel Earwicker; 23.07.2009

Позволете ми напълно да игнорирам вашия пример и да ви дам пример за това къде правим извод за тип метод в C#. (Ако тази тема ви интересува, препоръчвам ви да прочетете „тип извод" архив на моя блог.)

Обмисли:

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

Тук имаме общ метод M, който взема речник, който картографира низове върху списъци от T. Да предположим, че имате променлива:

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. Ние унифицираме низ с низ, което очевидно е добре, но не научаваме нищо от него.

След това обединяваме List със List и осъзнаваме, че трябва да рекурсираме отново.

След това обединяваме int с T и осъзнаваме, че int е граница на T.

Алгоритъмът за извеждане на типа се отдръпва, докато не може да постигне повече напредък, и след това започва да прави допълнителни изводи от своите заключения. Единственото ограничение на T е int, така че заключаваме, че повикващият трябва да е искал T да бъде int. Затова се обаждаме на M<int>.

Ясно ли е?

person Eric Lippert    schedule 15.07.2009
comment
Да, вече съм абониран за вашия блог - радвам се да ви видя в Stack Overflow! Така че разбирам, че обединението идва от състава на типове от други типове... така че може би функциите от по-висок ред са достатъчни в език, подобен на схема, за да наложат необходимостта от обединение... хм... - person Paul Hollingsworth; 16.07.2009
comment
За да дам повече контекст - написах специфичен за домейн език, където работя, чийто интерпретатор е написан на C#... разглеждаме добавянето на извод за тип към него, за да осигурим по-добра предварителна проверка. Всъщност не е толкова специфичен за домейн - това е по същество интерпретатор на схема, който е много добре интегриран с нашето приложение. Вече добавихме пълна поддръжка за продължения, така че решихме, че някакъв вид извод за тип също би бил добър! Но първо трябва да разберем как да го направим! - person Paul Hollingsworth; 16.07.2009
comment
О, и докато може би четете това: Най-голямата победа за C# би била по-добра поддръжка за откриване на грешки при използване на IDisposable. Бих подскачал нагоре-надолу и бих се радвал от радост, ако добавите това! - person Paul Hollingsworth; 16.07.2009

Да предположим, че имаме функция

f(x, y)

където x може да бъде напр. FunctionOfTwoFunctionsOfInteger или може да е FunctionOfInteger.

да предположим, че минем

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

Сега с обединяването u е обвързано с 1, а z е обвързано с 2, така че първият аргумент е FunctionOfTwoFunctionsOfInteger.

И така, трябва да заключим, че типът x и y са FunctionOfTwoFunctionsOfInteger

Не съм много запознат с C#, но с ламбда изрази (или еквивалентни делегати или каквото и да е) това вероятно би трябвало да е възможно.

За пример за това, когато извеждането на типове е много полезно за подобряване на скоростта на доказване на теорема, погледнете „Парен валяк на Шуберт“

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

Има брой на Journal of Automated Reasoning, посветен на решения и формулировки на този проблем, повечето от които включват въведени изводи в системи за доказване на теореми:

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

person Larry Watanabe    schedule 15.07.2009
comment
Не следя съвсем това... Исках прост пример! ;-) Но благодаря за линковете ще погледна - person Paul Hollingsworth; 16.07.2009