Are type-level functors just functors in Hask's 2-category?
From what I understand, the typical interpretation of the Hask category is that category objects are Haskell types and morphisms are Haskell functions.
With this 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 one subcategory of the Hask object and S a
as a functor, mapping a category Z
to a category S Z
and mapping it to a category S(S Z)
, etc.
So, and advanced type-level lists (for example) could a type-level functor (for example Map
) be a functor in a 2-category Hask ?
source to share
You can think of Map
here as lifting arrows from a category where objects are kind things Nat
to a category where objects are kind things [Nat]
. But this is not a functor because it does not provide a canonical way to hoist objects Nat
onto objects [Nat]
(and there are several ways to do this).
If you have a more general Map
one that mirrors things at the value level, dispatches view a -> b
functions to view functions [a] -> [b]
, then it will give a functor.
In any case, 2 categories are not included in this picture. How the 2 categories work, they are similar to the normal categories, but they also have cards between the arrows themselves, which are also properly drawn. (And the higher categories, in turn, have maps between those cells, etc.). So, Hask
it is not a 2-category, since we do not have special cards between our arrows.
Side note: while Hask
not a 2-category, it results in an associate as it is "enriched in itself." In this category, objects are "hask-enriched categories". That is, categories whose objects are whatever you choose, but whose morphisms are haskell functions - hack subcategories, given, for example. []
,Maybe
etc. all fit here). Morphisms in this category are functors between such Husk-rich categories. That is, they map objects to objects and (haskell) between objects (haskell) between objects. Thus, they correspond to what we usually think of as natural conversions between functors. And now we need to add real 2-cells of natural transformations between them! That is, they are composed of what we will think of as "natural transformation morphisms" in typical Haskell.
But that is hardly what I think you meant.
source to share