comonad-coactions-0.1.0.1: test/Main.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# OPTIONS_GHC -Wno-unused-top-binds #-}

module Main (main) where

import Control.Comonad
import Control.Comonad.Coaction
import Control.Comonad.Store
import Control.Comonad.Traced (TracedT (..))
import Data.Functor.Compose
import Data.List.NonEmpty qualified as NE
import Data.Monoid (Sum)
import Data.Tree
import Test.QuickCheck
import Test.QuickCheck.Checkers
import Test.Tasty
import Test.Tasty.QuickCheck

leftcomodule ::
  forall w f a.
  ( LeftComodule w f,
    Arbitrary (f a),
    Show (f a),
    EqProp (f a),
    EqProp (w (w (f a)))
  ) =>
  TestBatch
leftcomodule =
  ( "left comodule laws",
    [ ("left coidentity", property leftP),
      ("coassociativity", property coassocP)
    ]
  )
  where
    leftP :: f a -> Property
    coassocP :: f a -> Property

    leftP a = extract (lduplicate @w a) =-= a
    coassocP a = duplicate @w (lduplicate a) =-= fmap lduplicate (lduplicate a)

leftcomodulestore ::
  forall w s a.
  ( Comonad w,
    Arbitrary s,
    Arbitrary (w (Fun s a)),
    Show s,
    EqProp s,
    EqProp (w a),
    Show (w (Fun s a)),
    EqProp (w (w (w a, s))),
    ComonadTransStack w (StoreT s w)
  ) =>
  TestBatch
leftcomodulestore =
  ( "left comodule laws for StoreT",
    [ ("right coidentity", property leftP),
      ("associativity", property coassocP)
    ]
  )
  where
    leftP :: w (Fun s a) -> s -> s -> Property
    coassocP :: w (Fun s a) -> s -> s -> Property

    leftP a s t =
      let x@(StoreT f1 s1) = StoreT (applyFun <$> a) s
          StoreT f2 s2 = extract (lduplicate @w x)
       in (($ t) <$> f1, s1) =-= (($ t) <$> f2, s2)
    coassocP a s t =
      let x = StoreT (applyFun <$> a) s
          w1 = fmap (\(StoreT f u) -> (($ t) <$> f, u)) <$> duplicate @w (lduplicate x)
          w2 = fmap (\(StoreT f u) -> (($ t) <$> f, u)) <$> fmap lduplicate (lduplicate x)
       in w1 =-= w2

leftcomoduletraced ::
  forall w m a.
  ( Comonad w,
    Arbitrary m,
    Arbitrary a,
    Monoid m,
    EqProp (w a),
    Arbitrary (w (Fun m a)),
    Show m,
    Show (w (Fun m a)),
    EqProp (w (w (w a))),
    ComonadTransStack w (TracedT m w)
  ) =>
  TestBatch
leftcomoduletraced =
  ( "left comodule laws for TracedT",
    [ ("right coidentity", property leftP),
      ("associativity", property coassocP)
    ]
  )
  where
    leftP :: w (Fun m a) -> m -> Property
    coassocP :: w (Fun m a) -> m -> Property

    leftP a t =
      let x@(TracedT f1) = TracedT (applyFun <$> a)
          TracedT f2 = extract (lduplicate @w x)
       in (($ t) <$> f1) =-= (($ t) <$> f2)
    coassocP a t =
      let x = TracedT (applyFun <$> a)
          w1 = fmap (\(TracedT f) -> ($ t) <$> f) <$> duplicate @w (lduplicate x)
          w2 = fmap (\(TracedT f) -> ($ t) <$> f) <$> fmap lduplicate (lduplicate x)
       in w1 =-= w2

rightcomodule ::
  forall w f a.
  ( RightComodule w f,
    EqProp (f a),
    EqProp (f (w (w a))),
    Arbitrary (f a),
    Show (f a)
  ) =>
  TestBatch
rightcomodule =
  ( "right comodule laws",
    [ ("right coidentity", property rightP),
      ("coassociativity", property coassocP)
    ]
  )
  where
    rightP :: f a -> Property
    coassocP :: f a -> Property

    rightP a = fmap extract (rduplicate @w a) =-= a
    coassocP a = fmap duplicate (rduplicate @w a) =-= fmap rduplicate (rduplicate a)

rightcomodulestore ::
  forall w s a.
  ( Comonad w,
    Arbitrary s,
    Arbitrary (w (Fun s a)),
    Show s,
    Show (w (Fun s a)),
    EqProp s,
    EqProp (w a),
    EqProp (w (w (w a))),
    ComonadTransStack w (StoreT s w)
  ) =>
  TestBatch
rightcomodulestore =
  ( "right comodule laws for StoreT",
    [ ("right coidentity", property rightP),
      ("associativity", property coassocP)
    ]
  )
  where
    rightP :: w (Fun s a) -> s -> s -> Property
    coassocP :: w (Fun s a) -> s -> s -> Property

    rightP a s t =
      let x@(StoreT f1 s1) = StoreT (applyFun <$> a) s
          StoreT f2 s2 = fmap extract (rduplicate @w x)
       in (($ t) <$> f1, s1) =-= (($ t) <$> f2, s2)
    coassocP a s t =
      let x = StoreT (applyFun <$> a) s
          StoreT f1 s1 = fmap duplicate (rduplicate @w x)
          StoreT f2 s2 = fmap rduplicate (rduplicate x)
       in (($ t) <$> f1, s1) =-= (($ t) <$> f2, s2)

bicomodule ::
  forall s t f a.
  ( BiComodule s t f,
    Arbitrary a,
    EqProp (s (f (t a))),
    Arbitrary (f a),
    Show (f a)
  ) =>
  TestBatch
bicomodule =
  ( "bicomodule laws",
    [ ("coassociativity 1", property assoc1P),
      ("coassociativity 2", property assoc2P)
    ]
  )
  where
    assoc1P :: f a -> Property
    assoc2P :: f a -> Property

    assoc1P a = biduplicate @s @t a =-= lduplicate (rduplicate a)
    assoc2P a = biduplicate @s @t a =-= fmap rduplicate (lduplicate a)

instance (EqProp a) => EqProp (Tree a)

main :: IO ()
main =
  defaultMain
    ( testGroup "monad action laws"
        $ uncurry testProperties
          <$> [ leftcomodule @NE.NonEmpty @(Compose NE.NonEmpty Maybe) @Int,
                rightcomodule @NE.NonEmpty @(Compose Maybe NE.NonEmpty) @Int,
                rightcomodulestore @NE.NonEmpty @Bool @Int,
                rightcomodulestore @Tree @Char @Int,
                leftcomodulestore @Tree @Char @Char,
                leftcomoduletraced @Tree @(Sum Int) @Char
              ]
    )