Better roles for Control.Monad.Trans.Free.Church.F

[ekmett]

We wind up with a nominal role for the 'm' parameter, because it occurs inside f in the body of FT

newtype FT f m a = FT { runFT :: forall r. (a -> m r) -> (f (m r) -> m r) -> m r }

We should be able to achieve representational by smashing that occurrence of f with Yoneda.

newtype FT f m a = FT { runFT :: forall r. (a -> m r) -> (forall x. (x -> m r) -> f x -> m r) -> m r }

This is the same trick that drives the Mendler-style catamorphism.

[masaeedu]

@ekmett Just for my own edification, wouldn't "smashing the occurrence of f" involve the following conversion?

fwd :: Functor f => f x -> (forall y. (x -> y) -> f y)
fwd fx = \xy -> fmap xy fx

If we're smashing f (m r) specifically, plug and chugging converts the following:

newtype FT f m a = FT { runFT :: forall r. (a -> m r) -> (f (m r) -> m r) -> m r }

to:

newtype FT f m a = FT { runFT :: forall r. (a -> m r) -> ((forall x. ((m r) -> x) -> f x) -> m r) -> m r }

Is there some further isomorphism that produces the type you have above?