Is `data PoE a = Empty | Pair a a` a monad?

问题:

This question comes from this answer in example of a functor that is Applicative but not a Monad: It is claimed that the

data PoE a = Empty | Pair a a deriving (Functor,Eq)

cannot have a monad instance, but I fail to see that with:

instance Applicative PoE where
    pure x = Pair x x
    Pair f g <*> Pair x y = Pair (f x) (g y)
    _        <*> _        = Empty
instance Monad PoE where
    Empty    >>= _ = Empty
    Pair x y >>= f = case (f x, f y) of 
                       (Pair x' _,Pair _ y') -> Pair x' y'
                       _ -> Empty

The actual reason why I believe this to be a monad is that it is isomorphic to Maybe (Pair a) with Pair a = P a a. They are both monads, both traversables so their composition should form a monad, too. Oh, I just found out not always.

Which counter-example failes which monad law? (and how to find that out systematically?)

---

edit: I did not expect such an interest in this question. Now I have to make up my mind if I accept the best example or the best answer to the "systematically" part.

Meanwhile, I want to visualize how join works for the simpler Pair a = P a a:

                   P
          ________/ \________
         /                   \
        P                     P
       / \                   / \
      1   2                 3   4

it always take the outer path, yielding P 1 4, more commonly known as a diagonal in a matrix representation. For monad associativy I need three dimensions, a tree visualization works better. Taken from chi's answer, this is the failing example for join, and how I can comprehend it.

                  Pair
          _________/\_________
         /                    \
       Pair                   Pair
        /\                     /\
       /  \                   /  \
    Pair  Empty           Empty  Pair
     /\                           /\
    1  2                         3  4

Now you do the join . fmap join by collapsing the lower levels first, for join . join collapse from the root.

回答1:

Apparently, it is not a monad. One of the monad "join" laws is

join . join = join . fmap join

Hence, according to the law above, these two outputs should be equal, but they are not.

main :: IO ()
main = do
  let x = Pair (Pair (Pair 1 2) Empty) (Pair Empty (Pair 7 8))
  print (join . join $ x)
  -- output: Pair 1 8
  print (join . fmap join $ x)
  -- output: Empty

The problem is that

join x      = Pair (Pair 1 2) (Pair 7 8)
fmap join x = Pair Empty Empty

Performing an additional join on those does not make them equal.

how to find that out systematically?

join . join has type m (m (m a)) -> m (m a), so I started with a triple-nested Pair-of-Pair-of-Pair, using numbers 1..8. That worked fine. Then, I tried to insert some Empty inside, and quickly found the counterexample above.

This approach was possible since a m (m (m Int)) only contains a finite amount of integers inside, and we only have constructors Pair and Empty to try.

For these checks, I find the join law easier to test than, say, associativity of >>=.

回答2:

QuickCheck immediately finds a counterexample to associativity.

