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?

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.