Homomorphic static analysis

Hey @marcosh,

great post, thank you. Due to the posts by you and others I have recently looked more into category/arrow based programming. Now I have a question on which I’d like to pick your brain (or anyone elses in the community.)

I really like the concept of Alternative and Parallel like you used them and how you drew the diagram. This strongly suggested to me that strong profunctors (/arrows) are a way to express parallelism. But I hit a problem with that:

I assume your implementation of f &&& g is something like lmap dup (first' f >>> second g'). Here morally first' f and second' g are “parallel”, you drew it like that in your diagram and that makes sense because f and g have no data dependency.

But now assume that we run this in a profunctor which has observable side effects. e.g. a newtype around Kleisli IO where we would want &&& or *** to use concurrently.

Now we have two choices

1. either we implement *** so that f *** g /= first' f >>> second' g because we implement *** truly parallel while first' f >>> second' g executes f and g sequentially. This is unsatisfying because it a) breaks the intuition implied by your diagrams and b) seems at least dubious for Arrows where *** is defined as first f >>> arr swap >>> first g >>> arr swap and it says “you may implement a more efficient version”. Which is not documented as a law but to me implies that we should have a law that f *** g == first f >>> second g.

2. we find an implementation of our profunctor which truly fuses first' f >>> second' g and runs f and g concurrently. I tried that and it is possible. However what I couldn’t manage to do was to achieve fusion in a way that first' f >>> second' g /= first' f >>> lmap id (second' g) It seems impossible to me because there is now way to detect whether lmap f introduces a data dependency between f and g. Now that is a problem because Profunctor documents the law lmap id == id.

(I looked into this and my impression is that 2. is only really possible for “Causal Commutative Arrows”, which is quite restrictive.)

So my take away is, that observably parallel arrows cannot do anything interesting when their Profunctor instance is not trivial (like in your static analysis which has a phantom parameter.) So profunctor based programming seems to be fundamentally sequential to me.

What do you think?