System F - отличный способ просто рассуждать о типах при программировании прототипа. Помимо его реализации, я бы хотел использовать существующую реализацию.Что такое каноническая реализация System F?
При поиске реализаций, похоже, не существует - и я не уверен, почему.
Мой вопрос: Что такое каноническая реализация системы F?
Types and Programming Languages книга B.C. Пирс знаменит (среди прочего) для предоставления и обсуждения implementations типизированных лямбда-исчислений в OCaml.
Книга обеспечивает реализацию системы F, которая называется fullpoly и объясняет детали реализации в главе 25. fullpoly расширяет реализацию simply-typed лямбда-исчисления с булевы - simplebool.
Инструкции по созданию и исполнению этих инструкций и переводчиков можно найти here.
Я не уверен насчет «canonity», но вы можете взглянуть на реализации (в OCaml) по B.C. Пирс [здесь] (https://www.cis.upenn.edu/~bcpierce/tapl/checkers/fullpoly/) и [здесь] (https://www.cis.upenn.edu/~bcpierce/tapl/checkers/fullomega). Реализации описаны в его [TAPL] (https://www.cis.upenn.edu/~bcpierce/tapl/) книге. –
Прохладный - можете ли вы расширить это в ответ? – hawkeye
Хорошо, все готово. –