Profunctor Equipment in Haskell

Previously: Profunctor Equipment.To make things more palatable for programmers, I decided to provide a toy implementation of some of the equipments in Haskell. The advantage of this encoding is that it can be verified by the compiler, and I still trust the compiler more than I trust the AI.A more adequate implementation would require a full-blown dependently typed language, but if we restrict ourselves to just a single category and work only with endo-functors and endo-profunctors, we can get at least some intuitions. If you want to see a more elaborate version, see the proarrows library by Sjoerd Visscher. The only 0-cell I’ll be using is the Haskell category of types and functions. For vertical 1-cells I’ll use the standard library implementation of Functor, and for horizontal ones I’ll use Profunctor. A 2-cell in :is implemented as a natural transformation:type Cell f g h j = forall a c . h a c -> j (f a) (g c)The forall serves as a universal quantifier. The horizontal composition of such cells is given by:hcomp :: (Functor f, Functor f', Functor g, Functor g' , Profunctor h, Profunctor j, Profunctor k) => Cell f g h j -> Cell f' g' j k -> Cell (Compose f' f) (Compose g' g) h khcomp fg_hj fg_jk hac = dimap getCompose Compose $ fg_jk (fg_hj hac)I used the library definition of functor composition:newtype Compose f g a = Compose { getCompose :: f (g a) }Vertical composition of cells uses a more elaborate profunctor composition:vcomp :: (Functor f, Functor g, Functor h , Profunctor p, Profunctor q, Profunctor r, Profunctor s) => Cell f g p r -> Cell g h q s -> Cell f h (Procompose q p) (Procompose s r)vcomp fg_pr gh_qs (Procompose qxc pax) = Procompose (gh_qs qxc) (fg_pr pax)Profunctor composition is defined using a coend.

In Haskell, we implement a coend:as an existential type: data Procompose p q d c where Procompose :: p x c -> q d x -> Procompose p q d cHere, x is a type that’s not in the argument list, so it’s interpreted using the existential counterpart of forall.This is the horizontal unit cell:type Hunit p = Cell Identity Identity p phUnit :: Profunctor p => Hunit phUnit = dimap runIdentity Identityand here’s its vertical counterpart:type Vunit f a b = Cell f f (->) (->)vUnit :: Functor f => Vunit f a bvUnit = fmapI used the library implementation of the Identity functor, and the type constructor (->) for the hom-profunctor–the unit of profunctor composition. The unit laws are satisfied up to isomorphism.The companion and the conjoint are synonyms of the library types Costar and Star:newtype Star f d c = Star { runStar :: d -> f c }newtype Costar f d c = Costar { runCostar :: f d -> c }type Companion f d c = Costar f d ctype Conjoint f d c = Star f d cThe companion unit and counit cells:are given by, respectively:type CompUnit f = Cell Identity f (->) (Costar f)compUnit :: Functor f => CompUnit fcompUnit h = Costar (fmap (h . runIdentity))andtype CompCoUnit f = Cell f Identity (Costar f) (->)compCoUnit :: Functor f => CompCoUnit f compCoUnit (Costar h) = Identity . hSimilarly for the conjoint:type ConjUnit f = Cell f Identity (->) (Star f)conjUnit :: Functor f => ConjUnit f conjUnit h = Star (fmap (Identity . h))and:type ConjCoUnit f = Cell Identity f (Star f) (->)conjCoUnit :: Functor f => ConjCoUnit f conjCoUnit (Star h) = h . runIdentityMore advanced constructions would require the definition of categories internal to Hask and the use of dependent types.Haskell code is available here.