Реализация вывода типа
Я вижу некоторые интересные дискуссии о статической и динамической типизации. Я обычно предпочитаю статическую типизацию из-за проверки типов компиляции, лучшего документированного кода и т. Д. Однако я согласен, что они загромождают код, если это делается, например, в Java.
Итак, я собираюсь начать создавать собственный язык функциональных стилей, и вывод типов - это одна из вещей, которую я хочу реализовать. Я понимаю, что это большая тема, и я не пытаюсь создать что-то, что не было сделано раньше, просто базовые выводы...
Любые указатели на то, что читать, которые помогут мне в этом? Желательно что-то более прагматичное / практическое, а не более теоретические тексты теории категорий / теории типов. Если есть текст обсуждения реализации со структурами данных / алгоритмами, это было бы просто замечательно.
5 ответов
Я нашел следующие ресурсы полезными для понимания вывода типов в порядке возрастания сложности:
- Глава 30 (Вывод типа) свободно доступной книги PLAI, Языки программирования: применение и интерпретация, делает наброски логического вывода типа унификации.
- Летний курс " Интерпретация типов как абстрактных значений" представляет элегантные оценщики, средства проверки типов, средства восстановления типов и средства вывода, использующие Haskell в качестве метаязыка.
- Глава 7 (Типы) книги EOPL, Основы языков программирования.
- Глава 22 (Реконструкция типов) книги TAPL, Типы и языки программирования, и соответствующие реализации OCamlconcon и fullrecon.
- Глава 13 (Реконструкция типов) новой книги DCPL, Концепции проектирования в языках программирования.
- Подборка академических работ.
- Type Inference компилятора закрытия является примером подхода анализа потока данных к выводу типа, который лучше подходит для динамических языков, чем подход Хиндлера Милнера.
Однако, поскольку лучший способ обучения - это делать, я настоятельно рекомендую реализовать вывод типа для игрушечного функционального языка, выполняя домашнее задание курса языков программирования.
Я рекомендую эти две доступные домашние работы в ML, которые вы можете выполнить менее чем за день:
- PCF Interpreter ( решение) для разогрева.
- Вывод типа PCF ( решение) для реализации алгоритма W для вывода типа Хиндли-Милнера.
Эти задания взяты из более продвинутого курса:
К сожалению, большая часть литературы по этому вопросу очень плотная. Я тоже был на твоем месте. Я впервые познакомился с предметом из раздела Языки программирования: приложения и интерпретация
Я постараюсь обобщить абстрактную идею с последующими подробностями, которые я не нашел сразу очевидными. Во-первых, можно предположить, что вывод типа создает и затем решает ограничения. Чтобы сгенерировать ограничения, вы проходите через синтаксическое дерево и генерируете одно или несколько ограничений для каждого узла. Например, если узел является оператором "+", операнды и результаты должны быть числами. Узел, который применяет функцию, имеет тот же тип, что и результат функции, и так далее.
Для языка без '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
Я надеюсь, что это помогает прояснить немного темный мир.
В дополнение к Хиндли Милнеру для функциональных языков, еще один популярный подход к выводу типов для динамического языка abstract interpretation,
Идея абстрактной интерпретации состоит в том, чтобы написать специальный интерпретатор для языка, вместо того, чтобы поддерживать среду конкретных значений (1, false, замыкание), он работает с абстрактными значениями, такими как типы (int, bool и т. Д.). Поскольку она интерпретирует программу на абстрактных значениях, поэтому она называется абстрактной интерпретацией.
Pysonar2 - это элегантная реализация абстрактной интерпретации для Python. Он используется Google для анализа проектов Python. В основном это использует visitor pattern для отправки оценочного вызова соответствующему узлу AST. Функция посетителя transform принимает context в котором текущий узел будет оцениваться и возвращает тип текущего узла.