 In theoretical computer science, currying provides a way to study functions with multiple arguments in very simple theoretical models, such as the lambda calculus, in which functions only take a single argument.Consider a function formula_116 taking two arguments, and having the type formula_117, which should be understood to mean that "x" must have the type formula_3, "y" must have the type formula_4, and the function itself returns the type formula_57.The curried form of "f" is defined as

where formula_122 is the abstractor of lambda calculus.