A function type is a set of morphisms between two objects in a category $C$. This set is called the hom-set $C(a,b) \in Set$.

Function types are special because they live in the same category as the objects they map which for our use case is $Set$ or $Hask$.

A function type has an input type and a return type, so it is a composite type. Here we attempt to use a universal construction to create a function type which is a pattern that involves three objects; the function type itself, the argument type and the return type.

This pattern is function application. We simply apply the function to the argument in order to get the return type. To begin this universal construction we take some $z$ for the function type, some $a$ for the argument type and some $b$ for the return type. These are all objects because we are expressing this construction in terms of arbitrary categories.

The function application itself is a mapping from the product of the function type and the argument type $z \times a$ (which is an object in some category) to some other object $b$ in the category. In full $(z \times a) \xrightarrow {g} b$ where $g$ is the morphism.

If we think in terms of the category $Set$ (or more specifically for our purposes, $Hask$) then the object $z$ is the set of all function types, while the objects $a$ and $b$ are, respectively, the sets of argument and return types. Note that for $f \in z$ and $x \in a$ we have some $y \in b \equiv f (x) \in b$.

This pattern doesn't exist in every category, but it does exist in the categories of interest to programmers. Also, this only exists in those categories which have products for all pairs of objects.

As we saw in the universal constructions of product and coproduct we need to find the best candidate for the function type. That means there is a unique mapping between these candidates and our pattern (which we take to be the best candidate). In this case we take $z$ to be the best candidate if for $(z \times a) \xrightarrow {g} b$ there is a unique morphism $z' \xrightarrow {h} z$ such that the application of $g'$ factorizes through the application of $g$.

We really need to close the diagram through a morphism from $z' \times a$ to $z \times a$ which is possible because the product is a bifunctor and so we can use the morphism $h \times id$ which leads to the factorization $g' = g \circ (h \times id)$.

Therefore our $z$ is the best candidate, and so we do some renaming as in the diagram below:

Which gives us the formal definition of the universal function object $a \implies b$ that together with the morphism $eval$ factors some $g$ through the unique morphism $z \xrightarrow {h} (a \implies b)$.

This function object doesn't exist for any pair of objects in any given category but it does always exist in the category $Set$, and therefore also in $Hask$.

This is really currying

Think of the morphism $(z \times a) \xrightarrow {g} b$ as a function in two arguments. In fact, in $Set$ (and $Hask$), this is exactly the function $g$ from a pair of objects (which themselves are sets - types).

Additionally the universal property tells us that for every $g$ there is a unique morphism $z \xrightarrow {h} (a \implies b)$.

In the categories of interest to us as programmers, and given the above (in those categories) we know that $h$ is a function of one argument $z$ that returns a function $a \rightarrow b$. It is a higher order function. This shows the equivalence of $h$ and $g$ which is called currying where $h$ is the curried version of $g$. Conversely, given the unique $h$ we can always construct $g$ which is the uncurried version of h:

Function types are exponentials

What might seem bizarre at first actually makes a lot of sense. Given a function $a \rightarrow b$ we can define it's exponential as $b^a$. A function from $a$ has some set of values (possibly infinite in Haskell), and therefore for each of those we can multiply by the set of values in $b$. Remember we are dealing with objects that are actually sets as we are in our usual categories of interest.

An object from $Bool$ is defined by a pair $True$ and $False$). Let's say we map this to a hypothetical $Char$ which has 256 possible values (in Haskell the $Char$ type actually encodes Unicode). That means for every value of the argument type there are 256 possible values in the return type. Therefore the total is $Char^{Bool} = 256^2$.

The laws of exponents map directly to types.