Вывод типа

Вывод типа , иногда называемый реконструкцией типа , ^[1]^: 320 относится к автоматическому определению типа выражения на формальном языке . К ним относятся языки программирования и системы математических типов , а также естественные языки в некоторых областях информатики и лингвистики .

Нетехническое объяснение

Типы в самом общем виде могут быть связаны с назначенным использованием, предполагающим и ограничивающим действия, возможные для объекта этого типа. Многие существительные в языке определяют такое использование. Например, слово «поводок» указывает на другое использование, чем слово « линия» . Назвать что-либо столом означает другое обозначение, чем называть это дровами , хотя по сути это может быть одно и то же. Хотя их материальные свойства позволяют использовать вещи для определенных целей, они также подлежат особым обозначениям. Это особенно актуально в абстрактных областях, а именно в математике и информатике, где материал в конечном итоге представляет собой лишь биты или формулы.

Чтобы исключить нежелательное, но материально возможное использование, концепция типов определяется и применяется во многих вариациях. В математике парадокс Рассела положил начало появлению первых версий теории типов. В языках программирования типичными примерами являются «ошибки типа», например, команда компьютеру суммировать значения, которые не являются числами. Хотя это возможно с материальной точки зрения, результат больше не будет иметь смысла и, возможно, будет катастрофическим для всего процесса.

При типизации выражение противопоставляется типу. Например, $4$ , $2+2$ , и $2\cdot 2$ все это отдельные термины с типом $\mathrm {nat}$ для натуральных чисел . Традиционно за выражением следует двоеточие и его тип, например: $2:\mathrm {nat}$ . Это означает, что значение $2$ имеет тип $\mathrm {nat}$ . Эта форма также используется для объявления новых имен, например $n:\mathrm {nat}$ , очень похоже на введение в сцену нового персонажа словами «детектив Декер».

В отличие от истории, в которой обозначения разворачиваются медленно, объекты в формальных языках часто приходится с самого начала определять по их типу. Кроме того, если выражения неоднозначны, могут потребоваться типы, чтобы явно указать предполагаемое использование. Например, выражение $2$ может иметь тип $\mathrm {nat}$ но его также можно читать как рациональное или действительное число или даже как простой текст .

Как следствие, программы или доказательства могут настолько перегрузиться типами, что их желательно выводить из контекста. Это может быть возможно путем сбора данных об использовании нетипизированных выражений (включая неопределенные имена). Если, например, еще неопределенное имя n в выражении используется $n+2$ , можно заключить, что n — это как минимум число. Процесс вывода типа из выражения и его контекста — это вывод типа .

В общем, не только объекты, но и действия имеют типы и могут быть введены просто путем их использования. Для истории «Звездного пути» такой неизвестной деятельностью может быть «сияние», которое ради развития сюжета просто выполняется и никогда официально не представлено. Тем не менее, по тому, что происходит, можно определить его тип (транспорт). Кроме того, как объекты, так и действия могут быть построены из их частей. В таких условиях вывод типов не только становится более сложным, но и более полезным, поскольку позволяет собрать полное описание всего в составной сцене, сохраняя при этом возможность обнаруживать конфликтующие или непреднамеренные варианты использования.

Проверка типов против вывода типов

При типизации выражение E противопоставляется типу T, формально записываемому как E : T. Обычно типизация имеет смысл только в некотором контексте, который здесь опущен.

В этой ситуации особый интерес представляют следующие вопросы:

Э: Т? В этом случае заданы как выражение E, так и тип T. Итак, действительно ли E — это T? Этот сценарий известен как проверка типов .
Э: _? Здесь известно только выражение. Если есть способ получить тип для E, то мы выполнили вывод типа .
_ : Т? Наоборот. Учитывая только тип, есть ли для него какое-либо выражение или тип не имеет значений? Есть ли пример буквы Т? Это известно как тип проживания .

Для простого лямбда-исчисления все три вопроса разрешимы . Ситуация не столь комфортна, когда более выразительные допускаются типы.

