Product types can generally be considered "built-in" in typed lambda calculi via currying.
Making use of currying, n-ary type operators can be (re)written as a sequence of applications of unary type operators.
For example, giving the structure of the simply-typed λ-calculus at the type level requires binding, or higher-order, type operators.
Combining type operators with the polymorphic λ-calculus (System F) yields System Fω.
Some functional programming languages make explicit use of type constructors.