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

branch :: Selective f => f (Either a b) -> f (a ->...

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
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
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. 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 determined choice. 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. 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. 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. 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. 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 <*>. 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. 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. (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 does not capture this story. This select is a specialization to where one branch is a constant identity branch, and the general formulation cannot be recovered perfectly. That is, select allows for finite choice / optional effects, but it cannot encode which branches of control flow are exclusive.

We can squeeze it all into a single data type for a free arrow (a strong profunctor and a category) like this, subject to some laws.

data ControlFlow f i r where
Action :: (f (i -> r)) -> ControlFlow f i r
Pure :: (i -> r) -> ControlFlow f i r
-- `j` is existential here
Sequencing :: ControlFlow f i j -> ControlFlow f j r -> ControlFlow f i r
Absurd :: (i -> Void) -> ControlFlow f i r
-- `x` and `y` are existential here
CaseBranch ::
(i -> Either x y) ->
ControlFlow f x r ->
ControlFlow f y r ->
ControlFlow f i r

We then recover the free selective applicative as FreeSelective f = ControlFlow f ().

In search of a monoidal tensor

Monoidal tensors are associative up to isomorphism: x⊗(y⊗z)≅(x⊗y)⊗zx \otimes (y \otimes z) \cong (x \otimes y) \otimes z. Making them monoidal is an identity object: I⊗x≅x≅x⊗II \otimes x \cong x \cong x \otimes I. They may also satisfy symmetryin two ways, see the difference between braided monoidal categories and symmetric monoidal categories: x⊗y≅y⊗xx \otimes y \cong y \otimes x.

Monoids are a really nice setting for computation, and their symmetries (associativity, and left and right identities) ensure that we can focus on structure that matters while systematically ignoring the structure that does not matter.

Having the categorical structure also enables us to separate data that the program manipulates from the structure of the program itself. Finally, we consider static analysis as the analogous laws on plain monoids (not functors) via the constant functor (decategorification).

So we want an explanation of selective applicative functors in terms of monoidal tensors.

Tensorfail

Most explanations are missing the point of what should be possible with selective applicatives: they search for a tensor that can explain something about select :: f (Either u v) -> f (u -> v) -> f v.

One suggestionWhich I have seen a couple times is that it should come from a lax monoidal action on coproducts, of the shape f (Either u v) -> Either (f u) (f v), but that is just wrong: that is the wrong kind of static analysis for selective applicatives to support, as it would require evaluating the control flow purely statically, meaning that f cannot contain any interesting effects after all.

That is: Lax actions over coproducts (f (Either u v) -> Either (f u) (f v)) are incredibly rare in programming (or Set-like categories, more formally). It is clear that motivating examples of selective applicative functors do not satisfy this. We will in fact see that selective applicative structures are much more plentiful than monads or applicatives.

Another approach I looked at is viewing it through the lens of possibly-constant functions, like Either (u -> v) v. These are not nicely behaved either: they do not form a categoryat least not with nice properties, and even computationally, since we cannot detect constant functions in general, it is not clear why the computationally distinguished constant functions should be treated specially. Which is silly, because the point of these functors is all about computation, and I believe there is a nice story for it in category theory too!

So we need to change our approach and recognize that select is not a primitive that composes nicely: it does not have a monoidal tensor, so it is not the operation we should be looking at.

We need monoids if we are to determine what “composes nicely” even means. The failure of select to faithfully reproduce branch (or at least the failure of branch to faithfully reproduce a ternary branch) is exactly the failure of finding a tensorial explanation for what is happening.

We need to work harder to find the tensor in selective applicative functors, if we want to see a compositional story.

Finite continuations

Letʼs revisit the idea of adapting (>>=) :: f i -> (i -> f r) -> f r into a function with a finite number of cases. Can we find a data type that encodes this idea?

Not quite good enough

An idea that is a non-starter is just requiring that i is a finite type here: that would allow enumerating the cases f r, but there is no way to pass non-finite data from i to r (like branch :: f (Either x y) -> f (x -> r) -> f (y -> r) -> f r clearly does).

Slightly better would be something like f (idx, dat) -> (idx -> f (dat -> r)) -> f r, where idx is finite, and dat is non-finite data that can be processed to obtain r. But again this is unsatisfactory, since dat cannot depend on the chosen index, which again is something that branch can do (and this really matters if one case results in Void, for example, and you need to use absurd).

If we had dependent types, we could do IsFinite idx -> f (Σ (i : idx), dat i) -> (Π (i : idx), f (dat i -> r)) -> f r, which would adequately describe what we want. But we do not have dependent types in Haskell, and it does not feel like dependent types should be necessary, even if they are convenient. And it does not particularly get us closer to a categorical formulation.

Branching

So … letʼs revisit the type of branch again.

We want branch :: f (Either x y) -> f (x -> r) -> f (y -> r) -> f r to look more like (>>=) :: f i -> (i -> f r) -> f r. Is there a type Branch f i r that can replace the arrow (i -> f r) to make it happen?

We can mechanically write a datatype that expresses this: when i is of the form Either x y, then we should have the data f (x -> r) and f (y -> r):

data Branch f i r where
Branch ::
f (x -> r) ->
f (y -> r) ->
Branch f (Either x y) r

Matching on Branch gives the type equality i ~ (Either x y), but this is not essential, since we can always map an arbitrary f i on the left into a type that is of the form f (Either _ _) using (<$>). So it suffices to just have a function i -> Either x y instead of an equality.

Similarly, we will use i -> Void later, where we could have used a type equality.

This generalization is not crucial, per se. But it is convenient to work with ordinary profunctors down the line, instead of type equalities.

Finally, to generalize this, we want to be able to recurse: instead of stopping at singleton branches f (x -> r) and f (y -> r), what if we continued on to finitely more branches before getting to continuations of the form f (_ -> r)? Can we form an actual case tree?

Tensorful

Here is the final result, an arrow CaseTree f i r to replace the monadic arrow (i -> f r), making use of those observations.

class Casing f where
caseTreeOn :: forall i r. f i -> CaseTree f i r -> f r

data CaseTree f i r where
TwoCases ::
-- How to split the input into data for each case
-- (Note that `x` and `y` are existential here!)
(i -> Either x y) ->
-- Control flow for the `Left` case
(CaseTree f x r) ->
-- Control flow for the `Right` case
(CaseTree f y r) ->
CaseTree f i r
-- One static effect
OneCase :: (f (i -> r)) -> CaseTree f i r
-- Represent an empty case branching
ZeroCases :: (i -> Void) -> CaseTree f i r

-- We can recover `select` and `branch`
branch :: Casing f => f (Either x y) -> f (x -> z) -> f (y -> z) -> f z
branch input left right = caseTreeOn input $
TwoCases id (OneCase left) (OneCase right)

select :: Applicative f => Casing f => f (Either u v) -> f (u -> v) -> f v
select input continue = caseTreeOn input $
TwoCases id (OneCase $ pure id) (OneCase continue)

-- But the general form of `TwoCases` recursing into further `TwoCases`
-- is necessary to really express the structure of exclusive branching

You should think of CaseTree f i r as a “finite-case” function from datatype i to datatype r, with effects in the functor f. It is a restricted form of i -> f r, as this function demonstrates we can get back to the monadic arrow:

-- | One thing you can do is apply a `CaseTree` to a specific value of `i` to see
-- | what branch it chooses. This lets you apply it via `>>=`.
applyCaseTree :: forall i f r. Functor f => CaseTree i f r -> i -> f r
applyCaseTree (ZeroCases toVoid) i = absurd (toVoid i)
applyCaseTree (OneCase fir) i = fir <&> ($ i)
applyCaseTree (TwoCases fg x y) ij =
case fg ij of
Left i -> applyCaseTree x i
Right j -> applyCaseTree y j

Or, we can execute all effects from the f (_ -> r)s and get f (i -> r) simply by doing the case analysis at the level of the inner functions.

-- | The other way to apply it is via `<*>`, which means we do not get to skip
-- | executing any branches.
mergeCaseTree :: forall i f r. Applicative f => CaseTree i f r -> f (i -> r)
mergeCaseTree (ZeroCases toVoid) = pure (absurd . toVoid)
mergeCaseTree (OneCase fir) = fir
mergeCaseTree (TwoCases fg x y) =
liftA2 (\f g ij -> either f g (fg ij)) (mergeCaseTree x) (mergeCaseTree y)

This data type has a ton of structure. As a start, note that it is a profunctor: we can map the output covariantly, with map :: (r -> r') -> CaseTree f i r -> CaseTree f i r', and the input contravariantly, with a function of type (i' -> i) -> CaseTree f i r -> CaseTree i' f r.

This is the full mapping function: to transform from CaseTree f i r to CaseTree f' j r', you need a function j -> i, a natural transformation f ~> f', and a function r -> r'.

mapCaseTree :: forall f f' i j r r'. Functor f' =>
(forall d. f d -> f' d) -> (j -> i) -> (r -> r') -> CaseTree f i r -> CaseTree f' j r'
mapCaseTree _ g _ (ZeroCases toVoid) = ZeroCases (toVoid . g)
mapCaseTree f g h (OneCase fir) = OneCase (dimap g h <$> f fir)
mapCaseTree f g h (TwoCases split cx cy) =
TwoCases (split . g) (mapCaseTree id g h cx) (mapCaseTree id g h cy)

Note that the recursion in TwoCases handles f up front and recurses with f = id on the existential types x and y.

Having the Yoneda lemma for this functor is important for the laws below, to ensure that no generality is lost by using id :: Either x y -> Either x y to fill in split :: i -> Either x y.

Importantly, note that the return r and even the input i are ordinary data: we can just map over them with arbitrary functions, they donʼt need to be special finite functions at all. The finite structure is all contained in CaseTree.

More structure

We can give CaseTree (and ControlFlow below) the structure of a strong profunctor, which preserves some piece of state s across the input into the output.

instance Functor f => Strong (CaseTree f) where
first :: forall s j r. CaseTree f j r -> CaseTree f (j, s) (r, s)
second :: forall s j r. CaseTree f j r -> CaseTree f (s, j) (s, r)
instance Applicative f => Choice (CaseTree f) where
left :: forall i j r. CaseTree f j r -> CaseTree f (Either j i) (Either r i)
right :: forall i j r. CaseTree f j r -> CaseTree f (Either i j) (Either i r)

The first thing we may think of doing with this is simply preserving the input itself, which is an important manipulation later for making ControlFlow behave like an applicative functor (similar how the Reader monad has to keep its argument around).

keep :: Strong p => p i r -> p i (i, r)
keep f = lmap (join (,)) (second f)

We can use this to curry the CaseTree, pulling a function from the codomain into a tuple in the domain.

curry :: Strong p => p i (j -> r) -> p (i, j) r
curry = uncurry ($) <$> first cases

And a few other functions that mean that a strong profunctor acts like the familiar relation between a function domain and its codomain:

lowerFn :: Strong p => p () (i -> r) -> p i r
lowerFn c = dimap pure (uncurry ($)) (first c)

lowerArg :: Strong p => p () i -> p (i -> r) r
lowerArg c = dimap pure (uncurry (&)) (first c)

This exposes the monoidal structure between tensors we were looking for, enabling us to talk about laws and algebraic structure.

We can express associativity with TwoCases, and the identity between TwoCases and ZeroCases. These are not equalities in the data type CaseTree itself: these are laws that we expect to apply to implementations of Casing f (selective applicative functors).

Using the associativity of the tensor Either, we can express associativity of CaseTree (Either x (Either y z)) f r. (By the Yoneda lemma, any other choice of xyz that maps into Either x (Either y z) works just as well.)

assoc :: Either x (Either y z) -> Either (Either x y) z
assoc (Left x) = Left (Left x)
assoc (Right (Left y)) = Left (Right y)
assoc (Right (Right z)) = Right z

cx :: CaseTree f x r
cy :: CaseTree f y r
cz :: CaseTree f z r

TwoCases id cx (TwoCases id cy cz) ~=
TwoCases assoc (TwoCases id cx cy) cz

We know that Either has the identity Void.

absurd :: Void -> x

idL :: Either Void x -> x
idL = either absurd id
idR :: Either x Void -> x
idR = either id absurd

cx :: CaseTree f x r

TwoCases Left cx (ZeroCases absurd) ~= cx
TwoCases Right (ZeroCases absurd) cx ~= cx

Either is also a symmetric tensor, but the selective applicative functor may not always respect this symmetry.

sym :: Either x y -> Either y x
sym (Left x) = Right x
sym (Right y) = Left y

TwoCases id cx cy ~= TwoCases sym cy cx

Optionally, we can consider a kind of idempotence:

collapse :: Either x x -> x
collapse (Left x) = x
collapse (Right x) = x

TwoCases id (OneCase cx) (OneCase cx) ~=? OneCase (lmap collapse <$> cx)

This idempotence is generally bad from a computational point of view: the fact that cx appears in both cases means it is not decidable when/how this law would apply, it would require deciding whether two effects in f are equal. But for running the program, and for some forms of static analysis (with semilattices), it should hold.

---

Note that this is just a data structure. It is a data structure with existential types (x and y) and non-uniform recursion over those existential types (CaseTree f i r recurses into CaseTree f x r and CaseTree f y r). But it is still a finite data structure that you can recurse over.

---

You can think of CaseTree as performing two functions: it first splits the input i into a n-ary tensor product Either x (Either y (...)) (where the details of associativity and empty cases should not matter in the end), and then it provides an action specifically for each case it split into: (f (x -> r), f (y -> r), ...).

You could split these functions into their own data types, with a common index to make sure that they agree. That indexing type would have to be a binary tree of types, which is unpleasant without dependent types. Then you would existentially quantify over it to recover CaseTree. But CaseTree is a nice direct formulation of their composite.

---

the i has migrated inside the f, so now it has passed from the “static analysis” boundary over to the runtime side of the data and we no longer care about its branching structure, it has become a blob of arbitrary data

Free constructions and arrows

To return to the theoretical considerations.

The free monad gets a lot of attention.

data FreeMonad f r = Return r | Join (f (FreeMonad f r))

-- More suggestively
data FreeMonad f r
= Return r
| Join (Compose f (FreeMonad f r))

But the free applicative is much less common. Why is this?

Well, one reason is that it requires the Day convolution, which requires existential types. And we have already established that programmers avoid thinking about existential types.

data FreeApplicative f r
= Pure r
| Apply (Day f (FreeApplicative f) r)

-- This is the style that directly relates to `(<*>)`
data Day f g r where
-- Existential `i`
Day :: f (i -> r) -> g i -> Day f g r

-- This is the obviously-symmetric formulation
data Day f g r where
-- Existential `x` and `y`
Day :: f x -> g y -> (x -> y -> r) -> Day f g r

Monoid objects in monoidal categories

However, those are specifically the formulation of monads and applicatives as monoid objects (in a monoidal category). That is the source of the “a monad is just a monoid in the [monoidal] category of endofunctors [under composition]” meme, while an applicative functor is “just” a monoid in the [monoidal] category of endofunctors under Day convolution.

I argue that it is important to include “under composition” in the description of the monad, because there are many monoidal products available on functors, and functor composition is a surprising choice, since it is not symmetric at all!

In fact, you can think of the Day convolution as a symmetrization of the composition tensor: there is a natural map Day f g ~> Compose f g, and since Day is symmetric, it also has a map Day f g ~> Compose g f via Day g f ~> Day f g.

The monoid operation is an arrow merge⁡:M⊗M→M\operatorname{merge} : M \otimes M \to M in the functor category: that is, a natural transformation.

So for monads it is join :: Compose f f ~> f, which is just forall r. f (f r) -> f r, and for applicatives it is liftA2 :: Day f f ~> f, which expands to forall r x y. (x -> y -> r) -> f x -> f y -> f r, at which point we can either take x = (y -> r) and apply id to get back (<*>), or we can take r = (x, y) and apply (,) to get a tupling function below.

Applicative functors can also be thought of as lax monoidal functors (between two monoidal categories), which come with an operation tupling⁡:f(x)⊗f(y)→f(x⊗y)\operatorname{tupling} : f(x) \otimes f(y) \to f (x \otimes y). (In the case of applicative functors, both ⊗{\otimes} are the product ×{\times}.)

As we just said, it comes from the fact that a universal choice for the (x -> y -> r) function is the tuple constructor: because that preserves information, any other choice factors through it.

Arrows

We can formulate them differently. Instead of thinking of monads and applicatives as lax monoidal functors, we can think of them as arrows.

As a warmup, a free category can be expressed as

data FreeCategory p i o where
Id :: FreeCategory p y y
-- Existential `y`
Compose :: p x y -> FreeCategory p y z -> FreeCategory p x z

(This is an analogous structure to the humble cons list, since it has the non-recursive structure p _ _ on the left and the recursion FreeCategory p _ _ on the right.)

(Note that there’s some trickery around categories that are also profunctors here [indeed, profunctors with strength], that we will sidestep by only working in categories based on functions.)

newtype MonadArrow f i r = MonadArrow (i -> f r)
newtype FreeMonad f r = FreeMonad
(FreeCategory (MonadArrow f) Unit r)

newtype ApplicativeArrow f i r = ApplicativeArrow (f (i -> r))
newtype FreeApplicative f r = FreeApplicative
(FreeCategory (ApplicativeArrow f) Unit r)

The “monad arrow” here is also known as the Kleisli category of the monad f.

It turns out that the “applicative arrow” is explained as a change of enriching category (via f being a lax monoidal functor), even though we are only going from Set (which is itself a Set-enriched category) back to a different Set-enriched category (whose arrows are f (i -> r)).

We can form an arrow to model the free selective applicative by using CaseTree as our arrow type, as it already includes ApplicativeArrows as a special case (OneCase).

type SelectiveArrow = CaseTree
newtype FreeSelective f r = FreeSelective
(FreeCategory (SelectiveArrow f) Unit r)

However, it is nice to write out the cases like this, to really grasp how they model control flow for an applicative functor:

data ControlFlow f i r where
Action :: (f (i -> r)) -> ControlFlow f i r
Pure :: (i -> r) -> ControlFlow f i r
CaseFlow :: CaseTree (ControlFlow f Unit) i r -> ControlFlow f i r
Sequencing :: ControlFlow f i x -> ControlFlow f x r -> ControlFlow f i r

One function that is important to convince ourselves that ControlFlow really captures control flow, is this sequencing function, which distributes the remaining control flow across each branch of a CaseTree (like a category – matching up output and input).

sequenceCaseTree ::
forall i j f r.
Functor f =>
CaseTree (ControlFlow f Unit) i j ->
ControlFlow f j r ->
CaseTree (ControlFlow f Unit) i r

It is used to implement uncons (Sequencing _ _), which says that we can think of each ControlFlow as starting with a CaseTree if we want. (For Pure and Action, this is a single-branch case tree.)

uncons ::
forall f i r.
Functor f =>
ControlFlow f i r ->
CaseTree (ControlFlow f Unit) i r
uncons (Pure ir) = OneCase (Pure (const ir))
uncons (Action fir) = OneCase (Action (const <$> fir))
uncons (CaseFlow cases) = cases
uncons (Sequencing ab bc) =
sequenceCaseTree (uncons ab) bc

Finally, this tells us that we can split control flow over ControlFlow f (Either x y) just like we do for CaseTree.

bifurcate ::
forall x y i f r.
Functor f =>
(i -> Either x y) ->
ControlFlow f x r ->
ControlFlow f y r ->
ControlFlow f i r
bifurcate fg x y = CaseFlow $ TwoCases fg (uncons x) (uncons y)

Notice that we can essentially inline CaseTree into this data type too:

data ControlFlow f i r where
Action :: (f (i -> r)) -> ControlFlow f i r
Pure :: (i -> r) -> ControlFlow f i r
-- `j` is existential here
Sequencing :: ControlFlow f i j -> ControlFlow f j r -> ControlFlow f i r
Absurd :: (i -> Void) -> ControlFlow f i r
-- `x` and `y` are existential here
CaseBranch ::
(i -> Either x y) ->
ControlFlow f x r ->
ControlFlow f y r ->
ControlFlow f i r

However, this is not incredibly useful: a lot of forms of static analysis really want to deal with case branches at once, so they would need to detect CaseBranch and re-gather all the branches up.

Note that even if f is the type of functor where you could statically analyze the values in it (e.g. List as opposed to IO), we are instantiating it with an unknown function type.

I say unknown function type here because even if you could technically analyze the first action in ControlFlow f i r when i is finite, the fact that Sequencing (Pure id) _ constructs another equivalent (equal?) ControlFlow f i r where you can no longer analyze the first action on that basis (since it is now hidden behind an existential) means that you should not.

This hints to us that we can construct another type that consists of all the static information of ControlFlow, forgetting all of the functions (as they are unanalyzable) and thus all of the types:

data FlowInfo f where
Info :: f () -> FlowInfo f
Pure :: FlowInfo f
Sequencing :: FlowInfo f -> FlowInfo f -> FlowInfo f
Absurd :: FlowInfo f
CaseBranch :: FlowInfo f -> FlowInfo f -> FlowInfo f

-- In fact, it is an ordinary ADT now
data FlowInfo f
= Info (f ())
| Pure
| Sequencing (FlowInfo f) (FlowInfo f)
| Absurd
| CaseBranch (FlowInfo f) (FlowInfo f)

Notice how this looks like an untyped AST for a program now! We removed the existentials and the polymorphic recursion: it is the plainest of plain data types now.

In fact, you might spy what it has turned into: it is a free semiring, or something close to it. (Specifically it should be a near-semiring.)

summarize :: NearSemiring m => (f () -> m) -> FlowInfo f -> m
summarize f2m (Info f) = f2m f
summarize _ Pure = one
summarize f2m (Sequencing l r) = summarize f2m l * summarize f2m r
summarize _ Absurd = zero
summarize f2m (CaseBranch l r) = summarize f2m l + summarize f2m r

From the laws for a category, we know that Sequencing should be associative. We also have that Sequencing (Pure id) f ~ f ~ Sequencing f (Pure id) should all be equivalent. So once we forget the functions (by going from ControlFlow f i r to FlowInfo f), we need to treat all Pure :: FlowInfo f as equivalent.From a computational point of view, this is because we allow arbitrary type shuffling, while still treating them as trivial programs from the point of view of the computation that f encodes. So Pure is the identity for whatever operation we map Sequencing to.

Similarly we have that CaseBranch is associative, and its identity is Absurd.

We also would like to have that CaseBranch is commutative. The order of cases should not matter, since only one will be taken – in the monadic interpretation, at least. But we should be careful about making such strong determinations about what should and should not count, since that is what has led previous lines of reasoning about selective applicative functors astray. In particular, imposing this law on all instances would mean that a lot of useful instance derived from applicatives are not allowed.Note that for rings, and semirings with additive cancelation, commutativity of addition follows form two-sided distributivity, but this is not an issue for near-semirings as they only have one-sided distributivity.

Finally, we have the matter of distributivity. It turns out that we should only have one sided distributivity: (x + y) * z = x * z + y * z, which implies 0 * z = 0. (This is what makes it a near-semiring instead of a semiring.)

The other side of distributivity is not easy to satisfy for programs, in particular. The distributivity laws above work well for programs, but the other direction does not apply so well:

• 0 * z = 0 means that anything after absurdity does not matter (it is not going to get run!), while z * 0 = 0 is suspect only because z may have side effects that run before it gets to absurdity, which could be important to keep track of (especially if error recovery is a possibility).The functor result does not matter, since it is coming from absurdity!
• (x + y) * z = x * z + y * z says that control flow proceeds with the shared control flow after case branches, while z * (x + y) = z * x + z * y would require unbounded backtracking.

This makes sense, especially because we are encoding determined choice, where earlier results determine later control flow. We should not be surprised if an arrow of time occurs in our equations!

Arrow transformer

You might note that weʼve barely been using f here, just as a placeholder for a convenient arrow type. This suggests that we could formulate ControlFlow as a arrow transformer, and require the right kind of arrow p (a strong profunctor and category, at least) to make ControlFlowT p behave as we want.

data ControlFlowT p i r where
Action :: p i r -> ControlFlow f i r
Pure :: (i -> r) -> ControlFlow f i r
Sequencing :: ControlFlow f i j -> ControlFlow f j r -> ControlFlow f i r
Absurd :: (i -> Void) -> ControlFlow f i r
CaseBranch ::
(i -> Either x y) ->
ControlFlow f x r ->
ControlFlow f y r ->
ControlFlow f i r

I have not thought about this much.

Alternative

Finally it is time to address the elephant in the room: what does this have to do with <|> from Alternative?

As I mentioned in the overview, (<|>) :: f x -> f x -> f x (alternatively: f x -> f y -> f (Either x y)) is a combinator for nondeterministic choice, where the combinator itself does not give any information about which branch to take, it is completely up to the implementation.

The main examples of this are LogicT (a monad transformer that encodes nondeterminism, layering List semantics on top of another monad), and parser combinator transformers, the simplest of which would be a hypothetical ParserT. You can think of the basic monads Maybe, Either, List as simplifications of these ideas.

newtype ParserT m a =
ParserT { unParserT :: String -> m (Either Bool (String, a)) }

instance Functor m => Alt (ParserT m) where
ParserT l <|> ParserT r = ParserT \input -> do
parsedL <- l input
case parsedL of
Right parsed ->
pure parsed
Nothing ->
-- This encodes backtracking: restarting on the same input
-- But usually parser combinators check that the input was
-- not consumed at all, and use a combinator to enable
-- backtracking in those cases.
r input

--------------------

newtype LogicT m a =
LogicT { unLogicT :: forall r. (a -> m r -> m r) -> m r -> m r }

instance Functor m => Alt (LogicT m) where
LogicT l <|> LogicT r = LogicT \cons nil ->
l cons (r cons nil)

observeAllT :: Applicative m => LogicT m a -> m [a]

observeManyT :: Monad m => Int -> LogicT m a -> m [a]

ParserT is the most important example of the usefulness of <|>, where even something as simple as taking different actions based on different characters of input is encoded using <|>.

LogicT is a monad transformer with pervasive backtracking, modeling nondeterminism of the kind “run every possible computation to find every possible result”, essentially. It can also be lazily explored with observeManyT, to only obtain the first few results.

Still, the common theme is that to obtain even one successful result, backtracking deeply through the computation may be necessary.

Because they are both monads, they support: f (Maybe x) -> f x, via (_ >>= maybe empty pure). This operation makes sense in some applicatives, too, but it needs a specialized implementation. So generally we will talk about mapMaybe :: (x -> Maybe y) -> f x -> f y.

Indeed, we want to talk about structures on applicative functors simply because ParserT and LogicT have no capability for static analysis, as they are monads. So can we combine mapMaybe and <|> to get an explanation of select, branch, and so on?

The answer is yes: If we have an applicative parser without other side effects (i.e. m = Identity) and with enough backtracking, we could encode determined choice via nondeterministic choice.

selectLeft :: Filterable f => f (Either x y) -> f x
selectLeft = mapMaybe \case
Left x -> Just x
Right _ -> Nothing
selectRight :: Filterable f => f (Either x y) -> f y
selectRight = mapMaybe \case
Left _ -> Nothing
Right y -> Just y

branch :: Applicative f => Filterable f => f (Either x y) -> f (x -> r) -> f (y -> r) -> f r
branch determiner leftCase rightCase =
liftA2 (&) (selectLeft determiner) leftCase
<|>
liftA2 (&) (selectRight determiner) rightCase
-- ^ This easily generalizes to n-ary branches, unlike `branch` itself

Because this duplicates determiner, it would only be safe for things like ParserT Identity which does not have observable side effects from failed branches.Strictly speaking, you could have idempotent effects: f *> f = f. And it requires backtracking all the way back to before determiner to even catch a Right case out of it, which is something that parser combinators generally avoid for efficiency (for good reason!).

However, this makes sense for LR parser combinators (yes those are a thing! they are necessarily applicative parsers and not monadic). All of the backtracking is resolved ahead of time in LR parser combinators, thanks to the powers of static analysis. It just requires the capability to prune branches at runtime for mapMaybe, which not all LR parsers support.

And importantly: despite the fact that the branching can be explained via <|> and mapMaybe, it is also incredibly useful to have information about CaseTree, because that can be used to help ensure that the parser is not ambiguous.

Finally, it is interesting to note that Alternative functors have also been explained as categorified near-semirings (and thus support static analysis via near-semirings): From monoids to near-semirings: the essence of MonadPlus and Alternative by Exequiel Rivas, Mauro Jaskelioff, and Tom Schrijvers explains the typeclass laws, free constructions, and Cayley constructions (à la difference lists) from this perspective.Note that we could product a similar datatype for CaseTree and ControlFlow, that is a right-associated free construction with an efficient Cayley construction, but in the case of determined choice, this would turn binary search of the case tree into linear search, compromising efficiency.

So the conclusion is that the branching structures of Alternative and Selective are closely related, but not identical. The Alternative can be thought of as a functor with nondeterministic branching, while Selective needs to be explained via arrows to encode finite deterministic branching. They both allow retaining the structure of branches as independent from the sequential structure, and the selective structure can be encoded via <|> and mapMaybe in some well-behaved cases.

Conclusion

Selective applicative functors are all about control flow with determined choice: the result of previous actions will determine which branch should be taken. In order to keep track of which branches are exclusive from each other, and to explain it via tensors, we have to explain it as a theory of arrows, not of functors. This is useful for tracking or preventing ambiguity during parsing, as one example.

data CaseTree f i r where
TwoCases ::
-- How to split the input into data for each case
-- (Note that `x` and `y` are existential here!)
(i -> Either x y) ->
-- Control flow for the `Left` case
(CaseTree f x r) ->
-- Control flow for the `Right` case
(CaseTree f y r) ->
CaseTree f i r
-- One static effect
OneCase :: (f (i -> r)) -> CaseTree f i r
-- Represent an empty case branching
ZeroCases :: (i -> Void) -> CaseTree f i r

-- Typeclass, subject to some laws
class Casing f where
caseTreeOn :: forall i r. f i -> CaseTree f i r -> f r

-- Free structure
data ControlFlow f i r where
Action :: (f (i -> r)) -> ControlFlow f i r
Pure :: (i -> r) -> ControlFlow f i r
CaseFlow :: CaseTree (ControlFlow f Unit) i r -> ControlFlow f i r
-- `j` is existential here
Sequencing :: ControlFlow f i j -> ControlFlow f j r -> ControlFlow f i r

-- Alternative formulation of the free structure
data ControlFlow f i r where
Action :: (f (i -> r)) -> ControlFlow f i r
Pure :: (i -> r) -> ControlFlow f i r
-- `j` is existential here
Sequencing :: ControlFlow f i j -> ControlFlow f j r -> ControlFlow f i r
Absurd :: (i -> Void) -> ControlFlow f i r
-- `x` and `y` are existential here
CaseBranch ::
(i -> Either x y) ->
ControlFlow f x r ->
ControlFlow f y r ->
ControlFlow f i r

Despite requiring slightly more involved concepts to explain (arrows and existential types), it solidifies into a structure that looks like ordinary control flow constructs that one might write in an AST for a programming language. You can think of the applicative functor f as denoting the boundary between the ahead-of-time information available on the outside and the runtime information available to the functions (i -> r) on the inside at each step of the computation.

The requirements of selective applicative functors are intentionally flexible, to allow it to be implemented in varied ways: applicatives for simple composable sequencing and staging of effects, monads for efficient execution and flexibility, near-semirings for static analysis, with the selective applicative structure as a common meeting ground for all of it.

The laws follow the structure of a near-semiring.

• Multiplicative associativity: Sequencing (Sequencing f g) h = Sequencing f (Sequencing g h)
• Multiplicative identity: Sequencing (Pure id) f = f = Sequencing f (Pure id)
• Additive associativity: TwoCases id cx (TwoCases id cy cz) = TwoCases assoc (TwoCases id cx cy) cz
• Additive identity: TwoCases Left cx (ZeroCases absurd) = cx = TwoCases Right (ZeroCases absurd) cx
• Right distributivity: Sequencing (CaseBranch split cx cy) g = CaseBranch split (Sequencing cx g) (Sequencing cy g)
• Left absorbing element: Sequencing (Absurd absurd) g = Absurd absurd
• Optionally, (additive) commutativity: TwoCases id cx cy = TwoCases swap cx cy
• Optionally, additive idempotence: CaseBranch id cx cx = lcmap collapse cx

Next time we will study the theory of these functors from the other side: basic examples, how they compose, what would be a good syntax for them. Eventually we will look at some applications of selective applicative functors in depth, and maybe discuss what the future of functorial and arrow-like structures are: sequencing (monads and categories) and parallelism (applicatives), exclusive determined choice (selectives), nondeterministic choice (alternatives), and staging (functor composition). Can they all fit into one syntax? I mean, why not??