Are type-level functors just functors in the 2-category of Hask?

Question

From what I understand, the typical interpretation of the Hask category is that the objects of the category are Haskell types, and the morphisms are Haskell functions.

With that interpretation:

{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}
data Nat = Z | S Nat

type family Map (f :: Nat -> Nat) (x :: [Nat]) :: [Nat] where
Map f '[] = '[]
Map f (x ': xs) = (f x) ': (Map f (xs))

we could interpret Z as a single object sub-category of Hask, and S a as a functor, mapping the category Z to the category S Z, and mapping that to the category S(S Z), etc...

With that then, and a type-level promoted lists (for example), would a type-level functor (like Map) be a functor in the 2-category of Hask?

Hask is the category whose objects have kind *, so Z-as-only-object is not a subcategory since it has kind Nat. Still, you can certainly consider Z as a category – but what are the morphisms? If there exist no nontrivial ones it might not even invalidate the idea, but I wouldn't even know what to call those morphisms. — leftaroundabout
There would be no morphisms other than the identity morphisms. — Nathan BeDell

sclv sclv · Accepted Answer · 2016-03-19T19:13:01

You can think of Map here as lifting arrows from the category where objects are things of kind Nat to the category where objects are things of kind [Nat]. But that's not a functor, because it doesn't provide a canonical way to lift objects of Nat to objects of [Nat] (and there are multiple ways to do that).

If you had a more general Map that mirroring things on the value level sent functions of kind a -> b to functions of kind [a] -> [b] then it would give a functor.

In any case, 2-categories don't enter into this picture. The way 2-categories work is they're like normal categories, but they also have maps between arrows themselves, that also compose in the proper way. (And higher categories in turn have maps between those cells, etc). So Hask isn't a 2-category to begin with, as we have no special maps between our arrows.

Side note: while Hask isn't a 2-category, it does give rise to an associated one, as it is "enriched in itself". In this category, objects are "hask-enriched categories". That is to say, categories whose objects are whatever you choose, but whose morphisms are haskell functions -- the subcategories of hask given by e.g. [], Maybe, etc. all fit in here for example). The morphisms of this category are functors between such Hask-enriched categories. That is to say they map objects to objects, and (haskell) functions between objects to (haskell) functions between objects. So those correspond to what we normally think of as natural transformations between functors. And now we need to add the genuine 2-cells of natural transformations between those! That is to say, they consist of what we would think of as "morphisms of natural transformations" in typical Haskell.

But this is hardly what I imagine you had in mind.

Are type-level functors just functors in the 2-category of Hask?

1 Answers