Analog of free monads for Profunctors

We can define data Free f a = Pure a | Free (f (Free f a)) and so have Functor f => Monad (Free f).

If we define data T f a b = R a | S b | T (f a (T f a b)) have we some analogous M so Profunctor f => M (T f a), where class Profunctor f where dimap :: (a -> b) -> (c -> d) -> f b c -> f a d?

I've been wondering ever since i noted Data.Comp.Term.Context and Free are isomorphic about a potential analog for Data.Comp.Param.Term.Context.

Solution

There's a more appropriate notion of making a free thing from a profunctor. Then we can work by analogy.

A free monoid, Y, generated by a set X is can be thought of as the solution to the equation "Y=1+XY". In Haskell notation that is

data List a = Nil | Cons a (List a)

A free monad, M, generated by the functor F can be thought of as the solution to the equation "M=1+FM" where the product "FM' is the composition of functors. 1 is just the identity functor. In Haskell notation that is

data Free f a = Pure a | Free (f (Free a))

Making something free from a profunctor P should look like a solution, A, to "A=1+PA". The product "PA" is the standard composition of profunctors. The 1 is the "identity" profunctor, (->). So we get

data Free p a b = Pure (a -> b) | forall x.Free (p a x) (Free p x b)

This is also a profunctor:

instance Profunctor b => Profunctor (Free b) where
    lmap f (Pure g) = Pure (g . f)
    lmap f (Free g h) = Free (lmap f g) h
    rmap f (Pure g) = Pure (f . g)
    rmap f (Free g h) = Free g (rmap f h)

If the profunctor is strong then so is the free version:

instance Strong p => Strong (Free p) where
    first' (Pure f) = Pure (first' f)
    first' (Free f g) = Free (first' f) (first' g)

But what actually is Free p? It's actually a thing called a pre-arrow. Restricting, free strong profunctors are arrows:

instance Profunctor p => Category (Free p) where
    id = Pure id
    Pure f . Pure g = Pure (f . g)
    Free g h . Pure f = Free (lmap f g) h
    Pure f . Free g h = Free g (Pure f . h)
    f . Free g h = Free g (f . h)

instance (Profunctor p, Strong p) => Arrow (Free p) where
    arr = Pure
    first = first'

Intuitively you can think of an element of a profunctor P a b as taking an a-ish thing to a b-ish thing, the canonical example being given by (->). Free P is an unevaluated chain of these elements with compatible (but unobservable) intermediate types.