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?
Yes, and we can read off exactly what sense that is from the shape of the constructor. Let's look at
(,)first.The
(,)FunctorThis 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 forHask × HasktoHask, whereHask × Haskis 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 inbaseHaskell. Specifically, a bifunctorpis capable of turning maps from(a, b)to(a', b')in the product category into maps fromp a btop a' b'. Haskell's typeclass writes this in a slightly different but equivalent wayHaving a map
a -> band a mapc -> dis 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 mapsa -> bandc -> d).The
FixFunctorWe can deal with
Fixthe same way.Its shape is
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 toFixis aFunctor, i.e. a functor fromHasktoHask.In that case,
Fixhas the right shape to be a functor from the functor categoryHask ^ Haskto the categoryHask. 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,
Fixtakes the functorf(functors are the objects of a functor category; read that again if it doesn't make sense yet) and maps it to the typeFix fthat we just defined.Now, the arrows of a functor category are natural transformations. Given two functors
f, g :: C -> D, a natural transformationαfromftogis a mapping from the objects ofCto the arrows ofD. Specifically, for every objectxin the categoryC,α xshould be an arrow inDgoing fromf xtog x, with the following coherence condition:(Using notation such as function composition very loosely, in true category theory spirit)
Drawn as a commutative diagram, the following must commute,
Haskell doesn't really have a built-in type for natural transformations. With Rank-N types, we can write the correct shape
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
Fixis going to be a functor fromHask ^ HasktoHask, it should take a natural transformation to an ordinary Haskell function, and it should have the following shape.Once we have this type, we can write the implementation fairly easily.
or, equivalently (by the rules of natural transformations),
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.