Is this a valid monad instance?

Question

Here's my type and it's proposed monad instance.

newtype Inf m a = Inf { getInf :: m (a, Inf m a) }

instance (Monad m, Alternative m) => Monad (Inf m) where
    return a = Inf (pure (a, Inf empty))
    m >>= f = Inf $ do
        (st1, inf1) <- getInf m
        go (Left st1) inf1
        where
        go newStateOrInf inf1 = do
            let inf2 = case newStateOrInf of
                    Left st1 -> f st1
                    Right inf2 -> inf2
            res <- Left <$> getInf inf1 <|> Right <$> getInf inf2
            case res of
                Left (st1', inf1') -> go (Left st1') inf1'
                Right (st2, inf2') -> pure (st2, Inf (go (Right inf2') inf1))

I'm wondering if this is a valid monad instance. I sort of proved the first two laws (if you squint), but I'm having issues with associativity, if anyone wants to give it a shot.

The idea of the Inf type is something that can occasionally produce a new a, and a new Inf continuation. Then, using >>=, you can construct a new Inf that depends on the results of the first one. In that case, every time the first Inf produces a new value (the Left result), the second Inf gets regenerated. But when the secon Inf produces a new value, only it is updated, not the first one.

Answer 1

QuickCheck it, and a counterexample for the associativity law quickly appears for Inf [].

• I also tried with Inf Maybe and the few thousands of tests I tried pass.

• The right identity law (u >>= pure) = u also fails for both Inf [] and Inf Maybe.

Counterexample

Pasting the output of QuickCheck with a bit of manual formatting, the law ((u >>= k) >>= h) = (u >>= \x -> k x >>= h) fails with:

u = Inf {getInf = [(0,Inf {getInf = [(0,Inf {getInf = []})]})]}
k = \case
  0 -> Inf {getInf = [(0,Inf {getInf = []})]}
  _ -> Inf {getInf = []}
h = \case
  0 -> Inf {getInf = [(0,Inf {getInf = []})]}
  _ -> Inf {getInf = []}

where the two sides of the equation evaluate to:

(u >>= k) >>= h
=
Inf {getInf = [(0,Inf {getInf = []}),(0,Inf {getInf = []}),(0,Inf {getInf = [(0,Inf {getInf = []})]})]}
/=
Inf {getInf = [(0,Inf {getInf = []}),(0,Inf {getInf = [(0,Inf {getInf = []})]})]}
=
u >>= \x -> k x >>= h

Code

Full implementation below. I only had to add a couple lines of code:

• Functor and Applicative instances, required by Monad
• Eq and Show, for QuickCheck (derivable if you explicitly provide the right context)
• Arbitrary (have to tweak a little to get examples of reasonable size, also had to reduce the size parameter to a very small value (5) because that's roughly going to be the branching factor of the generated Inf [] trees, so they blow up very easily)
• the laws as testable functions (here we simply needed to test with monads with Eq and Show to find counterexamples, this would need to change with fancier monads)

{-# LANGUAGE DeriveFunctor, StandaloneDeriving, FlexibleContexts, ScopedTypeVariables, TypeApplications, GeneralizedNewtypeDeriving, DerivingStrategies, UndecidableInstances #-}

import Control.Monad
import Control.Applicative
import Test.QuickCheck

newtype Inf m a = Inf { getInf :: m (a, Inf m a) }
  deriving Functor

deriving stock instance (Eq a, Eq (Inf m a)) => Eq (m (a, Inf m a))) => Eq (Inf m a)
deriving stock instance (Show a, Show (Inf m a)) => Show (m (a, Inf m a))) => Show (Inf m a)

instance (Monad m, Alternative m) => Applicative (Inf m) where
  (<*>) = ap
  pure = return

instance (Monad m, Alternative m) => Monad (Inf m) where
    return a = Inf (pure (a, Inf empty))
    m >>= f = Inf $ do
        (st1, inf1) <- getInf m
        go (Left st1) inf1
        where
        go newStateOrInf inf1 = do
            let inf2 = case newStateOrInf of
                    Left st1 -> f st1
                    Right inf2 -> inf2
            res <- Left <$> getInf inf1 <|> Right <$> getInf inf2
            case res of
                Left (st1', inf1') -> go (Left st1') inf1'
                Right (st2, inf2') -> pure (st2, Inf (go (Right inf2') inf1))

instance (Arbitrary a, Alternative m, Arbitrary (Inf m a)) => Arbitrary (m (a, Inf m a))) => Arbitrary (Inf m a) where
  arbitrary = Inf <$> oneof
    [ pure empty
    , arbitrary
    ]
  shrink (Inf xs) = Inf <$> shrink xs

assoc :: forall m a b c. (Monad m, Eq (m c), Show (m c)) => m a -> Fun a (m b) -> Fun b (m c) -> Property
assoc u (Fn k) (Fn h) = (u >>= k >>= h) === (u >>= \x -> k x >>= h)

leftId :: forall m a b. (Monad m, Eq (m b), Show (m b)) => a -> Fun a (m b) -> Property
leftId x (Fn k) = (pure x >>= k) === k x

rightId :: forall m a. (Monad m, Eq (m a), Show (m a)) => m a -> Property
rightId u = u === (u >>= pure)

main :: IO ()
main = do
  quickCheckWith stdArgs{maxSuccess=100000} (leftId @(Inf Maybe) @Int @Int)
  quickCheckWith stdArgs{maxSize=5}         (leftId @(Inf []) @Int @Int)
  quickCheckWith stdArgs{maxSuccess=100000} (rightId @(Inf Maybe) @Int)
  quickCheckWith stdArgs{maxSize=5}         (rightId @(Inf []) @Int)
  quickCheckWith stdArgs{maxSuccess=100000} (assoc @(Inf Maybe) @Int @Int @Int)
  quickCheckWith stdArgs{maxSize=5}         (assoc @(Inf []) @Int @Int @Int)