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

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

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

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

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

1. Глава 30 (тип Умозаключение) из свободно доступной книги Плай , Языки программирования: применение и толкование , эскизы объединения на основе логического вывода типа.
2. Летний курс « Интерпретация типов как абстрактных значений» представляет изящные оценщики, средства проверки типов, реконструкторы типов и логические выводы, использующие Haskell в качестве метаязыка.
3. Глава 7 (Типы) книги EOPL , Основы языков программирования .
4. Глава 22 (Реконструкция типов) книги TAPL , Типы и языки программирования и соответствующие реализации OCaml recon и fullrecon .
5. Глава 13 (Реконструкция типов) новой книги DCPL , Design Concepts in Programming Languages .
6. Подборка научных статей .
7. TypeInference компилятора закрытия является примером подхода анализа потока данных к выводу типов, который лучше подходит для динамических языков, чем подход Хиндлера Милнера.

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

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

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

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

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

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

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

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

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

http://www.plai.org/

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

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

(if (= 1 2) 
    1 
    2)

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

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

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

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

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

Я нашел этот ресурс чрезвычайно полезным, чтобы связать алгоритмы 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, closure), он работает с абстрактными значениями, также известными как типы (int, bool и т. Д.). Поскольку он интерпретирует программу на абстрактных значениях, поэтому он называется абстрактной интерпретацией.

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

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

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