io-sim: MonadFix instance using unsafeInterleaveIO

Author: coot

io-sim/src/Control/Monad/IOSim/Internal.hs

@@ -66,12 +66,13 @@ import qualified Data.Set as Set
 import           Data.Time (UTCTime (..), fromGregorian)
 import           Data.Dynamic
 
-import           Control.Exception (assert)
+import           Control.Exception (NonTermination (..),
+                   assert, throw)
 import           Control.Monad (join)
 
 import           Control.Monad (when)
 import           Control.Monad.ST.Lazy
-import           Control.Monad.ST.Lazy.Unsafe (unsafeIOToST)
+import           Control.Monad.ST.Lazy.Unsafe (unsafeIOToST, unsafeInterleaveST)
 import           Data.STRef.Lazy
 
 import           Control.Monad.Class.MonadSTM hiding (STM, TVar)
@@ -527,6 +528,14 @@ schedule thread@Thread{
     -- ExploreRaces is ignored by this simulator
     ExploreRaces k -> schedule thread{ threadControl = ThreadControl k ctl } simstate
 
+    Fix f k -> do
+      r <- newSTRef (throw NonTermination)
+      x <- unsafeInterleaveST $ readSTRef r
+      let k' = unIOSim (f x) $ \x' ->
+                  LiftST (lazyToStrictST (writeSTRef r x')) (\() -> k x')
+          thread' = thread { threadControl = ThreadControl k' ctl }
+      schedule thread' simstate
+
 
 threadInterruptible :: Thread s a -> Bool
 threadInterruptible thread =

io-sim/src/Control/Monad/IOSim/Types.hs

@@ -70,6 +70,7 @@ module Control.Monad.IOSim.Types
 import           Control.Exception (ErrorCall (..), asyncExceptionFromException, asyncExceptionToException)
 import           Control.Applicative
 import           Control.Monad
+import           Control.Monad.Fix (MonadFix (..))
 
 import           Control.Monad.Class.MonadAsync hiding (Async)
 import qualified Control.Monad.Class.MonadAsync as MonadAsync
@@ -163,6 +164,8 @@ data SimA s a where
 
   ExploreRaces :: SimA s b -> SimA s b
 
+  Fix          :: (x -> IOSim s x) -> (x -> SimA s r) -> SimA s r
+
 
 newtype STM s a = STM { unSTM :: forall r. (a -> StmA s r) -> StmA s r }
 
@@ -238,6 +241,9 @@ instance Monoid a => Monoid (IOSim s a) where
 instance Fail.MonadFail (IOSim s) where
   fail msg = IOSim $ \_ -> Throw (toException (IO.Error.userError msg))
 
+instance MonadFix (IOSim s) where  
+    mfix f = IOSim $ \k -> Fix f k 
+
 
 instance Functor (STM s) where
     {-# INLINE fmap #-}

io-sim/src/Control/Monad/IOSimPOR/Internal.hs

@@ -69,12 +69,12 @@ import           Data.Set (Set)
 import qualified Data.Set as Set
 import           Data.Time (UTCTime (..), fromGregorian)
 
-import           Control.Exception (assert)
+import           Control.Exception (NonTermination (..), assert, throw)
 import           Control.Monad (join)
 
 import           Control.Monad (when)
 import           Control.Monad.ST.Lazy
-import           Control.Monad.ST.Lazy.Unsafe (unsafeIOToST)
+import           Control.Monad.ST.Lazy.Unsafe (unsafeIOToST, unsafeInterleaveST)
 import           Data.STRef.Lazy
 
 import           Control.Monad.Class.MonadSTM hiding (STM, TVar)
@@ -608,6 +608,14 @@ schedule thread@Thread{
                             , threadRacy    = True }
       schedule thread' simstate
 
+    Fix f k -> do
+      r <- newSTRef (throw NonTermination)
+      x <- unsafeInterleaveST $ readSTRef r
+      let k' = unIOSim (f x) $ \x' ->
+                  LiftST (lazyToStrictST (writeSTRef r x')) (\() -> k x')
+          thread' = thread { threadControl = ThreadControl k' ctl }
+      schedule thread' simstate
+
     GetMaskState k -> do
       let thread' = thread { threadControl = ThreadControl (k maskst) ctl }
       schedule thread' simstate

io-sim/test/Test/IOSim.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP                 #-}
 {-# LANGUAGE FlexibleContexts    #-}
 {-# LANGUAGE RankNTypes          #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -11,20 +12,25 @@ module Test.IOSim
 import           Data.Array
 import           Data.Either (isLeft)
 import           Data.Fixed (Fixed (..), Micro)
+import           Data.Foldable (foldl')
 import           Data.Function (on)
+import           Data.Functor (($>))
 import           Data.Graph
 import           Data.List (sortBy)
 import           Data.Time.Clock (picosecondsToDiffTime)
 
 import           Control.Exception (ArithException (..))
 import           Control.Monad
+import           Control.Monad.Fix
 import           System.IO.Error (ioeGetErrorString, isUserError)
 
 import           Control.Monad.Class.MonadFork
 import           Control.Monad.Class.MonadSTM.Strict
 import           Control.Monad.Class.MonadSay
+import qualified Control.Monad.Class.MonadSTM as LazySTM
 import           Control.Monad.Class.MonadThrow
 import           Control.Monad.Class.MonadTimer
+import           Control.Monad.Class.MonadTime
 import           Control.Monad.IOSim
 
 import           Test.STM
@@ -131,6 +137,13 @@ tests =
     [ testProperty "Reference vs IO"    prop_stm_referenceIO
     , testProperty "Reference vs Sim"   prop_stm_referenceSim
     ]
+  , testGroup "MonadFix instance"
+    [ testProperty "purity"     prop_mfix_purity
+    , testProperty "purity2"    prop_mfix_purity_2
+    , testProperty "tightening" prop_mfix_left_shrinking
+    , testProperty "lazy"       prop_mfix_lazy
+    , testProperty "recdata"    prop_mfix_recdata
+    ]
   ]
 
 
@@ -401,6 +414,155 @@ test_wakeup_order = do
     return (wakupOrder === [0..9]) --FIFO order
 
 
+--
+-- MonadFix properties
+--
+
+-- | Purity demands that @mfix (return . f) = return (fix f)@.
+--
+prop_mfix_purity :: Positive Int -> Bool
+prop_mfix_purity (Positive n) =
+       runSimOrThrow
+         (mfix (return . factorial)) n
+    == fix factorial n
+  where
+    factorial :: (Int -> Int) -> Int -> Int
+    factorial = \rec_ k -> if k <= 1 then 1 else k * rec_ (k - 1)
+
+
+prop_mfix_purity_2 :: [Positive Int] -> Bool
+prop_mfix_purity_2 as =
+    -- note: both 'IOSim' expressions are equivalent using 'Monad' and
+    -- 'Applicative' laws only.
+      runSimOrThrow (join $  mfix (return . recDelay)
+                         <*> return as')
+      == expected
+    &&
+      runSimOrThrow (mfix (return . recDelay) >>= ($ as'))
+      == expected
+  where
+    as' :: [Int]
+    as' = getPositive `map` as
+
+    -- recursive sum using 'threadDelay'
+    recDelay :: ( MonadMonotonicTime m
+                , MonadDelay m
+                )
+             => ([Int] -> m Time)
+             ->  [Int] -> m Time
+    recDelay = \rec_ bs ->
+                 case bs of
+                  []        -> getMonotonicTime
+                  (b : bs') -> threadDelay (realToFrac b)
+                            >> rec_ bs'
+
+    expected :: Time
+    expected = foldl' (flip addTime)
+                      (Time 0)
+                      (realToFrac `map` as')
+
+
+prop_mfix_left_shrinking
+    :: Int
+    -> NonNegative Int
+    -> Positive Int
+    -> Bool
+prop_mfix_left_shrinking n (NonNegative d) (Positive i) =
+   let mn :: IOSim s Int
+       mn = do say ""
+               threadDelay (realToFrac d)
+               return n
+   in
+        take i
+        (runSimOrThrow $
+          mfix (\rec_ -> mn >>= \a -> do
+                  threadDelay (realToFrac d) $> a : rec_))
+      ==
+        take i
+        (runSimOrThrow $
+          mn >>= \a ->
+            (mfix (\rec_ -> do
+              threadDelay (realToFrac d) $> a : rec_)))
+
+
+
+-- | 'Example 8.2.1' in 'Value Recursion in Monadic Computations'
+-- <https://leventerkok.github.io/papers/erkok-thesis.pdf>
+--
+prop_mfix_lazy :: NonEmptyList Char
+               -> Bool
+prop_mfix_lazy (NonEmpty env) =
+         take samples
+           (runSimOrThrow (withEnv (mfix . replicateHeadM)))
+      == replicate samples (head env)
+    where
+      samples :: Int
+      samples = 10
+
+      replicateHeadM ::
+                        (
+#if MIN_VERSION_base(4,13,0)
+                          MonadFail m,
+                          MonadFail (STM m),
+#endif
+                          MonadSTM  m
+                        )
+                     => m Char
+                     -> [Char] -> m [Char]
+      replicateHeadM getChar_ as = do
+        -- Note: 'getChar' will be executed only once! This follows from 'fixIO`
+        -- semantics.
+        a <- getChar_
+        return (a : as)
+
+      -- construct 'getChar' using the simulated environment
+      withEnv :: (
+#if MIN_VERSION_base(4,13,0)
+                   MonadFail m,
+#endif
+                   MonadSTM  m
+                 )
+              => (m Char -> m a) -> m a
+      withEnv k = do
+        v <- newTVarIO env
+        let getChar_ =
+              atomically $ do
+                as <- readTVar v
+                case as of
+                  [] -> error "withEnv: runtime error"
+                  (a : as') -> writeTVar v as'
+                            $> a
+        k getChar_
+
+
+-- | 'Example 8.2.3' in 'Value Recursion in Monadic Computations'
+-- <https://leventerkok.github.io/papers/erkok-thesis.pdf>
+--
+prop_mfix_recdata :: Property
+prop_mfix_recdata = ioProperty $ do
+    expected <- experiment
+    let res = runSimOrThrow experiment
+    return $
+      take samples res
+      ==
+      take samples expected
+  where
+    samples :: Int
+    samples = 10
+
+    experiment :: ( MonadSTM m
+                  , MonadFix m
+                  )
+               => m [Int]
+    experiment = do
+      (_, y) <-
+        mfix (\ ~(x, _) -> do
+                y <- LazySTM.newTVarIO x
+                return (1:x, y)
+             )
+      atomically (LazySTM.readTVar y)
+
+
 --
 -- Probe mini-abstraction
 --