Типы в языках программирования

Типы — это функция, присутствующая в некоторых строго статически типизированных языках. Это часто характерно для функциональных языков программирования в целом. Некоторые языки, которые включают вывод типа, включают C23 , ^[2] С++11 , ^[3] C# (начиная с версии 3.0), Chapel , Clean , Crystal , D , F# , ^[4] FreeBASIC , Go , Haskell , Java (начиная с версии 10), Julia , ^[5] Котлин , ^[6] ML , Nim , OCaml , Opa , Q#, RPython , Rust , ^[7] Скала , ^[8] Быстрый , ^[9] TypeScript , ^[10] Налейте , ^[11] Дарт , ^[12] и Visual Basic ^[13] (начиная с версии 9.0). Большинство из них используют простую форму вывода типа; система типов Хиндли-Милнера может обеспечить более полный вывод типов. Возможность автоматического вывода типов упрощает многие задачи программирования, позволяя программисту пропускать аннотации типов , но при этом разрешая проверку типов.

В некоторых языках программирования все значения имеют тип данных , явно объявленный во время компиляции , что ограничивает значения, которые определенное выражение может принимать во время выполнения . все чаще Компиляция по принципу «точно в срок» стирает различие между временем выполнения и временем компиляции. Однако исторически сложилось так, что если тип значения известен только во время выполнения, эти языки являются динамически типизированными . В других языках тип выражения известен только во время компиляции ; эти языки статически типизированы . В большинстве статически типизированных языков входные и выходные типы функций и локальных переменных обычно должны быть явно указаны с помощью аннотаций типов. Например, в ANSI C :

int add_one(int x) {
    int result; /* declare integer result */

    result = x + 1;
    return result;
}

Подпись , этого определения функции int add_one(int x), заявляет, что add_one — это функция, которая принимает один аргумент, целое число , и возвращает целое число. int result; объявляет, что локальная переменная result является целым числом. В гипотетическом языке, поддерживающем вывод типов, код мог бы быть написан следующим образом:

add_one(x) {
    var result;  /* inferred-type variable result */
    var result2; /* inferred-type variable result #2 */

    result = x + 1;
    result2 = x + 1.0;  /* this line won't work (in the proposed language) */
    return result;
}

Это идентично написанию кода на языке Dart , за исключением того, что на него налагаются некоторые дополнительные ограничения, описанные ниже. Можно было бы определить типы всех переменных во время компиляции. В приведенном выше примере компилятор сделает вывод, что result и x иметь целочисленный тип, поскольку константа 1 является целочисленным типом, и, следовательно, что add_one это функция int -> int. Переменная result2 не используется юридически, поэтому у него не будет типа.

На воображаемом языке, на котором написан последний пример, компилятор предположил бы, что в отсутствие информации об обратном + принимает два целых числа и возвращает одно целое число. (Вот как это работает, например, в OCaml .) Из этого средство вывода типа может сделать вывод, что тип x + 1 является целым числом, что означает result является целым числом и, следовательно, возвращаемым значением add_one является целым числом. Аналогично, поскольку + требует, чтобы оба его аргумента были одного типа, x должно быть целым числом, и, следовательно, add_one принимает одно целое число в качестве аргумента.

Однако в следующей строке result2 вычисляется путем добавления десятичной дроби. 1.0 с арифметикой с плавающей запятой , вызывая конфликт при использовании x как для целочисленных выражений, так и для выражений с плавающей запятой. Правильный алгоритм вывода типа для такой ситуации известен с 1958 года , а его правильность известна с 1982 года. Он пересматривает предыдущие выводы и с самого начала использует наиболее общий тип: в данном случае с плавающей запятой. Однако это может иметь пагубные последствия: например, использование чисел с плавающей запятой с самого начала может привести к проблемам с точностью, которых не было бы при использовании целочисленного типа.

