A Neighborhood of Infinity

Saturday, July 23, 2011

> {-# LANGUAGE TypeSynonymInstances, RankNTypes, ExistentialQuantification #-}

Introduction
When I wrote about coends a while back I made up a term 'difunctor'. More recently it was pointed out to me that the correct word for this concept is 'profunctor', but unfortunately my knowledge came from MacLane which mentions that word nowhere.

Profunctors are ubiquitous in Haskell programming. Probably the most natural definition of Hughes Arrows is via profunctors. Profunctors also play a role a little like tensors leading to a use of the terms 'covariant' and 'contravariant' that looks remarkably like the way those terms are used in tensor calculus.

For categories C and D, A profunctor is a functor Dop×C→Set and is written C↛D. (I hope that arrow between C and D is in your font. It's missing on iOS.)

I'll reuse my Haskell approximation to that definition:

> class Profunctor h where
>   lmap :: (d' -> d) -> h d c -> h d' c
>   rmap :: (c -> c') -> h d c -> h d c'

We need cofunctoriality for the first argument and functoriality for the second:

lmap (f . g) == lmap g . lmap f
rmap (f . g) == rmap f . rmap g

(Strictly we probably ought to call these 'endoprofunctors' as we're only really dealing with the category of Haskell types and functions.)

There are lots of analogies for thinking about profunctors. For example, some people think of them as generalising functors in the same way that relations generalise functions. More specifically, given a function f:A→B, f associates to each element of A, a single element of B. But if we want f to associate elements of A with elements of B more freely, for example 'mapping' elements of A to multiple elements of B then we instead use a relation which can be written as a function f:A×B→{0,1} where we say xfy iff f(x,y)=1. In this case, profunctors map to Set rather than {0,1}.

A good example is the type constructor (->)

> instance Profunctor (->) where
>   lmap f g = g . f
>   rmap f g = f . g

It's common that the first argument of a profunctor describes how an element related to a type is sucked in, and the second describes what is spit out. a -> b sucks in an a and spits out a b.

Given a function f we can turn it into a relation by saying that xfy iff y=f(x). Similarly we can turn a functor into a profunctor. Given a functor F:C→D we can define a profunctor F*:C↛D by

> data UpStar f d c = UpStar (d -> f c)
> instance Functor f => Profunctor (UpStar f) where
>   lmap k (UpStar f) = UpStar (f . k)
>   rmap k (UpStar f) = UpStar (fmap k . f)

You may be able to see how the second argument to a profunctor sort of plays a similar role to the return value of a functor, just as the second argument to a relation sometimes plays a rule similar to the return value of a function.

There also an opoosing way to make a profunctor from a functor just as there is with functions and relations:

> data DownStar f d c = DownStar (f d -> c)
> instance Functor f => Profunctor (DownStar f) where
>   lmap k (DownStar f) = DownStar (f . fmap k)
>   rmap k (DownStar f) = DownStar (k . f)

Note that the identity functor gives us something isomorphic to (->) whether you use UpStar or DownStar.

Dinatural transformations
Just as we have natural transformations between functors, we have dinatural transformations between profunctors. My previous definition of dinatural was specialised to a particular case - dinaturals between a profunctor and the constant profunctor.

Firstly, let's think about natural transformations. If F and G are functors, and h is a natural transformation h:F⇒G, then we have that
h . fmap f = fmap f . h
If we think of F and G as containers, then this rule says that a natural transformation relates the structures of the containers, not the contents. So using f to replace the elements with other elements should be invisible to h and hence commute with it.

Something similar happens with dinatural transformations. But this time, instead of relating the argument to a natural transformation to its return result, it instead relates the two arguments to a profunctor.

Given two profunctors, F and G, A dinatural transformation is a polymorphic function of type:

> type Dinatural f g = forall a. f a a -> g a a

but we also want something analogous to the case of natural transformations. We want to express the fact that if phi :: Dinatural F G, then phi doesn't see the elements of F a a or G a a. Here's a way to achieve this. Suppose we have a dinatural transformation:
phi :: Dinatural G F
and a function f :: X -> X' then we can use lmap to apply f on the left or right of F and G. The definition of dinaturals demands that:
rmap f . phi . lmap f = lmap f . phi . rmap f
ie. that we can apply f on the left before applying phi, and then do f on the right, or vice versa, and still get the same result.

I'm not sure but I think that we don't need to check this condition and that just like the case of naturals it just comes as a free theorem.

Composing profunctors
It's easy to see how to compose functors. A functor is a polymorphic function from one type to another. It's not straightforward to compose profunctors. It's tempting to say that a profunctor maps a pair of types to a type so they can be composed like functions. But the original definition says the definition is Dop×C→Set. So as a function it doesn't map back to the category but to Set. For Haskell we replace Set with Hask, the category of Haskell functions and types. So we have Haskop×Hask→Hask. It's easy invent a scheme to compose these because Hask appears 3 times. But it'd be wrong to exploit this in a general definition applying to many categories because in the proper definition of profunctor we can't assume that a profunctor maps back to the spaces you started with.

We can try composing profunctors by analogy with composing relations. Suppose R and S are relations. If T=S○R is the composition of R and S then xTz if and only if there exists a y such that xRy and ySz. If our relations are on finite sets then we can define T(x,z) = ΣyR(x,y)S(y,z) where we work in the semiring on {0,1} with 0+0=0, 0+1=1+0=1+1=1 but with the usual product.

There is an analogue of "there exists" in Haskell - the existential type. Remembering that we write Haskell existential types using forall we can define:

> data Compose f g d c = forall a.Compose (f d a) (g a c)

As mentioned above, functors give rise to profunctors. It'd be good if composition of functors were compatible with composition of profunctors. So consider
Compose (UpStar F) (UpStar G)
for some F and G. This is essentially the same as
exists a. (d -> F a, a -> G c)
What can we discover about an element of such a type? It consists of a pair of functions (f, g), but we can't ever extract the individual functions because the type of a has been erased. To get anything meaningful out of g we need to apply it to an a, but we don't have one immediately to hand, after all, we can't even know what a is. But we do have an F a if we can make a d. So we can use fmap to apply g to the result of a. So we can construct fmap g . f :: d -> F (G c). There is no other information we can obtain. So the composition is isomorphic to UpStar of the functorial composition of F and G. Again, we can probably make this a rigorous proof by making use of free theorems, but I haven't figured that out yet.

But there's a catch: I said I wanted a definition that applies to more categories than just Hask. Well we can replace exists a with the coend operator. We also implicitly used the product operation in the constructor Compose so this definition will work in categories with suitable products. Symmetric monodial categories in fact.

Under composition of profunctors, (->) is the identity. At least up to isomorphism. This composition of profunctors is also associative up to isomorphism. Unfortunately the "up to isomorphism" means that we can't make a category out of profunctors in the obvious way. But we can make a bicategory - essentially a category where we have to explicitly track the isomorphisms between things that are equal in ordinary categories.

Profunctors as tensors
Given a profunctor F we can write F i j suggestively as Fij. Let's write the composition of F and G as ∃k. Fik Gkj. We can use the Einstein summation convention to automatically 'contract' on pairs of upper and lower indices and write the composition as Fik Gkj. The analogy is even more intriguing when we remember that in tensor notation, the upper indices are covariant indices and the lower ones are contravariant indices. In the case of profunctors, the two arguments act like the arguments to covariant and contravariant functors respectively. Note alse that because (->) is essentially the identity, we have →ijFjk=Fik. So (->) acts like the Kronecker delta. You can read more about this at mathoverflow where it is hinted that this analogy is not yet well understood. Note that we're naturally led to the trace of a profunctor: exists a. F a a.

Arrows as profunctors
The last thing I want to mention is that Hughes' Arrows are profunctors. There is an intuition that fits. If A is an Arrow, we often think of A d c as consuming something related to type d and emitting something related to type c. The same goes for profunctors. The full paper explaining this is Asada and Hasuo's Categorifying Computations into Components via Arrows as Profunctors with the profunctorial definition of Arrows given as Definition 3.2 (though that definition also appears in some earlier papers.)

Anonymous said...

I think the

fmap g . f :: a -> F (G C)

should be

fmap g . f :: d -> F (G c) :)

sigfpe said...

I think my statements are correct, but I made a bad choice for the definition of Compose. I'm going to flip the definition. Tell me if you think the resulting statements are still incorrect and I'll type up the full working out I have on paper.

Thanks for looking closely though!

Anonymous said...

I wasn't objecting to the argument order of Compose; my comment was only about the paragraph below exists a. (d -> F a, a -> G c), in which (f,g) is taken to be of that type.

I was just saying that in that case fmap g . f is of type d -> F (G c), not a -> F (G c) (nothing deep, just a typo I think).

winterkoninkje said...

So, I have a two-part question about the generalities between profunctors and coends.

First: in the definition of profunctors you give here you restrict to mapping into Set whereas the definition of coend I've seen about allows mapping into any symmetric monoidal category X; I assume this is just you limiting the scope for simplicity of discussion?

Second: your definition of profunctors allows the categories C and D to differ, whereas the definitions I've seen for coends has them be the same; is there a reason for this restriction on the definition of coends, or were these other authors just limiting the scope for simplicity?

sigfpe said...

1. I've only ever seen profunctors mapping into Set. I'm guessing that for V-categories you map into V because you want Hom(_,_) (aka. (->)) to be a profunctor.

2. Profunctors have different categories but coends restrict to the same category. Coends sort of contract out a repeated index so I'd expect the same category to appear twice.

As my discussion is restricted to Hask, I'm always composing profunctors with matching categories, which means they can be composed with coends. In the more general case I think you need Kan extensions. But I haven't thought much about those (for the simple reason you often don't need them when reasoning about Haskell).

Dan Doel said...

In plain category theory, you can have a (co)end of any functor with a type of the form 'C^op x C -> D'. D needn't be symmetric monoidal; just a category. You can also have dinatural transformations between functors of this form. But you cannot have a dinatural transformation for profunctors of the form 'D^op x C -> Set' unless C = D.

There apparently is a notion of a (co)end of functors 'C^op x C -> V', with C enriched in V and V symmetric monoidal. But enriched category theory then has (co)ends 'C^op x C -> D' for C and D arbitrary V-enriched categories as well.

Derek Elkins said...

Profunctors is but one of many names for this concept. Two others are: distributors and C-D-bimodules. Emily Riehl's cute paper on weighted (co)limits uses them to good effect. Another nice application of profunctors is the theory of generalized species as described, e.g., here. (Composition of profunctors can be expressed through a left Kan extension, but I find the definition using coends more transparent. Either follows readily by thinking in analogy to set-theoretic relations though.)

Ivan Tomac said...

Just thought I'd mention the categories package by Edward Kmett implements this a bit more generally under the name bifunctor.
The relation to arrows is also made obvious by calling lmap first and rmap second.

sigfpe said...

This naming thing is annoying. I searched Ed's package looking for profunctors and of course failed to find them.

I find the name 'distributor' suggestive. You can reproduce some trivial results from functional analysis using them (eg. (->) is the Dirac delta) but I haven't thought of ways to do more ambitious functional analysis type things.

sigfpe said...

@Ivan Bifunctors are actually different. They are functorial in both their arguments, and unlike Profunctors, they don't necessarily map back down to the "base" category, in this case Set.

But...Ed has now uploaded a profunctors package.

Ivan Tomac said...

The bifunctor seems more general. I've noticed 'lmap' appears to work in reverse, compared to 'first' and it just occured to me as a result of that you wouldn't be able to create an instance of Bifunctor from Profunctor as Bifunctor requires both PFunctor and QFunctor to be parameterized over the same type, p, but I don't think I understand the implications of that.
It seems that PFunctor and QFunctor can be easily derived from a Profunctor however.

newtype a :<- b = W { unW :: b -> a }

instance Category (:<-) where
id = W Prelude.id
f . g = W (unW g . unW f)

instance Profunctor h => PFunctor h (:<-) (->) where first = lmap . unW

instance Profunctor h => QFunctor h (->) (->) where second = rmap

mike said...

Hi. Profunctors are one way to categorify linear algebra, so you'll get lots of similar constructions. The bicategory Prof is compact closed, where the "opposite" functor is the dual; upstar and downstar are currying and uncurrying.

Some other compact closed bicategories are Rel, with sets, relations, and implications; Span(Set), with sets, spans, and maps of spans; Prof and its equivalent 2-category Cocont of presheaf categories, cocontinuous functors, and natural transformations; nCob_2, whose objects are (n-2)-dimensional manifolds, morphisms are (n-1)-dimensional manifolds with boundary, and 2-morphisms are n-dimensional manifolds with corners; and Mat(R) where R is any rig category (it's symmetric monoidal under ⊕, monoidal under ⊗, and ⊗ distributes up to isomorphism over ⊕; Set is the principle example with product & coproduct), whose objects are objects of R, morphisms are Ob(R)-valued matrices, and 2-morphisms are Mor(R)-valued matrices.

mike said...

Oops, I got the objects of Mat(R) wrong. Objects are natural numbers; morphisms are Ob(R)-valued matrices and 2-morphisms are Mor(R)-valued matrices.

sigfpe said...

Hey @mike,

Are you Mike Shulman?

mike said...

No, Mike Stay, John Baez' student. I wrote the Rosetta stone paper with him and I'm almost done with a paper on compact closed bicategories. That's why I was asking about how Haskell dealt with the trace on the Google Haskell list :)

Here are some examples from my paper:

If you take a monad in Rel, you get a preorder:
- A relation H from a set O to itself
- An implication xHHy -> xHy, i.e. transitivity
- An implication T -> xHx, i.e. reflexivity.

If you take a monad in Span(Set), you get a small category:
- A span of sets O <-src- M -tgt-> O that maps morphisms to their source & target object
- A map of spans involving a function from M x_O M -> M, where M x_O M is the set of composable pairs of morphisms
- A map of spans involving a function from O to M picking out the identity.

If you take a (symmetric monoidal) monad in Prof, you get an Arrow:
- A profunctor A that assigns to any two types the set of abstract programs between them
- A natural transformation AA -> A for composition of abstract programs
- A natural transformation 1->A for "lifting"

Mike Stay said...

I've updated my blogger profile.

sigfpe said...

Hi @Mike!

(Via an indirect path) it was your post that prompted me to write this.

Mike Stay said...

We should have lunch! I'll grab a spot on your calendar.

Paolo G. Giarrusso said...

> For categories C and D, A profunctor is a functor Dop×C→Set and is written C↛D.
You write C↛D and not D↛C there, but that seems confusing since profunctors should generalize hom-functors, yet C↛D is covariant in the first argument and contravariant in the second. The actual profunctor takes argument in the right order, but this is still confusing.

So, I'd prefer to update that to read:
> For categories C and D, A profunctor is a functor Cop×D→Set and is written C↛D.
and update the rest accordingly. I noticed that as a result, UpStar would turn a functor F:C→D into a profunctor F*:D↛C, but I think that flipping shouldn't be a problem, because DownStar would turn a functor F:C→D into a profunctor F_{*}:C↛D (if I'm not mistaken).

As a related but distinct change, it would help to rename type variables in:
> class Profunctor h where
> lmap :: (d' -> d) -> h d c -> h d' c
> rmap :: (c -> c') -> h d c -> h d c'
to get:
> class Profunctor h where
> lmap :: (c' -> c) -> h c d -> h c' d
> rmap :: (d -> d') -> h c d -> h c d'
similarly to what Edward Kmett did in his package: