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

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

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

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

Ответы

Ответ 1

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

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

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

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

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

Ответ 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, начиная здесь.