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

Question

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

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

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

Answer 1

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

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

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

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

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

Эти задания взяты из более продвинутого курса:

1. Реализация MiniML

2. Полиморфные, экзистенциальные, рекурсивные типы (PDF)

3. Двунаправленная проверка типов (PDF)

4. Подтипы и объекты (PDF)

Answer 2

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

http://www.plai.org/

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

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

(if (= 1 2) 
    1 
    2)

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

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

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

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

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

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

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

Многие другие бумаги тоже хороши:

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

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

Answer 3

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

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

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

Answer 4

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

Answer 5

Лямбда Предельная, начиная с здесь .