diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2016, The University of Kansas + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of the University of Kansas nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/remote-monad.cabal b/remote-monad.cabal new file mode 100644 --- /dev/null +++ b/remote-monad.cabal @@ -0,0 +1,91 @@ +-- Initial remote-monad.cabal generated by cabal init. For further +-- documentation, see http://haskell.org/cabal/users-guide/ + +name: remote-monad +version: 0.1.0.0 +synopsis: An parametrizable Remote Monad, and parametrizable Applicative Functor +description: + An implementation of the concepts behind Remote Monads. There is support for various bundling strategies. + . + @ + {-# LANGUAGE GADTs #-} + {-# LANGUAGE KindSignatures #-} + . + module Main where + . + import Control.Remote.Monad + import Control.Remote.Monad.Packet.Weak + . + data Command :: * where + Say :: String -> Command + . + data Procedure :: * -> * where + Temperature :: Procedure Int + . + say :: String -> RemoteMonad Command Procedure () + say s = command (Say s) + . + temperature :: RemoteMonad Command Procedure Int + temperature = procedure Temperature + . + runWP :: WeakPacket Command Procedure a -> IO a + runWP (Command (Say s)) = print s + runWP (Procedure Temperature) = return 42 + . + send :: RemoteMonad Command Procedure a -> IO a + send m = runMonad runWP m + . + main = send $ do + say "Howdy doodly do" + say "How about a muffin?" + t <- temperature + say (show t ++ "F") + @ + + +license: BSD3 +license-file: LICENSE +author: Andy Gill, Justin Dawson +maintainer: andygill@ku.edu +copyright: (c) 2016 The University of Kansas +category: Control +build-type: Simple +tested-with: GHC == 7.10.3 +cabal-version: >=1.10 + +source-repository head + type: git + location: git://github.com/ku-fpg/remote-monad + +library + exposed-modules: + Control.Remote.Monad.Packet.Applicative + Control.Remote.Monad.Packet.Strong + Control.Remote.Monad.Packet.Weak + Control.Remote.Monad.Packet.Transport + Control.Remote.Applicative + Control.Remote.Monad + other-modules: + Control.Remote.Monad.Types + other-extensions: GADTs, RankNTypes, ScopedTypeVariables + build-depends: base >=4.7 && < 5 + , natural-transformation >= 0.3 && < 0.4 + , transformers >= 0.4 && < 0.6 + hs-source-dirs: src + default-language: Haskell2010 + + +test-suite remote-monad-properties + type: exitcode-stdio-1.0 + main-is: Test.hs + build-depends: base >= 4.7 && < 5 + , containers >= 0.1 && < 0.6 + , remote-monad == 0.1.0.0 + , QuickCheck == 2.8.* + , quickcheck-instances >= 0.1 && < 0.4 + , tasty >= 0.8 && < 0.12 + , tasty-quickcheck >= 0.8 && < 0.9 + hs-source-dirs: tests + default-language: Haskell2010 + ghc-options: -Wall + diff --git a/src/Control/Remote/Applicative.hs b/src/Control/Remote/Applicative.hs new file mode 100644 --- /dev/null +++ b/src/Control/Remote/Applicative.hs @@ -0,0 +1,91 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} + +{-| +Module: Control.Remote.Applicative +Copyright: (C) 2016, The University of Kansas +License: BSD-style (see the file LICENSE) +Maintainer: Andy Gill +Stability: Alpha +Portability: GHC +-} + +module Control.Remote.Applicative + ( -- * The remote applicative + RemoteApplicative + -- * The primitive lift functions + , command + , procedure + -- * The run functions + , runApplicative + , runWeakApplicative + , runStrongApplicative + , runApplicativeApplicative + ) where + + +import Control.Monad.Trans.Class +import Control.Monad.Trans.State.Strict + +import Control.Remote.Monad.Packet.Applicative as A +import qualified Control.Remote.Monad.Packet.Strong as Strong +import Control.Remote.Monad.Packet.Strong (StrongPacket, HStrongPacket(..)) +import qualified Control.Remote.Monad.Packet.Weak as Weak +import Control.Remote.Monad.Packet.Weak (WeakPacket) +import Control.Remote.Monad.Types +import Control.Natural + +-- | promote a command into the applicative +command :: c -> RemoteApplicative c p () +command c = RemoteApplicative (Command (pure ()) c) + +-- | promote a command into the applicative +procedure :: p a -> RemoteApplicative c p a +procedure p = RemoteApplicative (Procedure (pure id) p) + +class RunApplicative f where + -- | This overloaded function chooses the best bundling strategy + -- based on the type of the handler your provide. + runApplicative :: (Monad m) => (f c p ~> m) -> (RemoteApplicative c p ~> m) + +instance RunApplicative WeakPacket where + runApplicative = runWeakApplicative + +instance RunApplicative StrongPacket where + runApplicative = runStrongApplicative + +instance RunApplicative ApplicativePacket where + runApplicative = runApplicativeApplicative + +-- | The weak remote applicative, that sends commands and procedures piecemeal. +runWeakApplicative :: forall m c p . (Applicative m) => (WeakPacket c p ~> m) -> (RemoteApplicative c p ~> m) +runWeakApplicative f (RemoteApplicative (Command g c)) = runWeakApplicative f (RemoteApplicative g) <* f (Weak.Command c) +runWeakApplicative f (RemoteApplicative (Procedure g p)) = runWeakApplicative f (RemoteApplicative g) <*> f (Weak.Procedure p) +runWeakApplicative f (RemoteApplicative (Pure a)) = pure a + +-- | The strong remote applicative, that bundles together commands. +runStrongApplicative :: forall m c p . (Monad m) => (StrongPacket c p ~> m) -> (RemoteApplicative c p ~> m) +runStrongApplicative f (RemoteApplicative p) = do + (r,HStrongPacket h) <- runStateT (go p) (HStrongPacket id) + f $ h $ Strong.Done + return r + where + go :: forall a . ApplicativePacket c p a -> StateT (HStrongPacket c p) m a + go (Pure a) = return a + go (Command g c) = do + r <- go g + modify (\ (HStrongPacket cs) -> HStrongPacket (cs . Strong.Command c)) + return r + go (Procedure g p) = do + r1 <- go g + HStrongPacket cs <- get + put (HStrongPacket id) + r2 <- lift $ f $ cs $ Strong.Procedure $ p + return $ r1 r2 + +-- | The applicative remote applicative, that is the identity function. +runApplicativeApplicative :: (ApplicativePacket c p ~> m) -> (RemoteApplicative c p ~> m) +runApplicativeApplicative f (RemoteApplicative m) = f m diff --git a/src/Control/Remote/Monad.hs b/src/Control/Remote/Monad.hs new file mode 100644 --- /dev/null +++ b/src/Control/Remote/Monad.hs @@ -0,0 +1,132 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} + +{-| +Module: Control.Remote.Monad.Packet.Weak +Copyright: (C) 2016, The University of Kansas +License: BSD-style (see the file LICENSE) +Maintainer: Andy Gill +Stability: Alpha +Portability: GHC +-} + +module Control.Remote.Monad + ( -- * The remote monad + RemoteMonad + -- * The primitive lift functions + , command + , procedure + -- * The run functions + , runMonad + , runWeakMonad + , runStrongMonad + , runApplicativeMonad + , runMonadSkeleton + ) where + +import Control.Monad.Trans.Class +import Control.Monad.Trans.State.Strict + +import qualified Control.Remote.Applicative as A +import Control.Remote.Monad.Packet.Applicative as A +import Control.Remote.Monad.Packet.Weak as Weak +import Control.Remote.Monad.Packet.Strong as Strong +import Control.Remote.Monad.Types + +import Control.Natural + + +-- | promote a command into the remote monad +command :: c -> RemoteMonad c p () +command = Appl . A.command + +-- | promote a procedure into the remote monad +procedure :: p a -> RemoteMonad c p a +procedure = Appl . A.procedure + +class RunMonad f where + -- | This overloaded function chooses the best bundling strategy + -- based on the type of the handler your provide. + runMonad :: (Monad m) => (f c p ~> m) -> (RemoteMonad c p ~> m) + +instance RunMonad WeakPacket where + runMonad = runWeakMonad + +instance RunMonad StrongPacket where + runMonad = runStrongMonad + +instance RunMonad ApplicativePacket where + runMonad = runApplicativeMonad + +-- | This is a remote monad combinator, that takes an implementation +-- of a remote applicative, splits the monad into applicatives +-- without any merge stragegy, and uses the remote applicative. +-- Every '>>=' will generate a call to the 'RemoteApplicative' +-- handler; as well as one terminating call. +-- Using 'runBindeeMonad' with a 'runWeakApplicative' gives the weakest remote monad. +runMonadSkeleton :: (Monad m) => (RemoteApplicative c p ~> m) -> (RemoteMonad c p ~> m) +runMonadSkeleton f (Appl g) = f g +runMonadSkeleton f (Bind g k) = f g >>= runMonadSkeleton f . k + +-- | This is the classic weak remote monad, or technically the +-- weak remote applicative weak remote monad. +runWeakMonad :: (Monad m) => (WeakPacket c p ~> m) -> (RemoteMonad c p ~> m) +runWeakMonad f = runMonadSkeleton (A.runWeakApplicative f) + +-- | This is the classic strong remote monad. It bundles +-- packets (of type 'StrongPacket') as large as possible, +-- including over some monadic binds. +runStrongMonad :: forall m c p . (Monad m) => (StrongPacket c p ~> m) -> (RemoteMonad c p ~> m) +runStrongMonad f p = do + (r,HStrongPacket h) <- runStateT (go2 p) (HStrongPacket id) + f $ h $ Strong.Done + return r + where + go2 :: forall a . RemoteMonad c p a -> StateT (HStrongPacket c p) m a + go2 (Appl app) = go' app + go2 (Bind app k) = go' app >>= \ a -> go2 (k a) + + go' :: forall a . RemoteApplicative c p a -> StateT (HStrongPacket c p) m a + go' (RemoteApplicative m) = go m + + go :: forall a . ApplicativePacket c p a -> StateT (HStrongPacket c p) m a + go (A.Pure a) = return a + go (A.Command g c) = do + r <- go g + modify (\ (HStrongPacket cs) -> HStrongPacket (cs . Strong.Command c)) + return r + go (A.Procedure g p) = do + r1 <- go g + HStrongPacket cs <- get + put (HStrongPacket id) + r2 <- lift $ f $ cs $ Strong.Procedure $ p + return $ r1 r2 + +-- | The is the strong applicative strong remote monad. It bundles +-- packets (of type 'RemoteApplicative') as large as possible, +-- including over some monadic binds. +runApplicativeMonad :: forall m c p . (Monad m) => (A.ApplicativePacket c p ~> m) -> (RemoteMonad c p ~> m) +runApplicativeMonad f p = do + (r,h) <- runStateT (go2 p) (pure ()) + f $ h + return r + where + go2 :: forall a . RemoteMonad c p a -> StateT (A.ApplicativePacket c p ()) m a + go2 (Appl app) = go' app + go2 (Bind app k) = go' app >>= \ a -> go2 (k a) + + go' :: forall a . RemoteApplicative c p a -> StateT (A.ApplicativePacket c p ()) m a + go' (RemoteApplicative m) = go m + + go :: forall a . ApplicativePacket c p a -> StateT (A.ApplicativePacket c p ()) m a + go ap = case A.superCommand ap of + Nothing -> do + ap' <- get + put (pure ()) + lift $ f $ (ap' *> ap) + Just a -> do + modify (\ ap' -> ap' <* ap) + return a + diff --git a/src/Control/Remote/Monad/Packet/Applicative.hs b/src/Control/Remote/Monad/Packet/Applicative.hs new file mode 100644 --- /dev/null +++ b/src/Control/Remote/Monad/Packet/Applicative.hs @@ -0,0 +1,58 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} + +{-| +Module: Control.Remote.Monad.Packet.Applicative +Copyright: (C) 2016, The University of Kansas +License: BSD-style (see the file LICENSE) +Maintainer: Andy Gill +Stability: Alpha +Portability: GHC +-} + +module Control.Remote.Monad.Packet.Applicative + ( -- * The remote applicative + ApplicativePacket(..) + -- * Utility + , superCommand + ) where + + +import Control.Monad.Trans.Class +import Control.Monad.Trans.State.Strict + +import qualified Control.Remote.Monad.Packet.Strong as Strong +import Control.Natural + +-- | A Remote Applicative, that can encode both commands and procedures, bundled together. + +data ApplicativePacket (c :: *) (p :: * -> *) (a :: *) where + Command :: ApplicativePacket c p b -> c -> ApplicativePacket c p b + Procedure :: ApplicativePacket c p (a -> b) -> p a -> ApplicativePacket c p b + Pure :: a -> ApplicativePacket c p a + +instance Functor (ApplicativePacket c p) where + fmap f (Command g c) = Command (fmap f g) c + fmap f (Procedure g p) = Procedure (fmap (f .) g) p + fmap f (Pure a) = Pure (f a) + +instance Applicative (ApplicativePacket c p) where + pure a = Pure a + (Pure f) <*> m = fmap f m + (Command g c) <*> (Pure a) = Command (fmap (\ f -> f a) g) c + (Procedure g p) <*> (Pure a) = Procedure (fmap (\ f a1 -> f a1 a) g) p + m <*> (Command g2 c2) = Command (m <*> g2) c2 + m <*> (Procedure g2 p2) = Procedure (fmap (.) m <*> g2) p2 + + +-- | This simulates a 'ApplicativePacket', to see if it only contains commands, and if so, +-- returns the static result. The commands still need executed. The term super-command +-- is a play on Hughes' super-combinator terminology. + +superCommand :: ApplicativePacket c p a -> Maybe a +superCommand (Pure a) = Just a +superCommand (Command g _) = superCommand g +superCommand (Procedure _ _) = Nothing diff --git a/src/Control/Remote/Monad/Packet/Strong.hs b/src/Control/Remote/Monad/Packet/Strong.hs new file mode 100644 --- /dev/null +++ b/src/Control/Remote/Monad/Packet/Strong.hs @@ -0,0 +1,37 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeOperators #-} + +{-| +Module: Control.Remote.Monad.Packet.Strong +Copyright: (C) 2016, The University of Kansas +License: BSD-style (see the file LICENSE) +Maintainer: Andy Gill +Stability: Alpha +Portability: GHC +-} + +module Control.Remote.Monad.Packet.Strong where + +import qualified Control.Remote.Monad.Packet.Weak as Weak +import Control.Remote.Monad.Packet.Weak (WeakPacket) +import Control.Natural + + +-- | A Strong Packet, that can encode a list of commands, terminated by an optional procedure. + +data StrongPacket (c :: *) (p :: * -> *) (a :: *) where + Command :: c -> StrongPacket c p b -> StrongPacket c p b + Procedure :: p a -> StrongPacket c p a + Done :: StrongPacket c p () + +-- | promote a Weak packet transporter, into a Strong packet transporter. +runStrongPacket :: (Applicative m) => (WeakPacket c p ~> m) -> (StrongPacket c p ~> m) +runStrongPacket f (Command c pk) = f (Weak.Command c) *> runStrongPacket f pk +runStrongPacket f (Procedure p) = f (Weak.Procedure p) +runStrongPacket f Done = pure () + +-- | A Hughes-style version of 'StrongPacket', with efficent append. +newtype HStrongPacket c p = HStrongPacket (StrongPacket c p ~> StrongPacket c p) + diff --git a/src/Control/Remote/Monad/Packet/Transport.hs b/src/Control/Remote/Monad/Packet/Transport.hs new file mode 100644 --- /dev/null +++ b/src/Control/Remote/Monad/Packet/Transport.hs @@ -0,0 +1,22 @@ +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE StandaloneDeriving #-} + +{-| +Module: Control.Remote.Monad.Packet.Transport +Copyright: (C) 2016, The University of Kansas +License: BSD-style (see the file LICENSE) +Maintainer: Andy Gill +Stability: Alpha +Portability: GHC +-} + +module Control.Remote.Monad.Packet.Transport where + +-- | 'Transport' of a container for procedures, and other structures that are refreshed. + +data Transport (p :: * -> *) + = forall a . (Show a) => Transport (p a) + diff --git a/src/Control/Remote/Monad/Packet/Weak.hs b/src/Control/Remote/Monad/Packet/Weak.hs new file mode 100644 --- /dev/null +++ b/src/Control/Remote/Monad/Packet/Weak.hs @@ -0,0 +1,37 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE StandaloneDeriving #-} + +{-| +Module: Control.Remote.Monad.Packet.Weak +Copyright: (C) 2016, The University of Kansas +License: BSD-style (see the file LICENSE) +Maintainer: Andy Gill +Stability: Alpha +Portability: GHC +-} + +module Control.Remote.Monad.Packet.Weak where + +import Control.Remote.Monad.Packet.Transport + +-- | A Weak Packet, that can encode a command or a procedure. + +data WeakPacket (c :: *) (p :: * -> *) (a :: *) where + Command :: c -> WeakPacket c p () + Procedure :: p a -> WeakPacket c p a + +deriving instance (Show c, Show (p a)) => Show (WeakPacket c p a) + +instance (Read c, Read (Transport p)) => Read (Transport (WeakPacket c p)) where + readsPrec d = readParen (d > 10) $ \ r0 -> + [ (Transport $ Command c,r2) + | ("Command",r1) <- lex r0 + , (c,r2) <- readsPrec 11 r1 + ] ++ + [ (Transport $ Procedure p,r2) + | ("Procedure",r1) <- lex r0 + , (Transport p,r2) <- readsPrec 11 r1 + ] diff --git a/src/Control/Remote/Monad/Types.hs b/src/Control/Remote/Monad/Types.hs new file mode 100644 --- /dev/null +++ b/src/Control/Remote/Monad/Types.hs @@ -0,0 +1,52 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} + +{-| +Module: Control.Remote.Applicative +Copyright: (C) 2016, The University of Kansas +License: BSD-style (see the file LICENSE) +Maintainer: Andy Gill +Stability: Alpha +Portability: GHC +-} + +module Control.Remote.Monad.Types + ( RemoteMonad(..) + , RemoteApplicative(..) + ) where + + +import Control.Remote.Monad.Packet.Applicative +import Control.Natural + +data RemoteMonad c p a where + Appl :: RemoteApplicative c p a -> RemoteMonad c p a + Bind :: RemoteApplicative c p a -> (a -> RemoteMonad c p b) -> RemoteMonad c p b + +instance Functor (RemoteMonad c p) where + fmap f m = pure f <*> m + +instance Applicative (RemoteMonad c p) where + pure a = Appl (pure a) + Appl f <*> Appl g = Appl (f <*> g) + Appl f <*> Bind m k = Bind (pure (,) <*> f <*> m) (\ (a,b) -> fmap a $ k b) + Bind m k <*> r = Bind m (\ a -> k a <*> r) + +instance Monad (RemoteMonad c p) where + return = pure + Appl m >>= k = Bind m k + Bind m k >>= k2 = Bind m (\ a -> k a >>= k2) + + m1 >> m2 = m1 *> m2 -- This improves our bundling opportunities + +newtype RemoteApplicative c p a = RemoteApplicative (ApplicativePacket c p a) + +instance Functor (RemoteApplicative c p) where + fmap f (RemoteApplicative g) = RemoteApplicative (fmap f g) + +instance Applicative (RemoteApplicative c p) where + pure a = RemoteApplicative (pure a) + (RemoteApplicative f) <*> (RemoteApplicative g) = RemoteApplicative (f <*> g) diff --git a/tests/Test.hs b/tests/Test.hs new file mode 100644 --- /dev/null +++ b/tests/Test.hs @@ -0,0 +1,304 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} + + +{-| +Module: Main +Copyright: (C) 2015 The University of Kansas +License: BSD-style (see the file LICENSE) +Maintainer: Andy Gill +Stability: Experimental + +@QuickCheck@ properties for natural transformations. +-} +module Main (main) where + +import Data.Foldable (toList) +import Data.Sequence (Seq, fromList) + +import qualified Control.Remote.Monad as M +import Control.Remote.Monad.Packet.Applicative as AP +import qualified Control.Remote.Monad.Packet.Weak as WP +import qualified Control.Remote.Monad.Packet.Strong as SP +import qualified Control.Remote.Applicative as A + + +import Test.QuickCheck +import Test.QuickCheck.Instances () +import Test.Tasty (TestTree, defaultMain, testGroup) +import Test.Tasty.QuickCheck (testProperty) +import Test.QuickCheck.Poly (A) +import Test.QuickCheck.Monadic +import Test.QuickCheck.Gen.Unsafe (promote) + +import Data.IORef + +main :: IO () +main = defaultMain testProperties + +testProperties :: TestTree +testProperties = testGroup "QuickCheck remote monad properties" + [ testProperty "push works remotely" $ prop_push + , testProperty "pop works remotely" $ prop_pop + , testProperty "compare two remote monad strategies" $ testRunRemoteMonad + , testProperty "send (m >>= k) = send m >>= send . k" $ testRemoteMonadBindLaw + , testProperty "send (return a) = return a" $ testRemoteMonadReturnLaw + ] + + +---------------------------------------------------------------- +-- Basic stack machine, with its interpreter + +data C :: * where + Push :: A -> C + +data P :: * -> * where + Pop :: P (Maybe A) + +-- Basic evaluator + +runWP :: IORef [String] -> IORef [A] -> WP.WeakPacket C P a -> IO a +runWP tr ref (WP.Command (Push a)) = do + stack <- readIORef ref + writeIORef ref (a : stack) + modifyIORef tr (("push " ++ show a) :) + return () +runWP tr ref (WP.Procedure (Pop)) = do + modifyIORef tr (("pop") :) + stack <- readIORef ref + case stack of + [] -> return Nothing + (x:xs) -> do + writeIORef ref xs + modifyIORef tr ((show x) :) + return (Just x) + + +runSP :: IORef [String] -> IORef [A] -> SP.StrongPacket C P a -> IO a +runSP tr ref (SP.Command c pk) = runWP tr ref (WP.Command c) >> runSP tr ref pk +runSP tr ref (SP.Procedure p) = runWP tr ref (WP.Procedure p) +runSP tr ref SP.Done = pure () + +runAppP :: IORef [String] -> IORef [A] -> ApplicativePacket C P a -> IO a +runAppP tr ref (AP.Command g c) = runAppP tr ref g <* runWP tr ref (WP.Command c) +runAppP tr ref (AP.Procedure g p) = runAppP tr ref g <*> runWP tr ref (WP.Procedure p) +runAppP tr ref (AP.Pure a) = pure a + +---------------------------------------------------------------- +-- The different ways of running remote monads. + +data RemoteMonad = RemoteMonad String (forall a . IORef [String] -> IORef [A] -> M.RemoteMonad C P a -> IO a) + +instance Show RemoteMonad where + show (RemoteMonad msg _) = "Remote Monad: " ++ msg + +instance Arbitrary RemoteMonad where + arbitrary = elements + [ runWeakMonadWeakPacket + , runStrongMonadWeakPacket + , runStrongMonadStrongPacket +-- , runApplicativeMonadWeakPacket +-- , runApplicativeMonadStrongPacket + , runApplicativeMonadApplicativePacket + ] + +--- This is a complete enumeration of ways of building remote monads + +runWeakMonadWeakPacket :: RemoteMonad +runWeakMonadWeakPacket = RemoteMonad "WeakMonadWeakPacket" + $ \ tr ref -> M.runWeakMonad (runWP tr ref) + +runStrongMonadWeakPacket :: RemoteMonad +runStrongMonadWeakPacket = RemoteMonad "StrongMonadWeakPacket" + $ \ tr ref -> M.runStrongMonad (SP.runStrongPacket (runWP tr ref)) + +runStrongMonadStrongPacket :: RemoteMonad +runStrongMonadStrongPacket = RemoteMonad "StrongMonadStrongPacket" + $ \ tr ref -> M.runStrongMonad (runSP tr ref) +{- +runApplicativeMonadWeakPacket :: RemoteMonad +runApplicativeMonadWeakPacket = RemoteMonad "ApplicativeMonadWeakPacket" + $ \ tr ref -> M.runApplicativeMonad (A.runApplicative (runWP tr ref)) + +runApplicativeMonadStrongPacket :: RemoteMonad +runApplicativeMonadStrongPacket = RemoteMonad "ApplicativeMonadStrongPacket" + $ \ tr ref -> M.runApplicativeMonad (A.runApplicative (runSP tr ref)) +-} +runApplicativeMonadApplicativePacket :: RemoteMonad +runApplicativeMonadApplicativePacket = RemoteMonad "ApplicativeMonadApplicativePacket" + $ \ tr ref -> M.runApplicativeMonad (runAppP tr ref) + + +---------------------------------------------------------------- + +data DeviceM = Device (IORef [String]) (IORef [A]) (forall a . M.RemoteMonad C P a -> IO a) + +sendM :: DeviceM -> M.RemoteMonad C P a -> IO a +sendM (Device _ _ f) = f + +newDevice :: [A] + -> RemoteMonad + -> IO DeviceM +newDevice xs (RemoteMonad _ f) = do + tr <- newIORef [] + ref <- newIORef xs + return $ Device tr ref $ f tr ref + +readDevice :: DeviceM -> IO [A] +readDevice (Device _ ref _) = readIORef ref + +cmpDevices :: DeviceM -> DeviceM -> IO Bool +cmpDevices d1 d2 = (==) <$> readDevice d1 <*> readDevice d2 + +-- returns backwards, but is for cmp or debugging anyway +traceDevice :: DeviceM -> IO [String] +traceDevice (Device tr _ _) = readIORef tr + +---------------------------------------------------------------- + +newtype Remote a = Remote (M.RemoteMonad C P a) + +instance Show (Remote a) where + show _ = "" + +instance Arbitrary (Remote A) where + arbitrary = sized $ \ n -> Remote <$> arbitraryRemoteMonadA n + +---------------------------------------------------------------- + +data RemoteBind :: * -> * where + RemoteBind :: Arbitrary a => M.RemoteMonad C P a -> (a -> M.RemoteMonad C P b) -> RemoteBind b + +instance Show (RemoteBind a) where + show _ = "" + +---------------------------------------------------------------- + +arbitraryRemoteMonad' :: (CoArbitrary a, Arbitrary a) => [Gen (M.RemoteMonad C P a)] -> Int -> Gen (M.RemoteMonad C P a) +arbitraryRemoteMonad' base 0 = oneof base +arbitraryRemoteMonad' base n = frequency + [ (1 , oneof base) + , (1 , do RemoteBind m k <- arbitraryBind (arbitraryRemoteMonad' base) n + return (m >>= k) + ) + , (1 , do m1 <- arbitraryRemoteMonadA (n `div` 2) + m2 <- arbitraryRemoteMonad' base (n `div` 2) + return (m1 >> m2) + ) + , (1 , do m1 <- arbitraryRemoteMonadA (n `div` 2) + m2 <- arbitraryRemoteMonad' base (n `div` 2) + f <- arbitrary + return (fmap f m1 <*> m2) + ) + , (1 , do m1 <- arbitraryRemoteMonadA (n `div` 2) + m2 <- arbitraryRemoteMonad' base (n `div` 2) + return (m1 *> m2) + ) + , (1 , do m1 <- arbitraryRemoteMonadA (n `div` 2) + m2 <- arbitraryRemoteMonad' base (n `div` 2) + return (m2 <* m1) -- reversed, because we want to return m2's result + ) + ] + +arbitraryRemoteMonadUnit :: Int -> Gen (M.RemoteMonad C P ()) +arbitraryRemoteMonadUnit = arbitraryRemoteMonad' + [ return (return ()) + , M.command . Push <$> arbitrary + ] + +arbitraryRemoteMonadMaybeA :: Int -> Gen (M.RemoteMonad C P (Maybe A)) +arbitraryRemoteMonadMaybeA = arbitraryRemoteMonad' + [ return <$> arbitrary + , return $ M.procedure Pop + ] + +arbitraryRemoteMonadA :: Int -> Gen (M.RemoteMonad C P A) +arbitraryRemoteMonadA = arbitraryRemoteMonad' + [ return <$> arbitrary + ] + +arbitraryBind :: (Int -> Gen (M.RemoteMonad C P a)) -> Int -> Gen (RemoteBind a) +arbitraryBind f n = oneof + [ do m <- arbitraryRemoteMonadUnit (n `div` 2) + k <- promote (`coarbitrary` f (n `div` 2)) -- look for a better way of doing this + return $ RemoteBind m k + , do m <- arbitraryRemoteMonadMaybeA (n `div` 2) + k <- promote (`coarbitrary` f (n `div` 2)) + return $ RemoteBind m k + , do m <- arbitraryRemoteMonadA (n `div` 2) + k <- promote (`coarbitrary` f (n `div` 2)) + return $ RemoteBind m k + ] + +-------------------------------------------------------------------------- + +-- Test the remote push primitive +prop_push :: RemoteMonad -> [A] -> A -> Property +prop_push runMe xs x = monadicIO $ do + dev <- run $ newDevice xs runMe + () <- run $ sendM dev (M.command (Push x)) + ys <- run $ readDevice dev + assert (ys == (x : xs)) + +-- Test the remote pop primitive +prop_pop :: RemoteMonad -> [A] -> Property +prop_pop runMe xs = monadicIO $ do + dev <- run $ newDevice xs runMe + r <- run $ sendM dev (M.procedure Pop) + ys <- run $ readDevice dev + case xs of + [] -> assert (r == Nothing && ys == []) + (x':xs') -> assert (r == Just x' && ys == xs') + +-- Check that two remote monad configurations given the same trace and same result +testRunRemoteMonad :: RemoteMonad -> RemoteMonad -> Remote A -> [A] -> Property +testRunRemoteMonad runMe1 runMe2 (Remote m) xs = monadicIO $ do + dev1 <- run $ newDevice xs runMe1 + r1 <- run $ sendM dev1 m + tr1 <- run $ traceDevice dev1 + st1 <- run $ readDevice dev1 + + dev2 <- run $ newDevice xs runMe2 + r2 <- run $ sendM dev2 m + tr2 <- run $ traceDevice dev2 + st2 <- run $ readDevice dev2 + +-- monitor $ collect $ (tr1,tr2) + assert (r1 == r2 && tr1 == tr2 && st1 == st2) + +-- Check remote monad laws +testRemoteMonadBindLaw :: RemoteMonad -> [A] -> Property +testRemoteMonadBindLaw runMe xs = monadicIO $ do + RemoteBind m k <- pick (sized $ arbitraryBind arbitraryRemoteMonadA) + + dev1 <- run $ newDevice xs runMe + a <- run $ sendM dev1 m + r1 <- run $ sendM dev1 (k a) + tr1 <- run $ traceDevice dev1 + st1 <- run $ readDevice dev1 + + dev2 <- run $ newDevice xs runMe + r2 <- run $ sendM dev2 (m >>= k) + tr2 <- run $ traceDevice dev2 + st2 <- run $ readDevice dev2 + +-- monitor $ collect $ (runMe, tr1) + assert (r1 == r2 && tr1 == tr2 && st1 == st2) + +-- Check remote monad laws +testRemoteMonadReturnLaw :: RemoteMonad -> [A] -> A -> Property +testRemoteMonadReturnLaw runMe xs x = monadicIO $ do + + dev1 <- run $ newDevice xs runMe + x' <- run $ sendM dev1 (return x) + tr1 <- run $ traceDevice dev1 + st1 <- run $ readDevice dev1 + +-- monitor $ collect $ (runMe, tr1) + assert (x == x' && tr1 == [] && st1 == xs) +