# References to using profunctors in program analysis?

Profunctors from a category to itself seem like they'd be useful in representing the result of a program analysis; I can imagine a profunctor that given some information about a function it tells you what information you can derive about the composition of that function with something else.

Please post references below, if you have any. Thanks!

-

I don't really understand what you're after, it'd be great if you could expand a little bit; anyway, some pointers to the use of profunctors in related matters (possibly you already know about all this things):

## Hughes' arrows

This is what I think is more related to your question; arrows (these are not 1-cells/morphisms! (well, they are, see below)) are a generalization of (strong = enriched) monads as they're used in functional programming; the paper introducing them is

Hughes - Generalising monads to arrows - Science of computer programming :: (website)

Now, arrows correspond to strong monads in $\mathbf{Prof}$; (something like) this was first published in

Heunen, Jacobs - Arrows, like Monads, are Monoids - Electronic Notes in Theoretical Computer Science :: (pdf)

and a more precise account together with some generalizations is given in

Asada - Arrows are strong monads - Proceedings of the third ACM SIGPLAN workshop on Mathematically structured functional programming :: (pdf)

## semantics of concurrency

I guess this started with

Joyal, Nielsen, Winskel - Bisimulation from open maps - Logic in Computer Science :: (pdf)

where, viewing processes as presheaves, it is shown that in a lot of situations, bisimulations between processes can be defined in terms of spans of open maps between them (open here essentially the same as Joyal-Moerdijk); two processes are then bisimilar if there's a span of surjective open maps between them. This includes bisimilarity for synchronization trees, labelled transition systems, event structures, etc.

The connection with profunctors was first (I think) identified in

Cattani, Winskel - Profunctors, open maps and bisimulation - Mathematical Structures in Computer Science :: (pdf)

Where it is shown that profunctors (viewed as cocontinuous functors between presheaf categories) preserve open maps, and are thus a good notion of higher-order process: a profunctor $F \colon A \nrightarrow B$ maps $A$-processes to $B$-processes, an bisimulations to bisimulations. When viewing profunctors as higher-order processes, the structure of $\mathbf{Prof}$ (compact-closed, and thus traced, etc) starts to play a key role, and things start to look more like Abramsky geometry of interaction stuff and/or Walters (bi)categories with feedback etc: see for example

Hildebrandt, Panangaden, Winskel - Relational semantics of non-deterministic dataflow - CONCUR'98 Concurrency Theory :: (pdf)

This (presheaf categories - open maps - profunctors) setting has been somewhat generalized (modulo size issues) to work with a dense lax-idempotent 2-monad $T$ in $\mathbf{Cat}$, which in the presheaves and profunctors case would be (would it exist) the free-cocompletion 2-monad: one defines a notion of open map for a morphism in $TC$, and morphisms in the Kleisli 2-category $Alg_T$ preserve open maps.

-