This is about functionals in the sense of higher-order logic, which is the original sense and which has only that name. For functionals in the sense of functional analysis, see linear functional; for the relation between these, see under Examples below. For functionals on infinite-dimensional manifolds, see at nonlinear functional.
In a type theory with function types, given a type , a functional of base type is a term of type aka . This should be distinguished from (on the one hand) an operator, which is a term of type aka , and (on the other hand) a function, which (in this context) is a term of type aka .
More generally, any term whose type has the form aka may be called a functional, although usually not if any of these types is very trivial (since any type has this form, up to equivalence, if ).
Although one typically interprets type theory within set theory so that operations between types become functions, one may also use partial functions, which is necessary for many of the examples below.
In variational calculus one studies functions on spaces of sections of jet bundles or other mapping spaces. The notion of nonlinear functional is an abstraction of this. For example, such functionals appear in physics as action functionals. See covariant phase space and path integral for other functionals in physics.
If we interpret as the real line, then consists of real-valued maps of a real variable, which form a vector space. The linear maps from to are the original linear functionals. In functional analysis, we now replace with an arbitrary topological vector space (originally but no longer necessarily taken to be a subspace? of ) and consider linear maps from to instead; so these linear functionals are actually unstructured operations in a type-theoretic sense.