Vitalii Guzeev
Platonic Hask overview: representable functors and monoidal category structures
Feb 23, 2023In the previous post, I promised to justify the change of signature of fmap from (a -> b) -> f a -> f b from Prelude to (a -> b) -> (f a -> f b). And occasionally explain the former notation. There is a categorical notion to help, it is called Cartesian closedness.
Here we leave indices of \(\operatorname{Hom}\)-sets to context, same for definitions of objects — each subsection operates a fixed category.
Cartesian closedness
Definitions
Category \(\mathrm{C}\) is called cartesian closed if it has terminal object, for all \(A,B \in \operatorname{Ob}(\mathrm{C})\) there exists a product \(A \times B\) and exponential object \(B^A\).
To define all relevant notions it is convenient (following lectures in Russian by A. Gorodentsev) to define representable functor.
Functor \(F : \mathrm{C}^{op} \to Set\) is said to be representable if is it naturally isomorphic to \(\operatorname{Hom}(\_,A)\) for some \(A\). We call \(A\) the representing object of functor \(F\). Representing object is unique up to canonical isomorphism.
Any representing object has associated universal property. Let’s see it by example.
Consider objects \(A,B \in \mathrm{C}\). If functor \(\operatorname{Hom}(\_,A) \times \operatorname{Hom}(\_,B)\) is representable, its representing object \(A \times B\) is called the product of \(A\) and \(B\).
Write this definition: \(\forall Y\; Hom(Y, A \times B) \cong \operatorname{Hom}(Y,A) \times \operatorname{Hom}(Y,B)\).
By setting \(Y = A \times B\), we obtain via this isomorphism the pair of maps \(\pi_A : A \times B \to A\) and \(\pi_B : A \times B \to B\) which are the image of \(Id_{A \times B}\) under isomorphism. They are called canonical projections. For arbitrary \(Y\) this isomorphism guarantees existence and uniqueness of map \(\phi : Y \to A \times B\) for any pair of maps \(\psi_A : Y \to A\) and \(\psi_B : Y \to B\). There are maps \(\pi_A \circ \phi\) and \(\pi_B \circ \phi\), since isomorphism is natural, \(\pi_A \circ \phi = \psi_A\), \(\pi_B \circ \phi = \psi_B\).
Thus we obtain the universal property of a product:
For any \(Y\), \(f : Y \to A\) and \(g : Y \to B\) there exists map \(\phi : Y \to A \times B\) such that the following diagram commutes:
Consider constant functor \(\overline{\{0\}}\) moving all objects to a fixed singleton set and all morphisms to identity. We call representing object of \(\overline{\{0\}}\) terminal object of category \(\mathrm{C}\). By evaluating its universal property we have that it is the object \(T\) with exactly one morphism \(Y \to T\) for any \(Y\).
Assume \(\mathrm{C}\) has all binary products. Consider functor \(\operatorname{Hom}(\_ \times A, B)\). Its representing object \(B^A\) is called exponential object. Actually, we defined it via isomorphism \(\operatorname{Hom}(Y, B^A) \cong \operatorname{Hom}(Y \times A, B)\) which may look familiar.
By taking \(Y = B^A\) we obtain map \(eval : B^A \times A \to B\). We can draw the universal property:
Usually, terminal objects and products are defined in terms of limits. But limits are examples of representing objects and are not really important here. We will turn back to them later.
Hask is cartesian closed
To prove the statement in the header we have to demonstrate the terminal object, exponentials, and products.
Since morphisms in \(Hask\) do not have to preserve any structure the only candidates for the terminal object are types with a single term. These are types isomorphic to (). They are all isomorphic (admit invertible bijections between each other), hence there is no need to check universality.
The evaluation map of the exponential object suggests an object satisfying universal property for types a, b — it is a -> b. Products are given by type with two natural projections — (a,b). Since universal objects are defined up to natural isomorphisms, product types data Cons = Cons B C are also products, same for newtypes over arrow types, etc.
Definition of exponential object gives us a natural isomorphism (a,b) -> c \(\cong\) a -> (b -> c) for any types a, b, c. This isomorphism is called currying. In Haskell it is common and is reflected in both implementation and notation — type a -> b -> c is literally equivalent to a -> (b -> c) (which is known as partial evaluation) and is isomorphic to (a,b) -> c via inverse functions curry and uncurry.
There is an important proposition that any cartesian closed category is a closed symmetric monoidal category with the tensor product given by the product in the sense of given universal property.
Closedness (informally) means that hom-sets can be considered objects of the category. Again informally we can see it from the existence of exponentials — their elements are functions from a to b, and elements of \(Hom\)-sets are morphisms from a to b. The term closed monoidal category encapsulates some compatibility conditions between the tensor product and exponentials. Rigorous definitions and proof of the claimed proposition are worth a separate post to be written.
So let’s proceed to the definition of the symmetric monoidal category.
Monoidal category structure
Definitions
Category \(\mathrm{C}\) is called monoidal if
- It is equipped with tensor product bifunctor \(\otimes : \mathrm{C} \times \mathrm{C} \to \mathrm{C}\) and associator functor \(\alpha : \mathrm{C} \to \mathrm{C}\) satisfying associative law.
- There exists unit object \(I\) and unitor functors \(\lambda\), \(\rho\) satisfying identity law.
- Both associator and unitor maps are natural isomorphisms where defined.
Associativity law is the commutativity of the following diagram:
Identity law is the commutativity of the following diagram:
Monoidal category is called symmetric if \(\forall A,B\) there exists isomorphism \(s_{AB} : A \otimes B \to B \otimes A\) such that the following diagram commutes:
Hask
From cartesian closedness there automatically follows that \(Hask\) is symmetric monoidal with \(\otimes =\)(,) and unit — (). Associator and unitor functors are obvious. Denote this structure as \((Hask, (,), ())\).
Consider \(End(Hask)\). It is a monoidal category with tensor product given by composition, unit — by Identity functor, and with identical unitors and associator. Denote this structure as \((End(Hask),\circ,Id)\).
These two statements will be central in the next several posts.
Dual counterparts
Universal properties allow us to construct dual objects by formally reversing all arrows.
While doing it with already defined representing objects we obtain the following definitions:
- Initial object is defined as an object \(I\) such that it has unique morphism to any other object
- Coproduct is defined by the following diagram:
- Coexponential object is defined by the following diagram:
Category with an initial object, all coexponentials, and all binary coproducts is called cocartesian coclosed.
\(Hask\) does not have all coexponentials and is not cocartesian coclosed.
But it has all coproducts given by Either a b and it has the initial object Void. This data is enough to equip \(Hask\) with another structure of symmetric (since coproducts are symmetric) monoidal category. The tensor product is given by the coproduct and the unit is given by the initial object. Denote this structure as \((Hask, Either, Void)\).
Note on corepresentable functors
These universal objects with reversed arrows can be defined via duals to representable functors.
Functor \(F : \mathrm{C} \to Set\) is said to be corepresentable if is it naturally isomorphic to \(\operatorname{Hom}(A,\_)\) for some \(A\). \(A\) is called corepresenting object of functor \(F\). Representing object is unique up to canonical isomorphism.
Initial object corepresents \(\operatorname{Hom}(\emptyset, \_)\), \(A \coprod B\) corepresents \(\operatorname{Hom}(A,\_) \otimes \operatorname{Hom}(B,\_)\), coexponential corepresents \(\operatorname{Hom}(B, \_ \coprod A)\).
In \(Hask\) \(\operatorname{Hom}(A,\_)\) is written as (->) A. We can restrict functors to instances of the Functor type class and obtain the following definition of representable functor: functor F is said to be representable if there exists a natural isomorphism between F a and (->) A a for every type a. A is the corepresenting object of F. But F must be considered as a functor to Set with values — sets of terms of resulting types of Functor we started with instead of types.
This definition is captured in package representable-functors. Isomorphism Cons a ~ A -> a in terms of this library is written as f a ~ Key a -> a, to the left it is given by tabulate, to the right by index.