In formal semantics, a type shifter is an interpretation rule that changes an expression's semantic type. For instance, the English expression "John" might ordinarily denote John himself, but 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 that it generates.

1. Without type shifting: [ [ J o h n ] ] = j {\displaystyle \,\,[\![John]\!]=j}
2. Type shifting with Lift: [ [ J o h n ] ] = λ P ⟨ e , t ⟩ . P ( j ) {\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 the 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 the ambiguity.

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 that regard, they serve as an alternative to syntactic operations such as quantifier raising used in mainstream generative approaches to semantics. Type shifters have also been used to generate and compose alternative sets without the need to fully adopt an alternative-based semantics.