Однако часто используются вырожденные алгоритмы вывода типа, которые не могут вернуться назад и вместо этого в такой ситуации генерируют сообщение об ошибке. Такое поведение может быть предпочтительнее, поскольку вывод типа не всегда может быть нейтральным с точки зрения алгоритма, как показано в предыдущей проблеме точности с плавающей запятой.

Алгоритм промежуточной общности неявно объявляет result2 как переменную с плавающей запятой, а сложение неявно преобразует x до плавающей точки. Это может быть правильно, если контексты вызова никогда не предоставляют аргумент с плавающей запятой. Такая ситуация показывает разницу между выводом типа , который не предполагает преобразование типа , и неявным преобразованием типа , которое принудительно приводит данные к другому типу данных, часто без ограничений.

Наконец, существенным недостатком сложного алгоритма вывода типа является то, что результирующее разрешение вывода типа не будет очевидным для людей (особенно из-за обратного отслеживания), что может быть вредным, поскольку код в первую очередь предназначен для понимания людьми.

Недавнее появление JIT-компиляции позволяет использовать гибридные подходы, при которых тип аргументов, предоставляемых различным контекстом вызова, известен во время компиляции и может генерировать большое количество скомпилированных версий одной и той же функции. Каждую скомпилированную версию затем можно оптимизировать для другого набора типов. Например, JIT-компиляция позволяет иметь как минимум две скомпилированные версии add_one :

Версия, которая принимает целочисленные входные данные и использует неявное преобразование типов.

Версия, которая принимает в качестве входных данных число с плавающей запятой и повсюду использует инструкции с плавающей запятой.

Техническое описание

Вывод типа — это возможность автоматически определять, частично или полностью, тип выражения во время компиляции. Компилятор часто может определить тип переменной или сигнатуру типа функции без явных аннотаций типа. Во многих случаях можно полностью исключить аннотации типов из программы, если система вывода типов достаточно надежна или программа или язык достаточно просты.

Чтобы получить информацию, необходимую для вывода типа выражения, компилятор либо собирает эту информацию в виде совокупности и последующего сокращения аннотаций типов, данных для его подвыражений, либо посредством неявного понимания типа различных атомарных значений (например, true: Логическое значение; 42: Целое число; 3,14159: Действительное и т. д.). Именно благодаря распознаванию возможного сведения выражений к неявно типизированным атомарным значениям компилятор языка вывода типов может скомпилировать программу полностью без аннотаций типов.

В сложных формах программирования высшего порядка и полиморфизма компилятор не всегда может сделать такой вывод, и для устранения неоднозначности иногда необходимы аннотации типов. Например, известно, что вывод типа с помощью полиморфной рекурсии неразрешим. Более того, явные аннотации типов могут использоваться для оптимизации кода, заставляя компилятор использовать более конкретный (более быстрый/меньший) тип, чем он предполагал. ^[14]

Некоторые методы вывода типа основаны на удовлетворении ограничений. ^[15] или теории выполнимости по модулю . ^[16]

Пример высокого уровня

Например, Haskell функция map применяет функцию к каждому элементу списка и может быть определена как:

map f [] = []
map f (first:rest) = f first : map f rest

Введите вывод на map функция происходит следующим образом. map является функцией двух аргументов, поэтому ее тип ограничен формой a -> b -> c. В Haskell шаблоны [] и (first:rest) всегда соответствуют спискам, поэтому второй аргумент должен быть типом списка: b = [d] для какого-то типа d. Его первый аргумент f применяется аргументу к first, который должен иметь тип d, что соответствует типу в аргументе списка, поэтому f :: d -> e ( :: означает «имеет тип») для некоторого типа e. Возвращаемое значение map f, наконец, список чего угодно f производит, поэтому [e].

Соединение частей вместе приводит к map :: (d -> e) -> [d] -> [e]. В переменных типа нет ничего особенного, поэтому их можно переименовать как

map :: (a -> b) -> [a] -> [b]

