proving monad laws of a new monad instance (list of maybe)

Question

I made a new List of Maybe Monad instance and tried to prove the implementation does satisfy the Monad laws, am I doing it right or is the implementation incorrect? Any pointer is appreciated. Thanks!

newtype Test a = Test { getTest :: [Maybe a] }
  deriving Functor

instance Applicative Test where
  pure = return
  (<*>) = liftM2 ($)

instance Monad Test where
  return :: a -> Test a
  return a = Test $ [Just a]
  
  (>>=) :: Test a -> (a -> Test b) -> Test b
  Test [Nothing] >>= f = Test [Nothing]
  Test [Just x] >>= f = f x

{-
1. return x >>= f = f x
     return x >>= f = [Just x] >>= f = f x   
 
2. m >>= return = m
     [Nothing] >>= return = [Nothing]
     [Just x] >>= return = return x = [Just x] 

3. (m >>= f) >>= g    ==    m >>= (\x -> (f x >>= g))

   m = [Nothing]
   L.H.S. = ([Nothing] >>= f ) >>= g = Nothing >>= g = Nothing
   R.H.S. = [Nothing] >>= (\x -> (f x >>= g)) = Nothing
   m = [Just x]
   L.H.S. = ([Just x] >>= f) >>= g = f x >>= g
   R.H.S. = [Just x] >>= (\v -> (f v >>= g)) = (\v -> (f v >>= g)) x
          = f x >>= g
-}

It looks like you haven't finished defining it. What is Test [] >>= f or Test [Just x, Just y] >>= f? — David Fletcher
Enable warnings, they will report your pattern matching to be non-exhaustive. I didn't check your proofs, since you need to fix your >>= before. — chi
I read the Monad law proofs of the List Monad and noticed it used functions like concat and map, but it seems that I cannot use them in here. In that case, does that make the implementation significantly more difficult? — teraque
If you define pure directly, return has a default definition of return = pure, since Applicative is now a superclass of Monad. (Same amount of work, but fits with the modern Functor-Applicative-Monad hierarchy, rather than the old assumption that a Monad instance for a type already exists when it comes time to write an Applicative instance.) — chepner
You may find it easier to prove the monad laws in terms of monadic composition ((>=>) :: (a -> m b) -> (b -> m c) -> a -> m c / (<=<) = flip (>=>)) rather than application (>>= / =<<), since then they’re phrased more symmetrically: 1. left identity return >=> x = x; 2. right identity x >=> return = x; and 3. associativity (x >=> y) >=> z = x >=> (y >=> z). This also more clearly shows their relationship to the Monoid, Alternative, and Category laws. — Jon Purdy

Daniel Wagner Daniel Wagner · Accepted Answer · 2020-11-23T14:53:33

The bits of the proof you have written are only incorrect in unimportant ways. Specifically, in these two lines:

([Nothing] >>= f ) >>= g = Nothing >>= g = Nothing
[Nothing] >>= (\x -> (f x >>= g)) = Nothing

The three bare Nothings should be [Nothing]s.

However, the proof is incomplete, because there are values of type Test a that are neither of the form [Just (x :: a)] nor [Nothing]. This makes the proof as a whole incorrect in an important way.

proving monad laws of a new monad instance (list of maybe)

1 Answers