Function types

A function type is a set of morphisms between two objects in a category CC. This set is called the hom-set C(a,b)SetC(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 SetSet or HaskHask.

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 zz for the function type, some aa for the argument type and some bb 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×az \times a (which is an object in some category) to some other object bb in the category. In full (z×a)gb(z \times a) \xrightarrow {g} b where gg is the morphism.

If we think in terms of the category SetSet (or more specifically for our purposes, HaskHask) then the object zz is the set of all function types, while the objects aa and bb are, respectively, the sets of argument and return types. Note that for fzf \in z and xax \in a we have some ybf(x)by \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 zz to be the best candidate if for (z×a)gb(z \times a) \xrightarrow {g} b there is a unique morphism zhzz' \xrightarrow {h} z such that the application of gg' factorizes through the application of gg.

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

Therefore our zz 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    ba \implies b that together with the morphism evaleval factors some gg through the unique morphism zh(a    b)z \xrightarrow {h} (a \implies b).

g=eval(h×id)g = eval \circ (h \times id)

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

This is really currying

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

Additionally the universal property tells us that for every gg there is a unique morphism zh(a    b)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 hh is a function of one argument zz that returns a function aba \rightarrow b. It is a higher order function. This shows the equivalence of hh and gg which is called currying where hh is the curried version of gg. Conversely, given the unique hh we can always construct gg which is the uncurried version of h:

g=eval(h×id)g = eval \circ (h \times id)

Function types are exponentials

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

An object from BoolBool is defined by a pair TrueTrue and FalseFalse). Let's say we map this to a hypothetical CharChar which has 256 possible values (in Haskell the CharChar 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 CharBool=2562Char^{Bool} = 256^2.

The laws of exponents map directly to types.