Can I model a list of successes with short circuiting failure via the composition of applicative functors?

13
votes

The user 'singpolyma' asked on reddit if there was some general structure underlying:

data FailList a e = Done | Next a (FailList a e) | Fail e

A free monad was suggested, but I wondered if this could be modeled more generally via applicative functors. In Abstracting with Applicatives, Bazerman shows us that the sum of two applicative functors is also an applicative functor, with bias to the left/right, provided we have a natural transformation in the direction of the bias. This sounds like it's what we need! Thus, I started my proposal, but then quickly ran into problems. Can anyone see solutions to these problems?:

Firstly, we start with the definition of the sum of two functors. I started here because we want to model sum types - either successes or successes and a failure.

data Sum f g a = InL (f a) | InR (g a)

And the two functors we want to work with are:

data Success a = Success [a]
data Failure e a = Failure e [a]

Success is straight forward - it's essentially Const [a]. However, Failure e I'm not so sure about. It's not an applicative functor, because pure doesn't have any definition. It is, however, an instance of Apply:

instance Functor Success where
  fmap f (Success a) = Success a

instance Functor (Failure e) where
  fmap f (Failure e a) = Failure e a

instance Apply (Failure e) where
  (Failure e a) <.> (Failure _ b) = Failure e a

instance Apply Success where
  (Success a) <.> (Success b) = Success (a <> b)

instance Applicative Success where
  pure = const (Success [])
  a <*> b = a <.> b

Next, we can define the sum of these functors, with a natural transformation from right to left (so a left bias):

instance (Apply f, Apply g, Applicative g, Natural g f) => Applicative (Sum f g) where
  pure x = InR $ pure x
  (InL f) <*> (InL x) = InL (f <*> x)
  (InR g) <*> (InR y) = InR (g <*> y)
  (InL f) <*> (InR x) = InL (f <.> eta x)
  (InR g) <*> (InL x) = InL (eta g <.> x)

And the only thing we now have to do is define our natural transformation, and this is where it all comes crumbling down.

instance Natural Success (Failure e) where
  eta (Success a) = Failure ???? a

The inability to create a Failure seems to be the problem. Furthermore, even being hacky and using ⊥ isn't an option, because this will be evaluated, in the case where you have InR (Success ...) <*> InL (Failure ...).

I feel like I'm missing something, but I have no idea what it is.

Can this be done?

2
haskellalgebraapplicativecategory-theorynon-deterministic
The naturality condition forall (f :: a -> b). eta . fmap f == fmap f . eta strongly suggests that the error component must be constant. That makes me want to write an Default e => Applicative (Failure e). – J. Abrahamson
Also, your Apply/Applicative instances are weird. I fixed the heads so that they kind-check, but they generally aren't type-checking either! Success a isn't really isomorphic to Constant [a] either, though... at the very least, it needs more type indices! – J. Abrahamson
@tel - Default seems possible, I just can't see what a sane "default error message" would be. Also, your edits were rejected by other SO editors, though they are valid. I'll apply them myself. – ocharles
The instances of Functor and Apply of Success and Failure don't typecheck. Please update them so that we have a working starting point. – Petr

2 Answers

5
votes

I'm pretty sure the "correct" answer is to make e a monoid, much as you disliked the idea on the reddit discussion.

Consider Failure "oops" [(*1),(*2),(*3)] <*> Failure "doh" [1,2,3] Should the result have "oops" or "doh" as the failure? By making the e a monoid we capture the fact that there's no canonical choice, and let the consumer pick their poison (be it First, Last, [], etc.)

Note that this solution, much like the (Maybe e, [a]) representation, doesn't deal correctly with streaming/potentially-infinite data, since it is strict in whether we have a failure ending the list.

A different encoding would use fixpoints of applicatives, as per the followup post (http://comonad.com/reader/2013/algebras-of-applicatives/).

Then you take the list representation presented there (FixF (ProductF Embed (Sum (Const ()))) a) and alter it by sticking your error monoid in the unit position, to get the following:

Monid mon => FixF (ProductF Embed (Sum (Const mon))) a

And note that you can use a Maybe instead of a monoid to get exactly a FailList, but just as with FailList you then don't get an applicative instance for free unless you write one specifying the right way to combine errors.

Also note that with the fixpoint approach if we have the equivalent of Success [(*1),(*2),(*3)] <*> Failure "doh" [1,2,3,4,5] then we get back a Success with three elements (i.e. we are genuinely nonstrict in failure) while in the approach you suggest, we get back a Failure with three elements and the error from the five element failing list. Such are the tradeoffs of streaming vs. strict.

Finally, and most straightforwardly, we can just take type FailList e = Product (Const (First e)) ZipList to use standard applicative machinery and get something very close to the original data type.

2
votes
{-# LANGUAGE FlexibleInstances #-}

instance Applicative (Sum Success (Failure e)) where
  pure x = InL $ pure x
  (InL f) <*> (InL x) = InL (f <*> x)
  (InR (Failure e fs)) <*> (InR (Failure _ gs)) = InR (Failure e (fs <*> gs))
  (InR (Failure e fs)) <*> (InL (Success gs)) = InR (Failure e (fs <*> gs))
  (InL (Success gs)) <*> (InR (Failure e fs)) = InR (Failure e (gs <*> fs))

This is because you can always add a failure to a list of successes ;)

You may also use this type class instead of Natural f g:

class Transplant f g where
  transplant :: f a -> g b -> f b

instance Transplant (Failure e) Success where
  transplant (Failure e _) (Success a) = Failure e a

Have no idea what it means category-theory-wise.