 Type theory embodies a specific model of semantic compositionality in terms of functional application. According to this model, if two expressions x and y can concatenate into a meaningful expression xy, then (i), the meaning of one of these expressions is taken to be a function, (ii) the meaning of the other is taken to be an item of the kind that the function in question is defined for, and (iii) the meaning of xy is the output of the function when applied to the input. The type-theoretic representation of this meaning is written x(y) or y(x), depending on which expression is taken to be the function and which the input or argument. A functional application such as x(y) is said to be well-typed iff the input that y denotes is the type of input for which the function x is defined.