Оказывается, это также самый общий тип, поскольку никаких дополнительных ограничений не применяется. В качестве предполагаемого типа map , параметрически полиморфен тип аргументов и результатов f не выводятся, а оставляются как переменные типа, и поэтому map может применяться к функциям и спискам различных типов, при условии, что фактические типы совпадают при каждом вызове.

Подробный пример

Алгоритмы, используемые такими программами, как компиляторы, эквивалентны приведенным выше неформально структурированным рассуждениям, но немного более многословны и методичны. Мы снова начнем с определения map:

map f [] = []
map f (first:rest) = f first : map f rest

Сначала мы создаем новые переменные типа для каждого отдельного термина:

α обозначает тип map что мы хотим сделать вывод.
β обозначает тип f в первом уравнении.
[γ] обозначает тип [] в левой части первого уравнения.
[δ] обозначает тип [] в правой части первого уравнения.
ε обозначает тип f во втором уравнении.
ζ -> [ζ] -> [ζ] обозначает тип : в левой части первого уравнения. (Этот шаблон известен из его определения.)
η обозначает тип first.
θ обозначает тип rest.
ι -> [ι] -> [ι] обозначает тип : в правой части первого уравнения.

Затем мы создаем новые переменные типа для подвыражений, построенных на основе этих терминов, соответствующим образом ограничивая тип вызываемой функции:

κ обозначает тип map f []. Мы заключаем, что α ~ β -> [γ] -> κ где символ "похожий" ~ означает «объединяется с»; мы говорим, что α, тип map, должен быть совместим с типом функции, принимающей β и список γs и возвращая κ.
λ обозначает тип (first:rest). Мы заключаем, что ζ -> [ζ] -> [ζ] ~ η -> θ -> λ.
μ обозначает тип map f (first:rest). Мы заключаем, что α ~ ε -> λ -> μ.
ν обозначает тип f first. Мы заключаем, что ε ~ η -> ν.
ξ обозначает тип map f rest. Мы заключаем, что α ~ ε -> θ -> ξ.
ο обозначает тип f first : map f rest. Мы заключаем, что ι -> [ι] -> [ι] ~ ν -> ξ -> ο.

Мы также ограничиваем левую и правую части каждого уравнения единством друг с другом: κ ~ [δ] и μ ~ ο. В целом система унификаций, которую необходимо решить, такова:

α ~ β -> [γ] -> κ
ζ -> [ζ] -> [ζ] ~ η -> θ -> λ
α ~ ε -> λ -> μ
ε ~ η -> ν
α ~ ε -> θ -> ξ
ι -> [ι] -> [ι] ~ ν -> ξ -> ο
κ ~ [δ]
μ ~ ο

Затем мы заменяем до тех пор, пока больше нельзя будет исключить переменные. Точный порядок не имеет значения; если код проверяет тип, любой порядок приведет к одной и той же окончательной форме. Начнем с замены ο для μ и [δ] для κ:

α ~ β -> [γ] -> [δ]
ζ -> [ζ] -> [ζ] ~ η -> θ -> λ
α ~ ε -> λ -> ο
ε ~ η -> ν
α ~ ε -> θ -> ξ
ι -> [ι] -> [ι] ~ ν -> ξ -> ο

Замена ζ для η, [ζ] для θ и λ, ι для ν, и [ι] для ξ и ο, все возможно, потому что конструктор типа, такой как · -> · обратима по своим аргументам :

α ~ β -> [γ] -> [δ]
α ~ ε -> [ζ] -> [ι]
ε ~ ζ -> ι

Замена ζ -> ι для ε и β -> [γ] -> [δ] для α, сохраняя второе ограничение, чтобы мы могли восстановить α в конце:

α ~ (ζ -> ι) -> [ζ] -> [ι]
β -> [γ] -> [δ] ~ (ζ -> ι) -> [ζ] -> [ι]

И, наконец, замена (ζ -> ι) для β а также ζ для γ и ι для δ потому что конструктор типа, такой как [·] является обратимым, исключает все переменные, специфичные для второго ограничения:

α ~ (ζ -> ι) -> [ζ] -> [ι]

