Comments on A Neighborhood of Infinity: Profunctors in Haskell

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

2011-08-06T21:52:11.397-07:00

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

Hi @Mike! (Via an indirect path) it was your post...

2011-08-06T06:40:42.029-07:00

Hi @Mike!

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

I've updated my blogger profile.

2011-08-05T16:37:05.202-07:00

I've updated my blogger profile.

No, Mike Stay, John Baez' student. I wrote th...

2011-08-05T16:35:19.525-07:00

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"

Hey @mike, Are you Mike Shulman?

2011-08-05T16:18:48.238-07:00

Hey @mike,

Are you Mike Shulman?

Oops, I got the objects of Mat(R) wrong. Objects ...

2011-08-05T16:15:31.719-07:00

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.

Hi. Profunctors are one way to categorify linear ...

2011-08-05T16:00:53.005-07:00

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.

The bifunctor seems more general. I've noticed...

2011-08-04T04:58:09.193-07:00

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

@Ivan Bifunctors are actually different. They are ...

2011-07-28T10:18:12.245-07:00

@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.

This naming thing is annoying. I searched Ed's...

2011-07-25T18:00:59.039-07:00

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.

Just thought I'd mention the categories packag...

2011-07-25T17:52:38.341-07:00

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.

Profunctors is but one of many names for this conc...

2011-07-25T15:06:20.266-07:00

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.)

In plain category theory, you can have a (co)end o...

2011-07-25T13:44:20.834-07:00

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.

1. I've only ever seen profunctors mapping int...

2011-07-24T06:42:46.084-07:00

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).

So, I have a two-part question about the generalit...

2011-07-24T01:45:52.624-07:00

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?

I wasn't objecting to the argument order of
2011-07-23T18:45:37.064-07:00
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).

I think my statements are correct, but I made a ba...

2011-07-23T16:28:41.833-07:00

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!

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

2011-07-23T15:39:19.453-07:00

I think the

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

should be

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