В информатике полиморфная рекурсия (также называемая типизацией Милнера - Майкрофта или исчислением Милнера-Майкрофта ) относится к рекурсивной параметрически полиморфной функции , где параметр типа изменяется с каждым рекурсивным вызовом, а не остается постоянным. Вывод типа для полиморфной рекурсии эквивалентен полуунификации и, следовательно, неразрешим и требует использования полуалгоритма или аннотаций типов , предоставляемых программистом .
Пример
Вложенные типы данных
Рассмотрим следующий вложенный тип данных в Haskell :
данные Вложенные a = a :<: ( Вложенные [ a ]) | Эпсилон инфиксr 5 :<: вложенный = 1 :<: [ 2 , 3 , 4 ] :<: [[ 5 , 6 ],[ 7 ],[ 8 , 9 ]] :<: Эпсилон
Функция длины, определенная для этого типа данных, будет полиморфно рекурсивной, поскольку тип аргумента изменяется с Nested aна Nested [a]в рекурсивном вызове:
длина :: Вложенный a -> Int длина Эпсилон = 0 длина ( _ :<: xs ) = 1 + длина xs
Обратите внимание, что Haskell обычно выводит сигнатуру типа для такой простой на вид функции, но здесь ее нельзя опустить, не вызвав ошибку типа.
Типы более высокого ранга
Приложения
Анализ программы
В анализе программ на основе типов полиморфная рекурсия часто необходима для получения высокой точности анализа. Известные примеры систем, использующих полиморфную рекурсию, включают анализ времени связывания Дюссара, Хенглейна и Моссина [2] и систему управления памятью на основе регионов Тофте–Талпина . [3] Поскольку эти системы предполагают, что выражения уже были типизированы в базовой системе типов (не обязательно использующей полиморфную рекурсию), вывод может быть снова сделан разрешимым.
Структуры данных, обнаружение ошибок, графические решения
Структуры данных функционального программирования часто используют полиморфную рекурсию для упрощения проверок ошибок типов и решения проблем с неприятными «промежуточными» временными решениями, которые пожирают память в более традиционных структурах данных, таких как деревья. В двух следующих цитатах Окасаки (стр. 144–146) приводит пример CONS в Haskell , в котором полиморфная система типов автоматически отмечает ошибки программиста. [4] Рекурсивный аспект заключается в том, что определение типа гарантирует, что самый внешний конструктор имеет один элемент, второй — пару, третий — пару пар и т. д. рекурсивно, устанавливая автоматический шаблон поиска ошибок в типе данных. Робертс (стр. 171) приводит связанный пример в Java , используя Class для представления стекового фрейма. Приведенный пример является решением проблемы Ханойской башни , в которой стек имитирует полиморфную рекурсию с начальной, временной и конечной вложенной структурой подстановки стека. [5]
Смотрите также
Примечания
- ^ Дюссар, Дирк; Хенглейн, Фриц; Моссин, Кристиан. «Полиморфная рекурсия и квалификации подтипов: анализ полиморфного времени связывания в полиномиальном времени». Труды 2-го Международного симпозиума по статическому анализу (SAS) . CiteSeerX 10.1.1.646.5884 .
- ^ Tofte, Mads ; Talpin, Jean-Pierre (1994). «Реализация типизированного λ-исчисления вызова по значению с использованием стека регионов». POPL '94: Труды 21-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования . Нью-Йорк, США: ACM. стр. 188–201. doi : 10.1145/174675.177855 . ISBN 0-89791-636-0.
- ^ Крис Окасаки (1999). Чисто функциональные структуры данных . Нью-Йорк: Кембридж. стр. 144. ISBN 978-0521663502.
- ^ Эрик Робертс (2006). Рекурсивное мышление с помощью Java . Нью-Йорк: Wiley. С. 171. ISBN 978-0471701460.
Дальнейшее чтение
- Меертенс, Ламберт (1983). "Инкрементальная полиморфная проверка типов в B" (PDF) . Симпозиум ACM по принципам языков программирования (POPL), Остин, Техас .
- Майкрофт, Алан (1984). «Полиморфные схемы типов и рекурсивные определения». Международный симпозиум по программированию, Тулуза, Франция . Конспект лекций по информатике. Том 167. С. 217–228. doi :10.1007/3-540-12925-1_41. ISBN 978-3-540-12925-7.
- Хенглейн, Фриц (1993). «Вывод типа с полиморфной рекурсией». Труды ACM по языкам и системам программирования . 15 (2): 253–289. CiteSeerX 10.1.1.42.3091 . doi :10.1145/169701.169692. S2CID 17411856.
- Kfoury, AJ; Tiuryn, J.; Urzyczyn, P. (апрель 1993 г.). «Реконструкция типов при наличии полиморфной рекурсии». ACM Transactions on Programming Languages and Systems . 15 (2): 290–311. doi : 10.1145/169701.169687 . ISSN 0164-0925. S2CID 18059949.
- Майкл И. Шварцбах (июнь 1995 г.). «Полиморфный вывод типа». Технический отчет BRICS-LS-95-3 .
- Эммс, Мартин; Лейсс, Ханс (1996). «Расширение проверки типов для SML с помощью полиморфной рекурсии — доказательство корректности». Технический отчет 96-101 .
- Ричард Берд и Ламберт Меертенс (1998). «Вложенные типы данных».
- C. Vasconcellos, L. Figueiredo, C. Camarao (2003). "Практический вывод типов для полиморфной рекурсии: реализация на Haskell [ мертвая ссылка ] ". Журнал универсальной компьютерной науки .
- Л. Фигейредо, К. Камарао. «Вывод типов для полиморфных рекурсивных определений: спецификация в Haskell».
- Hallett, J. J; Kfoury, AJ (июль 2005 г.). «Примеры программирования, требующие полиморфной рекурсии». Electronic Notes in Theoretical Computer Science . 136 : 57–102. doi : 10.1016/j.entcs.2005.06.014 . ISSN 1571-0661.
Внешние ссылки
