Could the `Applicative` instance for `These` preserve more "failure" information?

Question

I'm looking at the These datatype from the these package, in particular at its Applicative instance:

instance (Semigroup a) => Applicative (These a) where
    pure = That
    This  a   <*> _         = This a
    That    _ <*> This  b   = This b
    That    f <*> That    x = That (f x)
    That    f <*> These b x = These b (f x)
    These a _ <*> This  b   = This (a <> b)
    These a f <*> That    x = These a (f x)
    These a f <*> These b x = These (a <> b) (f x)

If one of the These is a This, the result is always This. However, there seems to be a certain assymetry.

Here, if the second component is a These constructor, its information is completely discarded:

    This  a   <*> _         = This a

here the first component is a These constructor, but the a part is preserved in the result.

These a _ <*> This  b   = This (a <> b)

Testing it in ghci:

ghci> This "a" <*> These "b" True
This "a"
ghci> These "a" not <*> This "b"
This "ab"

But what if we added a case at the beginning like

This  a <*> These b _    = This (a <> b)

Would that break the Applicative laws?

Crying

Interesting observation. My guess is that the Applicative instance has to be biased in this way to be compatible with the Monad one, and that a different, more symmetrical, instance should be possible, along the lines of what Validation is for Either. (I haven't thought it through yet, though.) – Involuntary

The monad instance needs to define ` This a >>= g, and there's no way to call g` here, so the only sensible result is This a. I guess this forces the bias mentioned by duplode. Perhaps we could also have a non-monad variant of These which is more symmetrical. Anyway, you could try to run QuickCheck on the applicative laws just for fun. – Phraseology

Answer 1

Your proposed instance is lawful. One way of showing that is by approximating These by a pair of maybes:

{-# LANGUAGE GHC2021, LambdaCase, PatternSynonyms #-}
import Data.These
import Data.Functor.Product
import Data.Functor.Const

newtype NotQuiteThese a b = NQT (Product (Const (Maybe a)) Maybe b)
    deriving (Show, Functor, Applicative)

pattern Neither = NQT (Pair (Const Nothing) Nothing)
pattern This' a = NQT (Pair (Const (Just a)) Nothing)
pattern That' b = NQT (Pair (Const Nothing) (Just b))
pattern These' a b = NQT (Pair (Const (Just a)) (Just b))

theseToNqt :: These a b -> NotQuiteThese a b
theseToNqt = \case
    This a -> This' a
    That b -> That' b
    These a b -> These' a b

-- nqtToThese . theseToNqt = Just
nqtToThese :: NotQuiteThese a b -> Maybe (These a b)
nqtToThese = \case
    Neither -> Nothing
    This' a -> Just (This a)
    That' b -> Just (That b)
    These' a b -> Just (These a b)

NotQuiteThese is not isomorphic to These because of the superfluous Neither case. For our current purposes, though, that is not a problem: the encoding used here gives rise to an instance Semigroup a => Applicative (NotQuiteThese a) which is equivalent to your proposed instance as far as the non-Neither cases are concerned. (The first Maybe lifts the semigroup to a monoid, Const further lifts it to an applicative functor, and the product of applicatives is applicative.) Below is a quick demonstration:

ghci> nqtToThese $ theseToNqt (These "foo" (2*)) <*> theseToNqt (This "bar")
Just (This "foobar")
ghci> nqtToThese $ theseToNqt (This "foo") <*> theseToNqt (These "bar" 7)
Just (This "foobar")

The asymmetry in the canonical instance for These is imposed for the sake of compatibility with the Monad instance, so that (<*>) = ap holds. The unavoidable This a >>= _ = This a clause means ap (This a) _ = This a. This situation is analogous to the contrast between Either and its error-accumulating variant, Validation.

On a final note, if a These-plus-Neither type is ever necessary for practical purposes, you can use Can from the smash package -- as long as you don't mind Can having a Monad instance and thus an asymmetric Applicative as well.

Involuntary