haskellcompositionfunctorcategory-theory

Can `Fix` and `(,)` be seen as functors in some sense?


I've been wondering what a complete, all-encompassing context for instance Functor (f :.: g) would be. The immediate thought that pops into my head is:

newtype (f :.: g) a = Comp (f (g a))
instance (Functor f, Functor g) => Functor (f :.: g) where
    fmap f (Comp x) = Comp (fmap (fmap f) x)

But then, two contravariant functors would also compose to be covariant, like so:

instance (Contravariant f, Contravariant g) => Functor (f :.: g) where
    fmap f (Comp x) = Comp (contramap (contramap f) x)

Already not a promising beginning. However, I've also noticed that technically, f and g don't even have to have kind * -> * -- the only requirement for f :.: g :: * -> * is that f :: k -> * and g :: * -> k for some k. This means that non-functor types could compose to be functors, e.g.

newtype Fix f = Fix (f (Fix f))
instance Functor (Fix :.: (,)) where
    fmap f (Comp x) = Comp (go x) where
        go (Fix (x,xs)) = Fix (f x,go xs)

Fix :.: (,) is isomorphic to the Stream type:

data Stream a = a :> Stream a

so this does seem to be a non-trivial issue. This got me thinking -- if Haskell's Functor typeclass represents categorical functors from Hask to Hask, does that mean types like Fix and (,) could be functors working on some other categories? What would those categories be?


Solution

  • Yes, and we can read off exactly what sense that is from the shape of the constructor. Let's look at (,) first.

    The (,) Functor

    (,) :: * -> * -> *
    

    This takes two types and produces a type. Up to isomorphism, this is equivalent to

    (,) :: (*, *) -> *
    

    i.e. we might as well uncurry the function and take both arguments at once. So (,) can be viewed as a functor for Hask × Hask to Hask, where Hask × Hask is the product category. We have a word for a functor whose domain is the product of two categories. We call it a bifunctor, and it's actually in base Haskell. Specifically, a bifunctor p is capable of turning maps from (a, b) to (a', b') in the product category into maps from p a b to p a' b'. Haskell's typeclass writes this in a slightly different but equivalent way

    bimap :: Bifunctor p => (a -> b) -> (c -> d) -> p a c -> p b d
    

    Having a map a -> b and a map c -> d is exactly equivalent to having a map (a, c) -> (b, d) in the product category. (What I mean by that is: the maps (a, c) -> (b, d) in the product category are defined to be products of maps a -> b and c -> d).

    The Fix Functor

    We can deal with Fix the same way.

    newtype Fix f = Fix (f (Fix f))
    

    Its shape is

    Fix :: (* -> *) -> *
    

    It takes a one-argument type constructor and produces a type.

    Now, in Haskell, the * -> * part can be any one-argument type constructor, but categorically it's much nicer to work with functors. So I'm going to make the slightly stronger constraint (which it turns out we'll need in a minute) that the * -> * argument to Fix is a Functor, i.e. a functor from Hask to Hask.

    In that case, Fix has the right shape to be a functor from the functor category Hask ^ Hask to the category Hask. A functor, categorically, takes objects to objects and arrows to arrows. So let's take that one step at a time.

    The object part is easy, we've already defined it. Specifically, Fix takes the functor f (functors are the objects of a functor category; read that again if it doesn't make sense yet) and maps it to the type Fix f that we just defined.

    Now, the arrows of a functor category are natural transformations. Given two functors f, g :: C -> D, a natural transformation α from f to g is a mapping from the objects of C to the arrows of D. Specifically, for every object x in the category C, α x should be an arrow in D going from f x to g x, with the following coherence condition:

    For every arrow h : x -> y in C, we must have (g h) . (α x) === (α y) . (f h)

    (Using notation such as function composition very loosely, in true category theory spirit)

    Drawn as a commutative diagram, the following must commute,

    A commutative diagram representing (g h) . (α x) === (α y) . (f h)

    Haskell doesn't really have a built-in type for natural transformations. With Rank-N types, we can write the correct shape

    (forall a. f a -> g a)
    

    This is the shape of a natural transformation, but of course we haven't verified the coherence property. So we'll just have to trust that it satisfies that property.

    With all of this abstract nonsense in mind, if Fix is going to be a functor from Hask ^ Hask to Hask, it should take a natural transformation to an ordinary Haskell function, and it should have the following shape.

    fixmap :: (Functor f, Functor g) => (forall a. f a -> g a) -> Fix f -> Fix g
    

    Once we have this type, we can write the implementation fairly easily.

    fixmap h (Fix inner) = Fix (h . fmap (fixmap h) $ inner)
    

    or, equivalently (by the rules of natural transformations),

    fixmap h (Fix inner) = Fix (fmap (fixmap h) . h $ inner)
    

    I'm not aware of an idiomatic name for this shape of functor, nor am I aware of a typeclass that encompasses it, but of course nothing stops you from making it yourself.