 | This article includes a list of references, related reading, or external links, but its sources remain unclear because it lacks inline citations. Please help improve this article by introducing more precise citations. (January 2025) (Learn how and when to remove this message) |
In type theory, a type system has the property of subject reduction (also subject evaluation, type preservation or simply preservation) if evaluation of expressions does not cause their type to change. Formally, if ⊢ e1 : τ and e1 → e2 then ⊢ e2 : τ. Intuitively, this means one would not like to write a expression, in say Haskell, of type Int, and have it evaluate to a value v, only to find out that v is a string.
Together with progress, it is an important meta-theoretical property for establishing type soundness of a type system.
The opposite property, if Γ ⊢ e2 : τ and e1 → e2 then Γ ⊢ e1 : τ, is called subject expansion. It often does not hold as evaluation can erase ill-typed sub-terms of an expression, resulting in a well-typed one.
References
- Wright, Andrew K.; Felleisen, Matthias (1994). "A Syntactic Approach to Type Soundness". Information and Computation. 115 (1): 38–94. doi:10.1006/inco.1994.1093. S2CID 31415217.
- Pierce, Benjamin C. (2002). "8.3 Safety=Progress + Preservation". Types and Programming Languages. MIT Press. pp. 95–98. ISBN 0262162091. LCCN 2001044428.
This programming language theory or type theory-related article is a stub. You can help Misplaced Pages by expanding it. |
