monadLogic

[isovector]

I wrote the MonadLogic laws up, posting them here for posterity. Happy to open a PR if desired.

monadLogic
    :: forall m a b
     . ( CoArbitrary a
       , Arbitrary (m b)
       , Arbitrary a
       , Arbitrary (m a)
       , MonadPlus m
       , MonadLogic m
       , EqProp (m b)
       , EqProp (m (Maybe (a, m a)))
       , Show a
       , Show (m a)
       , Show (m b)
       , Function a
       )
    => m (a, b)
    -> TestBatch
monadLogic _ =
  ( "MonadLogic laws"
  , [ ("msplit mzero", msplit @m @a mzero =-= return Nothing)
    , ("msplit mplus", property $ do
        a <- arbitrary
        m <- arbitrary
        pure $
          counterexample (show a) $
          counterexample (show m) $
            msplit @m @a (return a `mplus` m) =-= return (Just (a, m))
      )
    , ("ifte return", property $ do
        a <- arbitrary
        thf <- arbitrary
        let th = applyFun thf
        el <- arbitrary
        pure $
          counterexample (show a) $
          counterexample (show thf) $
          counterexample (show el) $
            ifte @m @a @b (return a) th el =-= th a
      )
    , ("ifte mzero", property $ do
        thf <- arbitrary
        let th = applyFun thf
        el <- arbitrary @(m b)
        pure $
          counterexample (show thf) $
          counterexample (show el) $
            ifte @m @a @b mzero th el =-= el
      )
    , ("ifte mplus", property $ do
        a <- arbitrary
        m <- arbitrary
        thf <- arbitrary
        let th = applyFun thf
        el <- arbitrary @(m b)
        pure $
          counterexample (show a) $
          counterexample (show m) $
          counterexample (show thf) $
          counterexample (show el) $
            ifte @m @a @b (return a `mplus` m) th el
              =-= th a `mplus` (m >>= th)
      )
    ]
  )

[sjakobi]

I have no qualms about adding logict as a dependency, so a PR would very likely be accepted.

[isovector]

We stopped needing monadlogic in our project, so there is less impetus for me to get this merged.