Сокращение темы
В теории типов система типов обладает свойством предметной редукции (также предметной оценки , сохранения типа или просто сохранения если оценка выражений ) , не приводит к изменению их типа . Формально, если ⊢ e 1 : τ и e 1 → e 2 , то ⊢ e 2 : τ . Интуитивно это означает, что не хотелось бы писать выражение, скажем, на Haskell , типа Int и вычислять его значение v только для того, чтобы обнаружить, что v является строкой.
Вместе с прогрессом это важное метатеоретическое свойство для установления правильности типов системы типов.
Противоположное свойство, если Γ ⊢ e 2 : τ и e 1 → e 2 , то Γ ⊢ e 1 : τ , называется субъектным расширением . Это часто не соответствует действительности, поскольку оценка может стереть неправильно типизированные подтермы выражения, в результате чего получится правильно типизированное выражение.
Ссылки
[ редактировать ]- Райт, Эндрю К.; Феллейзен, Матиас (1994). «Синтаксический подход к правильности типов» . Информация и вычисления . 115 (1): 38–94. дои : 10.1006/inco.1994.1093 . S2CID 31415217 .
- Пирс, Бенджамин К. (2002). «8.3 Безопасность = Прогресс + Сохранение». Типы и языки программирования . МТИ Пресс. стр. 95–98. ISBN 0262162091 . LCCN 2001044428 .
Эта теории языков программирования или теории типов, статья, посвященная незавершена . Вы можете помочь Википедии, расширив ее . |
