In formal semantics, a type shifter is an interpretation rule which changes an expression's semantic type. For instance, while the English expression "John" might ordinarily denote John himself, a type shifting rule called Lift can raise its denotation to a function which takes a property and returns "true" if John himself has that property. Lift can be seen as mapping an individual onto the principal ultrafilter which it generates.[1][2][3]

1. Without type shifting: ${\displaystyle \,\,[\![John]\!]=j}$
2. Type shifting with Lift: ${\displaystyle [\![John]\!]=\lambda P_{\langle e,t\rangle }.P(j)}$

Type shifters were proposed by Barbara Partee and Mats Rooth in 1983 to allow for systematic type ambiguity. Work of this period assumed that syntactic categories corresponded directly with semantic types and researchers thus had to "generalize to the worst case" when particular uses of particular expressions from a given category required an especially high type. Moreover, Partee argued that evidence in fact supported expressions having different types in different contexts. Thus, she and Rooth proposed type shifting as a principled mechanism for generating this ambiguity.[1][2][3]

Type shifters remain a standard tool in formal semantic work, particularly in categorial grammar and related frameworks. Type shifters have also been used to interpret quantifiers in object position and to capture scope ambiguities. In this regard, they serve as an alternative to syntactic operations such as quantifier raising used in mainstream generative approaches to semantics. [4][5] Type shifters have also been used to generate and compose alternative sets without the need to fully adopt an alternative-based semantics.[6][7]