Какова каноническая реализация Системы F?
Система F - отличный способ просто рассуждать о типах при программировании прототипа. Помимо реализации этого, я бы хотел использовать существующую реализацию.
При поиске реализаций, кажется, их нет - и я не уверен почему.
Мой вопрос: какова каноническая реализация Системы F?
1 ответ
Решение
Книга BC Pierce " Типы и языки программирования" известна (помимо прочего) тем, что предоставляет и обсуждает реализации типизированных лямбда-исчислений в OCaml.
Книга предоставляет реализацию системы F, называемой fullpoly и объясняет детали реализации в Главе 25. fullpoly расширяет реализацию простейшего типа лямбда-исчисления с логическими значениями - simplebool,
Инструкции по созданию и выполнению этих проверок типов и интерпретаторов можно найти здесь.