Я начинаю личное библиографическое исследование по алгоритмам проверки типов и хочу несколько советов. Какие алгоритмы, стратегии и общие методы проверки типов наиболее часто используются?
Меня особенно интересуют сложные алгоритмы проверки типов, которые были реализованы в широко известных строго статических типизированных языках, таких как, например, C ++, Java 5+, Scala или другие. IE, алгоритмы проверки типов, которые не очень просты из-за очень простой типизации базового языка (как Java 1.4 и ниже).
Я не интересуюсь конкретным языком X, Y или Z. Я интересуюсь алгоритмами проверки типов независимо от языка, на который они нацелены. Если вы предоставляете ответ типа «язык L, о котором вы никогда не слышали, который является строго типизированным, а типизация сложная, имеет алгоритм проверки типа, который выполняет A, B и C путем проверки X и Y с использованием алгоритма Z» или « Стратегия X и Y, используемая для Scala, и вариант Z для A, используемый для C #, хороши из-за функций R, S и T, которые работают таким образом », тогда ответы хороши.
источник
Ответы:
Большинство исследований фактически не публикуют алгоритмы проверки типов для полноценных языков программирования. Вы найдете некоторые формализации большей части систем типов для полных языков программирования, такие как работа, выполненная Drossopoulou и Eisenbach для Java, или работа Nipkov et al над C ++ . Чаще, тем не менее, вы найдете системы типов только для некоторой базовой части языка (например, Featherweight Java) или для основных понятий языка, таких как локальный подход к выводу типов в scala .
В таких конференциях, как POPL и ICFP, вы найдете множество алгоритмов проверки типов для конкретных типов систем типов и новые подходы, такие как проверка двунаправленного и трехнаправленного типа.
В более общем смысле, вам, вероятно, нужно знать об алгоритме Дамаса-Милнера , локальном выводе типов, проверке двунаправленного и трехнаправленного типа и расширяться оттуда, следуя ссылкам в статьях и используя google scholar, чтобы найти, какие документы ссылаются на них, и опираться на них. описанные подходы. Кроме того, как указано выше, на конференциях, таких как POPL, ICPF, ESOP и даже ECOOP и OOPSLA, будут представлены документы, соответствующие вашему квесту.
источник
Основным инструментом являются грамматики атрибутов . Возможно, вам не удастся сделать все, что вы можете себе представить, с ними, но они являются хорошей отправной точкой.
По сути, вы можете пройтись по абстрактному синтаксическому дереву программы сверху вниз и / или снизу вверх и передать информацию. Так, например, вы можете передавать информацию о типе глобальной области видимости (например, классы и их члены) вниз и рекурсивно определять тип выражений, то есть снизу вверх, передавая результирующие типы вверх.
Найдите некоторые объяснения и примеры на слайдах здесь (Глава 5).
источник