Тип стирания
В программирования языках стирание типов — это процесс во время загрузки , при котором явные аннотации типов удаляются из программы до ее выполнения во время выполнения . Операционная семантика, не требующая, чтобы программы сопровождались типами, называется семантикой стирания типов , в отличие от семантики передачи типов . Семантика стирания типов — это принцип абстракции , гарантирующий, что выполнение программы во время выполнения не зависит от информации о типе. В контексте обобщенного программирования противоположность стиранию типов называется реификацией . [1]
Вывод типа
[ редактировать ]Обратная операция называется выведением типа . Хотя стирание типов может быть простым способом определения типизации в неявно типизированных языках (неявно типизированный термин является правильно типизированным тогда и только тогда, когда это стирание правильно типизированного явно типизированного лямбда-терма ), оно не обеспечивает правила вывод по этому определению.
См. также
[ редактировать ]Ссылки
[ редактировать ]- ^ Лангер, Анжелика. «Что такое овеществление?» .
- Крари, Карл; Вейрих, Стефани ; Моррисетт, Грег (2002). «Интенсиональный полиморфизм в семантике стирания типов». Журнал функционального программирования . 12 (6): 567–600. CiteSeerX 10.1.1.5.4507 . дои : 10.1017/S0956796801004282 .