Near Sermiring and MonadPlus

NSemiring.hs

{-# LANGUAGE Rank2Types, ScopedTypeVariables #-}
import Prelude hiding ((<*>), abs)
import qualified Control.Applicative as A
import Control.Monad
import Test.QuickCheck

class NearSemiring m where
  (<+>) :: m a -> m a -> m a
  zero :: m a
  (<*>) :: m a -> m a -> m a
  one :: m a

newtype S m a = S { unS :: a -> m a }

instance MonadPlus m => NearSemiring (S m) where
  (S ma) <+> (S mb) = S $ \x -> ma x `mplus` mb x
  zero = S $ const mzero
  (S m) <*> (S k) = S $ \x -> m x >>= k
  one = S return

--

newtype Ran f g x = Ran { unRan :: forall y. (x -> f y) -> g y }
newtype Exp f g x = Exp { unExp :: forall y. (x -> y) -> (f y -> g y) }
newtype DC f x = DC { unDC :: Ran (Exp f f) (Exp f f) x }

instance Functor (DC f) where
  fmap = undefined

instance Applicative (DC f) where
  pure = undefined
  (<*>) = undefined

instance A.Alternative (DC f) where
  empty = undefined
  (<|>) = undefined

instance Monad (DC f) where
  return x = DC $ Ran $ \f -> f x
  DC (Ran m) >>= f = DC $ Ran $ \g -> m (\a -> unRan (unDC $ f a) g)

instance MonadPlus (DC f) where
  mzero = DC $ Ran $ \k -> Exp $ \c x -> x
  mplus (DC (Ran a)) (DC (Ran b)) = DC $ Ran $ \sk -> Exp $ \f fk -> unExp (a sk) f $ unExp (b sk) f fk

rep :: Monad m => m a -> DC m a
rep x = DC $ Ran $ \g -> Exp $ \h m -> x >>= \a -> unExp (g a) h m

abs :: MonadPlus m => DC m a -> m a
abs (DC (Ran f)) = unExp (f $ \x -> Exp $ \h m -> return (h x) `mplus` m) id mzero

main = do
  let toS = S . const

  quickCheck $ label "assocPlus" $ \(a :: [Int]) b c n ->
    unS (toS a <+> (toS b <+> toS c)) n === unS ((toS a <+> toS b) <+> toS c) n
  quickCheck $ label "assocMult" $ \(a :: [Int]) b c n ->
    unS (toS a <*> (toS b <*> toS c)) n === unS ((toS a <*> toS b) <*> toS c) n
  quickCheck $ label "zeroLeft" $ \(a :: [Int]) n ->
    unS (zero <+> toS a) n === unS (toS a) n
  quickCheck $ label "zeroRight" $ \(a :: [Int]) n ->
    unS (toS a <+> zero) n === unS (toS a) n
  quickCheck $ label "distribLeft" $ \(a :: [Int]) b c n ->
    unS ((toS a <+> toS b) <*> toS c) n === unS ((toS a <*> toS c) <+> (toS b <*> toS c)) n
  quickCheck $ label "distribRight" $ \(a :: [Int]) b c n ->
    unS (toS a <*> (toS b <+> toS c)) n === unS ((toS a <*> toS b) <+> (toS a <*> toS c)) n

  let toD = toS . rep
  let unD f x = abs $ unS f x
  quickCheck $ label "assocPlus" $ \(a :: [Int]) b c n ->
    unD (toD a <+> (toD b <+> toD c)) n === unD ((toD a <+> toD b) <+> toD c) n
  quickCheck $ label "assocMult" $ \(a :: [Int]) b c n ->
    unD (toD a <*> (toD b <*> toD c)) n === unD ((toD a <*> toD b) <*> toD c) n
  quickCheck $ label "zeroLeft" $ \(a :: [Int]) n ->
    unD (zero <+> toD a) n === unD (toD a) n
  quickCheck $ label "zeroRight" $ \(a :: [Int]) n ->
    unD (toD a <+> zero) n === unD (toD a) n
  quickCheck $ label "distribLeft" $ \(a :: [Int]) b c n ->
    unD ((toD a <+> toD b) <*> toD c) n === unD ((toD a <*> toD c) <+> (toD b <*> toD c)) n
  quickCheck $ label "distribRight" $ \(a :: [Int]) b c n ->
    unD (toD a <*> (toD b <+> toD c)) n === unD ((toD a <*> toD b) <+> (toD a <*> toD c)) n