Selective Applicative Functors

I havenʼt seen a good accounting of the essence of selective applicative functors.

Theyʼve been longing for a better description, to help explain what should be allowed and what should be disallowed, beyond “hey, here is a function select that seems to do useful things and enable us to write interesting code”.

Selective applicative functors were originally proposed in 2019 in the paper Selective Applicative Functors, by Andrey Mokhov, Georgy Lukyanov, Simon Marlow, and Jeremie Dimino, with this typeclass definition:

class Applicative f => Selective f where<br>select :: f (Either a b) -> f (a -> b) -> f b

The paper mentions a branch combinator derived from () = select:

branch :: Selective f => f (Either a b) -> f (a -> c) -> f (b -> c) -> f c<br>branch x l r = fmap (fmap Left) x fmap (fmap Right) l r

But the story has stopped short after select because the familiar tools of theoretical analysis failed to apply to select: there was no account for select in terms of monoidal tensors, and even branch did not meaningfully compose with itself, which means that there was no obvious way that the laws related to more familiar algebraic and categorical structures like monoids (and, it turns out, near-semirings).

However, the final answer for what selective applicative functors want to be is really cool.<br>We just have to work a bit harder to see it: we have to consider arrows (composable profunctors) instead of plain functors.

Selective applicative functors want to encode exclusive and exhaustive determined choice.<br>They can choose between a finite number of predetermined case branches based upon previous results during evaluation.select itself has an implicit pure branch with no side-effects, where branch has two branches.

Once you see it, it makes so much sense from a programming language perspective: it has the shape of an AST for a programming language.<br>We can even go farther and relate it to the other typeclass for control flow, Alternative, which provides for nondeterministic choice.

Overview

Here it is, here is the essence of selective applicatives!

Letʼs start from the familiar territory of monads.<br>Monads encode the essence of dynamic control flow: because >>= allows binding any function as a continuation, an action in a monad can construct an arbitrary action to execute next, dynamically.<br>This also forces a clear direction to evaluation: the left effects have to happen before the right effects, because the result of the left action is used to determine the whole action on the right.<br>This also disallows static analysis: the constant functor Const is not an interesting monad.The reason it does not have a Monad instance at all is because it would not be compatible with the much more compelling Applicative instance.

This is in contrast to applicative functors, which have no “arrow of time”: their structure can be dualized to run effects in reverse because it has no control flow required by the interface.Of course particular applicative functors can have interesting control flow themselves, via combinators other than .<br>And their static analysis, given by Monoid m => Applicative (Const m), uses monoids to accumulate information about each action that was sequenced by .

Selective applicative functors sit in the sweet spot of expressing finite control flow: they allow (but do not require) that an implementation choose between a finite number of branches of otherwise static control flow.

This means that we need something that restricts >>= to finite-case functions to encode exclusive determined choice.

This will be defined as a CaseTree data type below.

It turns out that the most natural setting is to consider arrows instead of functors.<br>The functor can be recovered as an arrow out of the unit type (spelled () in Haskell and Unit in PureScript).

Any approach that does not consider arrows seems doomed to failure, mainly for the reason that we want to work with coproducts (either :: (x -> r) -> (y -> r) -> (Either x y -> r)) which involves the domain in an essential manner, while products (tuple :: (i -> x) -> (i -> y) -> (i -> Tuple x y)) stay in the codomain and thus are more amenable to restricting to actions on functors.

The concept that we need, of “finite-case functions”, is a bit tricky to formulate (especially in programming data types: it needs existential types), which I believe is part of why it has been missed.

However, once we focus on the arrows instead of the applicative actions in isolation, it can all pop into place and it pays off in revealing details of the structure we were really after.

For example, we learn that selective applicative functors allow static analysis via near-semirings by using a constant functor.<br>(That is, we define static analysis to be an interpretation into a constant functor, and we learn that near-semirings are the algebraic structure we need to make it work.)

The common formulation of select :: f (Either u v) -> f (u -> v) -> f v...