The lambda calculus is Alonzo Church's model of computation. It consists of a simple language (variable, abstraction (lambda, represented as a \), and application) and semantics (beta reduction). Lambda terms reduce by beta reduction, which is a capture-avoiding substitution. For example, (\x.x x) \y.y --> \y.y \y.y. When a lambda term has multiple possible reductions, an evaluation strategy must be adopted. Common policies include applicative order, normal order, call by value, call by name, and call by need. A type theory is a discipline that imposes syntactic categories on lambda terms. In particular, every lambda bound variable is assigned a type that must match up with any argument to which the lambda abstraction is applied. In practice, this means a type theory can prohibit nonsensical terms such as 1+true. The simply-typed lambda calculus imposes a basic type theory. Types must be an arrow type (function type) or some applied type such as Int, Bool, Unit, etc. The simply-typed lambda calculus's type theory actually cannot assign types to a special lambda term called the fix-point operator: (\x.x x) (\x.x x). Languages such as Haskell uses a more sophisticated type theory called the Hindley-Milner type discipline which permits prenex polymorphism for terms bound by a let expression. Hindley-Milner also happens to be a type theory that admits type inference and thus programs do not need to have type-annotated terms to benefit to type theory guarantees of safety.