Реализация вывода типа

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

Итак, я собираюсь начать собственный язык функционального стиля, и тип вывода - одна из тех вещей, которые я хочу реализовать. Я понимаю, что это большая тема, и я не пытаюсь создать что-то, чего раньше не было, просто базовые выводы...

Любые указатели на то, что читать, что поможет мне в этом? Предпочтительно что-то более прагматичное/практическое, в отличие от более теоретических теорий теории теории/текстов теории типов. Если там будет текст обсуждения реализации, с структурами данных/алгоритмами, это будет просто прекрасно.

Ответ 1

Я нашел следующие ресурсы полезными для понимания вывода типа в порядке возрастания сложности:

Глава 30 (вывод типа) свободно доступная книга PLAI, Языки программирования: приложение и интерпретация, эскизы на основе унифицированного вывода типа.
Летний курс Интерпретация типов как абстрактных значений представляет элегантных оценщиков, контролеров типов, типов реконструировщиков и указателей, использующих Haskell в качестве метаязыка.
Глава 7 (Типы) книга EOPL, Основы языков программирования.
Глава 22 (Реконструкция типа) книга TAPL, Типы и языки программирования и соответствующие реализации OCaml recon и fullrecon.
Глава 13 (Реконструкция типа) новая книга DCPL, Концепции дизайна на языках программирования.
Выбор академических работ.
Closure compiler TypeInference является примером подхода анализа потока данных для вывода типа, который лучше подходит для динамических языков, Подход Хиндлера Милнера.

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

Я рекомендую эти две доступные домашние задания в ML, которые вы можете выполнить как минимум за один день:

PCF Interpreter (решение), чтобы разогреться.
Вывод типа PCF (решение) для реализации алгоритм W для вывода типа Хиндли-Милнера.

Эти присвоения относятся к более продвинутому курсу:

Ответ 2

Несчастливо, что большая часть литературы по этому вопросу очень плотная. Я тоже был в твоей обуви. Я получил свое первое знакомство с предметом на языках программирования: приложения и интерпретация

http://www.plai.org/

Я попытаюсь обобщить абстрактную идею, за которой последуют детали, которые я не нашел сразу очевидными. Во-первых, вывод типа можно рассматривать как генерирование, а затем решение ограничений. Чтобы генерировать ограничения, вы рекурсируете через дерево синтаксиса и генерируете одно или несколько ограничений для каждого node. Например, если node является оператором '+', то операнды и результаты должны быть числами. A node, который применяет функцию, имеет тот же тип, что и результат функции, и т.д.

Для языка без 'let', вы можете вслепую решить вышеупомянутые ограничения путем подстановки. Например:

(if (= 1 2) 
    1 
    2)

здесь мы можем сказать, что условие оператора if должно быть логическим и что тип оператора if совпадает с типом его предложений "then" и "else". Поскольку мы знаем, что 1 и 2 являются числами, путем подстановки мы знаем, что оператор "if" - это число.

Где что-то неприятно, и то, что я не мог понять какое-то время, имеет дело с let:

(let ((id (lambda (x) x)))
    (id id))

Здесь мы привязали 'id' к функции, которая возвращает все, что вы передали, иначе известная как функция идентификации. Проблема заключается в том, что тип параметра функции "x" различен при каждом использовании идентификатора. Второй "id" является функцией от a- > a, где a может быть любым. Первое из (a- > a) → (a- > a) Это известно как let-полиморфизм. Ключ заключается в разрешении ограничений в определенном порядке: сначала разрешите ограничения для определения "id" . Это будет a- > a. Затем новые, отдельные копии типа идентификатора могут быть заменены на ограничения для каждого места "id" , например a2- > a2 и a3- > a3.

Это не было легко объяснено в онлайн-ресурсах. Они упомянут алгоритм W или M, но не то, как они работают с точки зрения решения ограничений, или почему это не противоречит let-polymorphism: каждый из этих алгоритмов обеспечивает упорядочение при решении ограничений.

Я нашел этот ресурс чрезвычайно полезным для привязки алгоритма W, M и общей концепции генерации ограничений и решения всех проблем. Он немного плотный, но лучше, чем многие:

http://www.cs.uu.nl/research/techreps/repo/CS-2002/2002-031.pdf

Многие из других статей тоже хороши:

http://people.cs.uu.nl/bastiaan/papers.html

Я надеюсь, что это поможет прояснить несколько мутный мир.

Ответ 3

В дополнение к Hindley Milner для функциональных языков, другой популярным подходом к типу вывода для динамического языка является abstract interpretation.

Идея абстрактной интерпретации состоит в том, чтобы написать специальную переводчика для языка, вместо того чтобы поддерживать среду конкретные значения (1, ложь, замыкание), он работает с абстрактными значениями, ака типы (int, bool и т.д.). Поскольку он интерпретирует абстрактные значения, поэтому она называлась абстрактной интерпретацией.

Pysonar2 - элегантная реализация абстрактной интерпретации для Python. Он используется Google для анализа Python проекты. В основном используется visitor pattern для отправки запрос оценки к соответствующему AST node. Функция посетителя transform принимает context, в котором будет оцениваться текущий node, и возвращает тип тока node.

Ответ 4

Типы и языки программирования Бенджамина С. Пирса

Ответ 5

Lambda the Ultimate, начиная здесь.