haskell - Is this type a valid "rank-2 bifunctor"?

Question

The rank2classes package provides a version of Functor for which the mapped functions seem to be natural transformations between type constructors.

Following that idea, here's a rank-2 version of Bifunctor:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
import Data.Kind

type Rank2Bifunctor :: ((Type -> Type) -> (Type -> Type) -> Type) -> Constraint
class Rank2Bifunctor b where
  rank2bimap ::
    (forall x. p x -> p' x) -> (forall x. q x -> q' x) -> b p q -> b p' q'

It seems clear that this type Foo can be given a Rank2Bifunctor instance:

data Foo f g = Foo (f Int) (g Int)

instance Rank2Bifunctor Foo where
    rank2bimap tleft tright (Foo f g) = Foo (tleft f) (tright g)

But what about this Bar type which nests f and g:

data Bar f g = Bar (f (g Int))

For starters, it seems that we would need to require Functor p in the signature of rank2bimap, to be able to transform the g inside the f.

Is Bar a valid "rank-2 bifunctor"?

question from:https://stackoverflow.com/questions/66047704/is-this-type-a-valid-rank-2-bifunctor

Answer 1

Indeed that's not an instance of your Bifunctor, since the lack of constraint allows you to pick a contravariant functor for f and then rank2bimap would amount roughly to implement fmap for f:

rank2bimap id :: (g ~> g') -> Bar f g -> Bar f g'  -- covariance of f, kinda (since Bar f g = f (g Int))

type f ~> f' = (forall x. f x -> f' x)

If you add the requirement that f and g (optional here) be functors, then you do get a bifunctor:

rank2bimap :: (Functor f, Functor g) => (f ~> f') -> (g ~> g') -> Bar f g -> Bar f' g'

In particular, to prove the bifunctor laws, you will need the free theorem of f ~> f', assuming f and f' are functors, then n :: f ~> f' satisfies that for all phi, fmap phi . n = n . fmap phi.