How does the category theory represent that each function (each morphism) has a function type (an object)?

Question

In Haskell, the collection of all the types form a category named Hask.

In the category, objects are types, including function types. Morphisms are functions between types.

How does the category theory represent that each function (each morphism) has a function type (an object)?

Thanks.

Answer 1

I will give you a somewhat lose answer, because I am not that familiar with Haskell, but the question that you are specifically asking works in much simpler context.

So instead of general Haskell, we will focus on a given simply-typed lambda calculus (with product types). Then we can the same way build a category $\mathcal{C}$, whose objects are types, and morphisms are functions between types. Doing this we do not end up with any category, but with a cartesian closed category. This is the categorical notion that describes properly the existence of function types, and their interraction with morphisms. A cartesian closed category is firstly a category which has all finite products. This makes sense : given two types $A,B$, you can construct the type of pairs $A\times B$, and it behaves as the categorical product of the two types (this is the introduction and elimination of the pairs). Whenever you have such a category, any object $B$ defines a functor $\_\times B$, and a cartesian closed category is a category where this functor has a right adjoint. I will denote this right adjoint $(\_)^B$. Coming back to our category of types, $C^B$ will be the type of function from $B$ to $C$.

Now we will check that being right adjoint is the correct specification for the function type. By definition, it means that $Hom(A\times B,C) = Hom(A,C^B)$, and this equality corresponds exaclty to the curryfication. Note that this is a version of curryfication that involves an interraction between the (internal) function type $C^B$ and the (external) Hom of our category. Essentially by uniqueness of adjoints, this property characterises entirely the function types, thus having function types amounts exactly to being cartesian closed. Some other nice programming stuff are reflected by this : If you take the counit of this adjunction $$ \epsilon \in Hom(C^B\times B,C)$$ This is actually the evaluation function

eval : (B -> C) x B -> C
eval (f , b) = f b

And if you consider the unit $$ \eta \in Hom(C, (C\times B)^B)$$ This is the (probably less useful in programming) function

unit : C -> (B -> (C x B))
unit (c) = (lam b => (c,b)) 

Now if you come back to Haskell, you probably want dependent types. This is harder to describe categorically, but is doable, via a notion of locally cartesian closed category. I will not get into the details here, since you asked about (non-dependant) function types, the case of cartesian closed category is probably the one you should focus on first. It basically answers the question in the case you asked, just know that there exists generalised notions for managing dependent types and even dependent functon types (often called $\Pi$-types, I don't know if they are even here in Haskell)