{-# LANGUAGE DeriveFunctor #-}

import Test.QuickCheck

data PoE a = Empty | Pair a a deriving (Functor,Eq, Show)

instance Applicative PoE where
    pure x = Pair x x
    Pair f g <*> Pair x y = Pair (f x) (g y)
    _        <*> _        = Empty
instance Monad PoE where
    Empty    >>= _ = Empty
    Pair x y >>= f = case (f x, f y) of 
                       (Pair x' _,Pair _ y') -> Pair x' y'
                       _ -> Empty

instance Arbitrary a => Arbitrary (PoE a) where
  arbitrary = oneof [pure Empty, Pair <$> arbitrary <*> arbitrary]

prop_assoc :: PoE Bool -> (Bool -> PoE Bool) -> (Bool -> PoE Bool) -> Property
prop_assoc m k h =
  ((m >>= k) >>= h) === (m >>= (\a -> k a >>= h))

main = do
  quickCheck $ \m (Fn k) (Fn h) -> prop_assoc m k h

Output:

*** Failed! Falsifiable (after 35 tests and 3 shrinks):    
Pair True False
{False->Pair False False, True->Pair False True, _->Empty}
{False->Pair False True, _->Empty}
Pair False True /= Empty

回答3:

Since you are interested in how to do it systematically, here's how I found a counterexample with quickcheck:

{-# LANGUAGE DeriveFunctor #-}

import Control.Monad ((>=>))
import Test.QuickCheck

-- <your code>

Defining an arbitrary instance to generate random PoEs.

instance (Arbitrary a) => Arbitrary (PoE a) where
    arbitrary = do
      emptyq <- arbitrary
      if emptyq
        then return Empty
        else Pair <$> arbitrary <*> arbitrary

And tests for the monad laws:

prop_right_id m = (m >>= return) == m
    where
    _types = (m :: PoE Int)

prop_left_id fun x = (return x >>= f) == f x
    where
    _types = fun :: Fun Int (PoE Int)
    f = applyFun fun

prop_assoc fun gun hun x = (f >=> (g >=> h)) x == ((f >=> g) >=> h) x
    where
    _types = (fun :: Fun Int (PoE Int),
              gun :: Fun Int (PoE Int),
              hun :: Fun Int (PoE Int),
              x :: Int)
    f = applyFun fun
    g = applyFun gun
    h = applyFun hun

I don't get any failures for the identity laws, but prop_assoc does generate a counterexample:

ghci> quickCheck prop_assoc
*** Failed! Falsifiable (after 7 tests and 36 shrinks):
{6->Pair 1 (-1), _->Empty}
{-1->Pair (-3) (-4), 1->Pair (-1) (-2), _->Empty}
{-3->Empty, _->Pair (-2) (-4)}
6

Not that it's terribly helpful for understanding why the failure occurs, it does give you a place to start. If we look carefully, we see that we are passing (-3) and (-2) to the third function; (-3) maps to Empty and (-2) maps to a Pair, so we can't defer to the laws of either of the two monads PoE is composed of.

回答4:

This kind of potential Monad instance can be concisely described as "taking the diagonal". It is easier to see why if we use the join presentation. Here is join for the Pair type you mention:

join (P (P a00 a11) (P a10 a11)) = P a00 a11

Taking the diagonal, however, is only guaranteed to give a lawful join for fixed length (or infinite) lists. That's because of the associativity law:

join . join = join . fmap join

If the n-th list in a list of lists doesn't have an n-th element, it will lead to the diagonal being trimmed: it will end before its n-th element. join . join takes the outer diagonal (of a list of lists of lists) first, while join . fmap join takes the inner diagonals first. It may be possible for an insufficiently long innermost list which is not in the outer diagonal to trim join . fmap join, but it can't possibly affect join . join. (This would be easier to show with a picture instead of words.)

Your PoE is a list-like type that doesn't have fixed length (the length is either zero or two). It turns out that taking its diagonal doesn't give us a monad, as the potential issue discussed above actually gets in the way (as illustrated in chi's answer).

Additional notes:

• This is precisely the reason ZipList is not a monad: the zippy behaviour amounts to taking the diagonal.

• Infinite lists are isomorphic to functions from the naturals, and fixed length lists are isomorphic to functions from the naturals up to an appropriate value. This means you can get a Monad instance for them out of the instance for functions -- and the instance you get, again, amounts to taking the diagonal.

• Once upon a time I got confused about this exact issue.

回答5:

(Posting this as a separate answer, as it has little overlap with my other one.)

The actual reason why I believe this to be a monad is that it is isomorphic to Maybe (Pair a) with Pair a = P a a. They are both monads, both traversables so their composition should form a monad, too. Oh, I just found out not always.

The conditions for the composition of monads m-over-n with n traversable are:

-- Using TypeApplications notation to make the layers easier to track.
sequenceA @n @m . pure @n = fmap @m (pure @n)
sequenceA @n @m . fmap @n (join @m)
    = join @m . fmap @m (sequenceA @n @m) . sequenceA @n @m
sequenceA @n @m . join @n
    = fmap @m (join @n) . sequenceA @n @m . fmap @n (sequenceA @n @m)

(There is also sequenceA @n @m . fmap @n (pure @m) = pure @m, but that always holds.)

In our case, we have m ~ Maybe and n ~ Pair. The relevant method definitions for Pair would be:

fmap f (P x y) = P (f x) (f y)
pure x = P x x
P f g <*> P x y = P (f x) (g y)
join (P (P a00 a01) (P a10 a11)) = P a00 a11 -- Let's pretend join is a method.
sequenceA (P x y) = P <$> x <*> y

Let's check the third property:

sequenceA @n @m . join @n
    = fmap @m (join @n) . sequenceA @n @m . fmap @n (sequenceA @n @m)

-- LHS
sequenceA . join $ P (P a00 a01) (P a10 a11)
sequenceA $ P a00 a11
P <$> a00 <*> a11 -- Maybe (Pair a)

-- RHS
fmap join . sequenceA . fmap sequenceA $ P (P a00 a01) (P a10 a11)
fmap join . sequenceA $ P (P <$> a00 <*> a01) (P <$> a10 <*> a11)
fmap join $ P <$> (P <$> a00 <*> a01) <*> (P <$> a10 <*> a11)
fmap join $ (\x y z w -> P (P x y) (P z w)) <$> a00 <*> a01 <*> a10 <*> a11
(\x _ _ w -> P x w) <$> a00 <*> a01 <*> a10 <*> a11 -- Maybe (Pair a)

These are clearly not the same: while any a values will be drawn exclusively from a00 and a11, the effects of a01 and a10 are ignored in the left-hand side, but not in the right-hand side (in other words, if a01 or a10 are Nothing, the RHS will be Nothing, but the LHS won't necessarily be so). The LHS corresponds exactly to the vanishing Empty in chi's answer, and the RHS corresponds to the inner diagonal trimming described in my other answer.

---

P.S.: I forgot to show that the would-be instance we are talking about here is the same one being discussed in the question:

join' ::  m (n (m (n a))) -> m (n a)
join' = fmap @m (join @n) . join @m . fmap @m (sequenceA @n @m)

With m ~ Maybe and n ~ Pair, we have:

join' :: Maybe (Pair (Maybe (Pair a))) -> Maybe (Pair a)
join' = fmap @Maybe (join @Pair) . join @Maybe . fmap @Maybe (sequenceA @Pair @Maybe)

join @Maybe . fmap @Maybe (sequenceA @Pair @Maybe) means the join' will result in Nothing unless there are no Nothings anywhere:

join' = \case
    Just (P (Just (P a00 a01)) (Just (P a10 a11))) -> _
    _ -> Nothing

Working out the non-Nothing case is straightforward:

fmap join . join . fmap sequenceA $ Just (P (Just (P a00 a01)) (Just (P a10 a11)))
fmap join . join $ Just (Just (P (P a00 a01) (P a10 a11)))
fmap join $ Just (P (P a00 a01) (P a10 a11))
Just (P a00 a11)

Therefore...

join' = \case
    Just (P (Just (P a00 _)) (Just (P _ a11))) -> Just (P a00 a11)
    _ -> Nothing

... which is essentially the same as:

join = \case
    Pair (Pair a00 _) (Pair _ a11) -> Pair (a00 a11)
    _ -> Empty