Замены больше невозможны, и изменение маркировки дает нам map :: (a -> b) -> [a] -> [b], то же самое, что мы нашли, не вдаваясь в эти подробности.

Алгоритм вывода типа Хиндли – Милнера

Алгоритм, впервые использованный для вывода типа, теперь неофициально называется алгоритмом Хиндли-Милнера, хотя по праву этот алгоритм следует приписать Дамасу и Милнеру. ^[17] Ее также традиционно называют реконструкцией типа . ^[1]^: 320 Если термин правильно типизирован в соответствии с правилами типизации Хиндли-Милнера, то эти правила генерируют основную типизацию для этого термина. Процесс обнаружения этой основной типизации — это процесс «реконструкции».

Происхождением этого алгоритма является алгоритм вывода типа для просто типизированного лямбда-исчисления , который был разработан Хаскеллом Карри и Робертом Фейсом в 1958 году. ^{[ нужна ссылка ]} В 1969 году Дж. Роджер Хиндли расширил эту работу и доказал, что их алгоритм всегда выводит наиболее общий тип. В 1978 году Робин Милнер ^[18] независимо от работы Хиндли предоставил эквивалентный алгоритм, алгоритм W. В 1982 году Луис Дамас ^[17] наконец доказал, что алгоритм Милнера является полным, и расширил его для поддержки систем с полиморфными ссылками.

Побочные эффекты использования самого общего типа

По замыслу вывод типа, особенно правильный (с обратным отслеживанием) вывод типа, предполагает использование наиболее общего подходящего типа, однако это может иметь последствия, поскольку более общие типы не всегда могут быть алгоритмически нейтральными, типичными случаями являются:

число с плавающей запятой рассматривается как общий тип целого числа, тогда как число с плавающей запятой приводит к проблемам с точностью
вариантные/динамические типы рассматриваются как общий тип других типов, что вводит правила приведения и сравнения, которые могут быть разными, например, такие типы используют оператор «+» как для числового сложения, так и для конкатенации строк, но какая операция выполняется: определяется динамически, а не статически

Вывод типов для естественных языков

Алгоритмы вывода типов использовались для анализа естественных языков , а также языков программирования. ^[19]^[20]^[21] Алгоритмы вывода типа также используются в некоторых грамматических индукциях. ^[22]^[23] и грамматические системы на основе ограничений для естественных языков. ^[24]

Ссылки

