В теории типа , система типа обладает свойством уменьшения объекта (также оценка объекта , сохранение типа или просто сохранение ) , если оценка из выражений не вызывает их типа к изменению. Формально, если Γ ⊢ 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. CiteSeerX 10.1.1.44.5122 . DOI : 10.1006 / inco.1994.1093 .
- Пирс, Бенджамин С. (2002). «8.3 Безопасность = прогресс + сохранение». Типы и языки программирования . MIT Press. ISBN 978-0-262-16209-8.
Эта статья по теории языков программирования или теории типов незавершена . Вы можете помочь Википедии, расширив ее . |
