 Simply typed lambda calculus is the internal language of cartesian closed categories; and it is for this reason that pairs and lists are the primary types in the type theory of LISP, scheme and many functional programming languages.By contrast, the product for monoidal categories (such as Hilbert space and the vector spaces of functional analysis) is the tensor product.The internal language of such categories is linear logic, a form of quantum logic; the corresponding type system is the linear type system.