^ Перейти обратно: ^а ^б Бенджамин К. Пирс (2002). Типы и языки программирования . МТИ Пресс. ISBN 978-0-262-16209-8 .
^ «WG14-N3007: Вывод типа для определений объектов» . open-std.org . 10.06.2022. Архивировано из оригинала 24 декабря 2022 года.
^ «Спецификаторы типа заполнителя (начиная с C++11) — cppreference.com» . ru.cppreference.com . Проверено 15 августа 2021 г.
^ Картермп. «Вывод типа — F#» . docs.microsoft.com . Проверено 21 ноября 2020 г.
^ «Вывод · Язык Джулии» . docs.julialang.org . Проверено 21 ноября 2020 г.
^ «Спецификация языка Котлин» . kotlinlang.org . Проверено 28 июня 2021 г.
^ «Заявления — Справочник по Rust» . doc.rust-lang.org . Проверено 28 июня 2021 г.
^ «Вывод типа» . Документация Скала . Проверено 21 ноября 2020 г.
^ «Основы — язык программирования Swift (Swift 5.5)» . docs.swift.org . Проверено 28 июня 2021 г.
^ «Документация — Вывод типа» . www.typescriptlang.org . Проверено 21 ноября 2020 г.
^ «Проекты/Вала/Руководство — GNOME Wiki!» . Wiki.gnome.org . Проверено 28 июня 2021 г.
^ «Система типов Дарт» . dart.dev . Проверено 21 ноября 2020 г.
^ Кэтлин Доллард. «Вывод локального типа — Visual Basic» . docs.microsoft.com . Проверено 28 июня 2021 г.
^ Брайан О'Салливан; Дон Стюарт; Джон Герзен (2008). «Глава 25. Профилирование и оптимизация» . Реальный мир Haskell . О'Рейли.
^ Тальпен, Жан-Пьер и Пьер Жувело. « Полиморфный тип, область и вывод эффекта ». Журнал функционального программирования 2.3 (1992): 245-271.
^ Хасан, Мостафа; Урбан, Катерина; Эйлерс, Марко; Мюллер, Питер (2018). «Вывод типов на основе MaxSMT для Python 3» . Компьютерная проверка . Конспекты лекций по информатике. Том. 10982. стр. 12–19. дои : 10.1007/978-3-319-96142-2_2 . ISBN 978-3-319-96141-5 .
^ Перейти обратно: ^а ^б Дамас, Луис; Милнер, Робин (1982), «Основные схемы типов для функциональных программ», POPL '82: Материалы 9-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования (PDF) , ACM, стр. 207–212.
^ Милнер, Робин (1978), «Теория полиморфизма типов в программировании», Журнал компьютерных и системных наук , 17 (3): 348–375, doi : 10.1016/0022-0000(78)90014-4 , hdl : 20.500 .11820/d16745d7-f113-44f0-a7a3-687c2b709f66
^ Центр, Искусственный интеллект. Синтаксический анализ и вывод типов для естественных и компьютерных языков. Архивировано 4 июля 2012 г. на Wayback Machine . Дисс. Стэнфордский университет, 1989 год.
^ Эмеле, Мартин С. и Реми Заяк. « Типизированные грамматики объединения. Архивировано 5 февраля 2018 г. в Wayback Machine ». Материалы 13-й конференции по компьютерной лингвистике. Том 3. Ассоциация компьютерной лингвистики, 1990.
^ Парески, Ремо. « Типовый анализ естественного языка ». (1988).
^ Фишер, Кэтлин и др. «Фишер, Кэтлин и др. « От грязи до лопат: полностью автоматическое создание инструментов на основе специальных данных ». Уведомления ACM SIGPLAN. Том 43. № 1. ACM, 2008». Уведомления ACM SIGPLAN. Том. 43. № 1. АКМ, 2008.
^ Лаппин, Шалом; Шибер, Стюарт М. (2007). «Теория и практика машинного обучения как источник понимания универсальной грамматики» (PDF) . Журнал лингвистики . 43 (2): 393–427. дои : 10.1017/s0022226707004628 . S2CID 215762538 .
^ Стюарт М. Шибер (1992). Грамматические формализмы, основанные на ограничениях: синтаксический анализ и вывод типов для естественных и компьютерных языков . МТИ Пресс. ISBN 978-0-262-19324-5 .

Внешние ссылки

Архивное электронное письмо Роджера Хиндли, объясняющее историю вывода типов.
Вывод полиморфного типа Майкла Шварцбаха дает обзор вывода полиморфного типа.
Базовая статья Луки Карделли по проверке типов, описывает алгоритм и включает реализацию в Modula-2.
Реализация вывода типа Хиндли-Милнера в Scala , Эндрю Форрест (получено 30 июля 2009 г.)
Реализация Хиндли-Милнера в Perl 5, Никита Борисов в Wayback Machine (архивировано 18 февраля 2007 г.)
Что такое Хиндли-Милнер? (и почему это круто?) Объясняет Хиндли-Милнер, примеры на Scala

[TAPL-1] Перейти обратно: ^а ^б Бенджамин К. Пирс (2002). Типы и языки программирования . МТИ Пресс. ISBN 978-0-262-16209-8 .

[2] «WG14-N3007: Вывод типа для определений объектов» . open-std.org . 10.06.2022. Архивировано из оригинала 24 декабря 2022 года.

[3] «Спецификаторы типа заполнителя (начиная с C++11) — cppreference.com» . ru.cppreference.com . Проверено 15 августа 2021 г.

[4] Картермп. «Вывод типа — F#» . docs.microsoft.com . Проверено 21 ноября 2020 г.

[5] «Вывод · Язык Джулии» . docs.julialang.org . Проверено 21 ноября 2020 г.

[6] «Спецификация языка Котлин» . kotlinlang.org . Проверено 28 июня 2021 г.

[7] «Заявления — Справочник по Rust» . doc.rust-lang.org . Проверено 28 июня 2021 г.

[8] «Вывод типа» . Документация Скала . Проверено 21 ноября 2020 г.

[9] «Основы — язык программирования Swift (Swift 5.5)» . docs.swift.org . Проверено 28 июня 2021 г.

[10] «Документация — Вывод типа» . www.typescriptlang.org . Проверено 21 ноября 2020 г.

[11] «Проекты/Вала/Руководство — GNOME Wiki!» . Wiki.gnome.org . Проверено 28 июня 2021 г.

[12] «Система типов Дарт» . dart.dev . Проверено 21 ноября 2020 г.

[13] Кэтлин Доллард. «Вывод локального типа — Visual Basic» . docs.microsoft.com . Проверено 28 июня 2021 г.

[14] Брайан О'Салливан; Дон Стюарт; Джон Герзен (2008). «Глава 25. Профилирование и оптимизация» . Реальный мир Haskell . О'Рейли.

[15] Тальпен, Жан-Пьер и Пьер Жувело. « Полиморфный тип, область и вывод эффекта ». Журнал функционального программирования 2.3 (1992): 245-271.

[16] Хасан, Мостафа; Урбан, Катерина; Эйлерс, Марко; Мюллер, Питер (2018). «Вывод типов на основе MaxSMT для Python 3» . Компьютерная проверка . Конспекты лекций по информатике. Том. 10982. стр. 12–19. дои : 10.1007/978-3-319-96142-2_2 . ISBN 978-3-319-96141-5 .

[Damas-and-Milner-1982-17] Перейти обратно: ^а ^б Дамас, Луис; Милнер, Робин (1982), «Основные схемы типов для функциональных программ», POPL '82: Материалы 9-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования (PDF) , ACM, стр. 207–212.

[18] Милнер, Робин (1978), «Теория полиморфизма типов в программировании», Журнал компьютерных и системных наук , 17 (3): 348–375, doi : 10.1016/0022-0000(78)90014-4 , hdl : 20.500 .11820/d16745d7-f113-44f0-a7a3-687c2b709f66

[19] Центр, Искусственный интеллект. Синтаксический анализ и вывод типов для естественных и компьютерных языков. Архивировано 4 июля 2012 г. на Wayback Machine . Дисс. Стэнфордский университет, 1989 год.

[20] Эмеле, Мартин С. и Реми Заяк. « Типизированные грамматики объединения. Архивировано 5 февраля 2018 г. в Wayback Machine ». Материалы 13-й конференции по компьютерной лингвистике. Том 3. Ассоциация компьютерной лингвистики, 1990.

[21] Парески, Ремо. « Типовый анализ естественного языка ». (1988).

[22] Фишер, Кэтлин и др. «Фишер, Кэтлин и др. « От грязи до лопат: полностью автоматическое создание инструментов на основе специальных данных ». Уведомления ACM SIGPLAN. Том 43. № 1. ACM, 2008». Уведомления ACM SIGPLAN. Том. 43. № 1. АКМ, 2008.

[23] Лаппин, Шалом; Шибер, Стюарт М. (2007). «Теория и практика машинного обучения как источник понимания универсальной грамматики» (PDF) . Журнал лингвистики . 43 (2): 393–427. дои : 10.1017/s0022226707004628 . S2CID 215762538 .

[Shieber1992-24] Стюарт М. Шибер (1992). Грамматические формализмы, основанные на ограничениях: синтаксический анализ и вывод типов для естественных и компьютерных языков . МТИ Пресс. ISBN 978-0-262-19324-5 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]