Merge pull request #83 from input-output-hk/jdral/infinite-stream

Make `Stream`s definitely finite or definitely infinite

Author: jorisdral

fs-sim/CHANGELOG.md

@@ -8,6 +8,26 @@
   exception is thrown during execution of the function. Though we fixed the bug,
   it is also a breaking change: the type signature now has an additional
   constraint.
+* Change finiteness guarantees for `Stream`s. Where streams could previously be
+  *definitely* finite or *possibly* infinite, they should now be *definitely*
+  finite or *definitely* infinite. This is mostly a conceptual change: it was
+  already guaranteed by most if not all of the `Stream` functions. Still, the
+  conceptual change should make the use of `Streams` more ergonomic going
+  forward.
+
+  As a result of and in addition to the conceptual change, the `Stream`
+  interface got an overhaul. The concrete changes are:
+
+  * The internals of the `Stream` are now exposed, but with big warnings about
+    unsafe usage related to finiteness.
+  * Added new `runStreamN` and `runStreamIndefinitely` functions.
+  * Renamed `mkInfinite` to `unsafeMkInfinite`.
+  * Added new `isFinite` and `isInfinite` queries.
+  * Added a new `genFiniteN` function.
+  * Removed `genMaybe'`, as it was just a specific instantiation of `genMaybe`
+    that has no clear benefit being its own top-level function.
+  * Added a new `liftShrinkStream` function.
+  * Updated documentation.
 
 ## 0.3.1.0 -- 2024-12-10
 

fs-sim/fs-sim.cabal

@@ -63,6 +63,7 @@ test-suite fs-sim-test
   other-modules:
     Test.System.FS.Sim.Error
     Test.System.FS.Sim.FsTree
+    Test.System.FS.Sim.Stream
     Test.System.FS.StateMachine
     Test.Util
     Test.Util.RefEnv
@@ -74,6 +75,7 @@ test-suite fs-sim-test
     , bifunctors
     , bytestring
     , containers
+    , deepseq
     , fs-api
     , fs-sim
     , generics-sop

fs-sim/src/System/FS/Sim/Error.hs

@@ -433,8 +433,10 @@ genErrors genPartialWrites genSubstituteWithJunk = do
     hPutBufSomeAtE <- commonPutErrors
     return Errors {..}
   where
-    streamGen l = Stream.genInfinite . Stream.genMaybe' l . QC.elements
-    streamGen' l = Stream.genInfinite . Stream.genMaybe' l . QC.frequency
+    genMaybe' = Stream.genMaybe 2
+
+    streamGen l = Stream.genInfinite . genMaybe' l . QC.elements
+    streamGen' l = Stream.genInfinite . genMaybe' l . QC.frequency
 
     commonGetErrors = streamGen' 20
       [ (1, return $ Left FsReachedEOF)

fs-sim/src/System/FS/Sim/Stream.hs

@@ -1,60 +1,85 @@
 {-# LANGUAGE DeriveFunctor       #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
--- | Possibly infinite streams of @'Maybe' a@s.
+-- | Finite and infinite streams of @'Maybe' a@s.
 module System.FS.Sim.Stream (
     -- * Streams
-    Stream
+    Stream (..)
+  , InternalInfo (..)
     -- * Running
   , runStream
+  , runStreamN
+  , runStreamIndefinitely
     -- * Construction
   , always
   , empty
-  , mkInfinite
   , repeating
+  , unsafeMkInfinite
   , unsafeMkFinite
+    -- * Modify
+  , filter
     -- * Query
   , null
+  , isFinite
+  , isInfinite
     -- * Generation and shrinking
   , genFinite
+  , genFiniteN
   , genInfinite
   , genMaybe
-  , genMaybe'
   , shrinkStream
+  , liftShrinkStream
   ) where
 
 import           Control.Monad (replicateM)
-import           Prelude hiding (null)
+import           Prelude hiding (filter, isInfinite, null)
+import qualified Prelude
 import qualified Test.QuickCheck as QC
 import           Test.QuickCheck (Gen)
 
 {-------------------------------------------------------------------------------
   Streams
 -------------------------------------------------------------------------------}
 
--- | A 'Stream' is a stream of @'Maybe' a@s, which is /possibly/ infinite or
--- /definitely/ finite.
---
--- Finiteness is tracked internally and used for 'QC.shrink'ing and the 'Show'
--- instance.
-data Stream a = Stream {
-      -- | Info about the size of the stream.
-      _streamInternalInfo :: InternalInfo
-    , _getStream          :: [Maybe a]
+-- | A stream of @'Maybe' a@s that can be infinite.
+data Stream a =
+  -- | UNSAFE: when constructing, modifying, or accessing the internals of a
+  -- 'Stream', it is the responsibility of the user to preserve the following
+  -- invariant:
+  --
+  -- INVARIANT: if the stream is marked as 'Infinite', then the internal list
+  -- should be infinite. If the stream is marked as 'Finite', then the internal
+  -- list should finite.
+  --
+  -- * If the internal list is infinite but marked as 'Finite', then 'QC.shrink'
+  --   or 'show' on the corresponding stream will diverge.
+  --
+  -- * If the internal list is finite but marked as 'Infinite', then 'QC.shrink'
+  --   on the corresponding stream will degrade to an infinite list of empty
+  --   streams.
+  UnsafeStream {
+      -- | UNSAFE: see 'UnsafeStream' for more information.
+      --
+      -- Info about the finiteness of the stream. It is used for 'QC.shrink'ing
+      -- and the 'Show' instance.
+      unsafeStreamInternalInfo :: InternalInfo
+      -- | UNSAFE: see 'UnsafeStream' for more information.
+      --
+      -- The internal list underlying the stream.
+    , unsafeStreamList         :: [Maybe a]
     }
   deriving Functor
 
--- | Tag for 'Stream's that describes whether it is either /definitely/ a finite
--- stream, or /possibly/ an infinite stream.
+-- | Tag for 'Stream's that describes whether it is finite or infinite.
 --
--- Useful for the 'Show' instance of 'Stream': when a 'Stream' is /definitely/
--- finite, we can safely print the full stream.
+-- Useful for the 'Show' instance of 'Stream': when a 'Stream' is finite, we can
+-- safely print the full stream.
 data InternalInfo = Infinite | Finite
 
--- | Fully shows a 'Stream' if it is /definitely/ finite, or prints a
--- placeholder string if it is /possibly/ infinite.
+-- | Fully shows a 'Stream' if it is finite, or prints a placeholder string if
+-- it is infinite.
 instance Show a => Show (Stream a) where
-  showsPrec n (Stream info xs) = case info of
+  showsPrec n (UnsafeStream info xs) = case info of
       Infinite -> ("<infinite stream>" ++)
       Finite   -> (if n > 10 then ('(':) else id)
                 . shows xs
@@ -65,104 +90,149 @@ instance Show a => Show (Stream a) where
   Running
 -------------------------------------------------------------------------------}
 
--- | Advance the 'Stream'. Return the @'Maybe' a@ and the remaining 'Stream'.
+-- | \( O(1) \): advance the 'Stream'. Return the @'Maybe' a@ and the remaining
+-- 'Stream'.
 --
 -- Returns 'Nothing' by default if the 'Stream' is empty.
 runStream :: Stream a -> (Maybe a, Stream a)
-runStream s@(Stream _    []    ) = (Nothing, s)
-runStream   (Stream info (a:as)) = (a, Stream info as)
+runStream s@(UnsafeStream _    []    ) = (Nothing, s)
+runStream   (UnsafeStream info (a:as)) = (a, UnsafeStream info as)
+
+-- | \( O(n) \): like 'runStream', but advancing the stream @n@ times.
+--
+-- If @n<=0@, then the stream is advanced @0@ times.
+runStreamN :: Int -> Stream a -> ([Maybe a], Stream a)
+runStreamN n s
+  | n <= 0 = ([], s)
+  | otherwise =
+      let (x, s') = runStream s
+          (xs, s'') = runStreamN (n-1) s'
+      in  (x:xs, s'')
+
+-- | \( O(\infty) \): like 'runStream', but advancing the stream indefinitely.
+--
+-- For infinite streams, this produces an infinite list. For finite streams,
+-- this produces a finite list.
+runStreamIndefinitely :: Stream a -> [Maybe a]
+runStreamIndefinitely (UnsafeStream _ as) = as ++ repeat Nothing
 
 {-------------------------------------------------------------------------------
   Construction
 -------------------------------------------------------------------------------}
 
 -- | Make an empty 'Stream'.
 empty :: Stream a
-empty = Stream Finite []
+empty = UnsafeStream Finite []
 
 -- | Make a 'Stream' that always generates the given @a@.
 always :: a -> Stream a
-always x = Stream Infinite (repeat (Just x))
+always x = UnsafeStream Infinite (repeat (Just x))
 
 -- | Make a 'Stream' that infinitely repeats the given list.
 repeating :: [Maybe a] -> Stream a
-repeating xs = Stream Infinite $ concat (repeat xs)
+repeating xs = UnsafeStream Infinite $ cycle xs
 
--- | UNSAFE: Make a 'Stream' that is marked as definitely finite.
---
--- This is unsafe since a user can pass in any list, and evaluating
--- 'Test.QuickCheck.shrink' or 'show' on the resulting 'Stream' will diverge. It
--- is the user's responsibility to only pass in a finite list.
+-- | UNSAFE: Make a 'Stream' that is marked as finite. It is the user's
+-- responsibility to only pass in finite lists. See 'UnsafeStream' for more
+-- information.
 unsafeMkFinite :: [Maybe a] -> Stream a
-unsafeMkFinite = Stream Finite
+unsafeMkFinite = UnsafeStream Finite
 
--- | Make a 'Stream' that is marked as possibly infinite.
-mkInfinite :: [Maybe a] -> Stream a
-mkInfinite = Stream Infinite
+-- | UNSAFE: Make a 'Stream' that is marked as infinite. It is the user's
+-- responsibility to only pass in infinite lists. See 'UnsafeStream' for more
+-- information.
+unsafeMkInfinite :: [Maybe a] -> Stream a
+unsafeMkInfinite = UnsafeStream Infinite
+
+{-------------------------------------------------------------------------------
+  Modify
+-------------------------------------------------------------------------------}
+
+-- | Filter a 'Stream', preserving finiteness.
+filter :: (Maybe a -> Bool) -> Stream a -> Stream a
+filter p (UnsafeStream info xs) = UnsafeStream info (Prelude.filter p xs)
 
 {-------------------------------------------------------------------------------
   Query
 -------------------------------------------------------------------------------}
 
--- | Return 'True' if the stream is empty.
+-- | Check that the stream is empty.
 --
--- A stream consisting of only 'Nothing's (even if it is only one) is not
--- considered to be empty.
+-- In general, a stream is only empty if the stream is equivalent to 'empty'.
+--
+-- A finite\/infinite stream consisting of only 'Nothing's is not considered to
+-- be empty. In particular, @'null' ('always' Nothing) /= True@.
 null :: Stream a -> Bool
-null (Stream _ []) = True
-null _             = False
+null (UnsafeStream Finite []) = True
+null _                        = False
+
+-- | Check that the stream is finite
+isFinite :: Stream a -> Bool
+isFinite (UnsafeStream Finite _)   = True
+isFinite (UnsafeStream Infinite _) = False
+
+-- | Check that the stream is infinite
+isInfinite :: Stream a -> Bool
+isInfinite (UnsafeStream Finite _)   = False
+isInfinite (UnsafeStream Infinite _) = True
 
 {-------------------------------------------------------------------------------
   Generation and shrinking
 -------------------------------------------------------------------------------}
 
--- | Shrink a stream like it is an 'Test.QuickCheck.InfiniteList'.
+-- | Shrink a stream like it is an 'QC.InfiniteList'.
+--
+-- Infinite streams are shrunk differently than lists that are finite, which is
+-- to ensure that we shrink infinite lists towards finite lists.
+--
+-- * Infinite streams are shrunk by taking finite prefixes of the argument
+--   stream. Note that there are an infinite number of finite prefixes, so even
+--   though the *shrink list* is infinite, the individual *list elements* are
+--   finite.
 --
--- Possibly infinite streams are shrunk differently than lists that are
--- definitely finite, which is to ensure that shrinking terminates.
--- * Possibly infinite streams are shrunk by taking finite prefixes of the
---  argument stream. As such, shrinking a possibly infinite stream creates
---  definitely finite streams.
--- * Definitely finite streams are shrunk like lists are shrunk normally,
---   preserving that the created streams are still definitely finite.
+-- * Finite streams are shrunk like lists are shrunk normally, preserving
+--   finiteness.
 shrinkStream :: Stream a -> [Stream a]
-shrinkStream (Stream info xs0) = case info of
-    Infinite -> Stream Finite <$> [take n xs0 | n <- map (2^) [0 :: Int ..]]
-    Finite   -> Stream Finite <$> QC.shrinkList (const []) xs0
+shrinkStream (UnsafeStream info xs0) = case info of
+    Infinite -> UnsafeStream Finite <$> [take n xs0 | n <- map (2^) [0 :: Int ..]]
+    Finite   -> UnsafeStream Finite <$> QC.shrinkList (const []) xs0
+
+-- | Like 'shrinkStream', but with a custom shrinker for elements of the stream.
+liftShrinkStream :: (Maybe a -> [Maybe a]) -> Stream a -> [Stream a]
+liftShrinkStream shrinkOne (UnsafeStream info xs0) = case info of
+    Infinite -> UnsafeStream Finite <$> [take n xs0 | n <- map (2^) [0 :: Int ..]]
+    Finite   -> UnsafeStream Finite <$> QC.shrinkList shrinkOne xs0
 
 -- | Make a @'Maybe' a@ generator based on an @a@ generator.
 --
 -- Each element has a chance of being either 'Nothing' or an element generated
--- with the given @a@ generator (wrapped in a 'Just').
---
--- The first argument is the likelihood (as used by 'QC.frequency') of a
--- 'Just' where 'Nothing' has likelihood 2.
+-- with the given @a@ generator (wrapped in a 'Just'). These /likelihoods/ are
+-- passed to 'QC.frequency'.
 genMaybe ::
-     Int   -- ^ Likelihood of 'Nothing'
-  -> Int   -- ^ Likelihood of @'Just' a@
+     Int -- ^ Likelihood of 'Nothing'
+  -> Int -- ^ Likelihood of @'Just' a@
   -> Gen a
   -> Gen (Maybe a)
 genMaybe nLi jLi genA = QC.frequency
     [ (nLi, return Nothing)
     , (jLi, Just <$> genA)
     ]
 
--- | Like 'genMaybe', but with the likelihood of 'Nothing' fixed to @2@. 'QC.frequency'
-genMaybe' ::
-     Int   -- ^ Likelihood of @'Just' a@
-  -> Gen a
+-- | Generate a finite 'Stream' of length @n@.
+genFiniteN ::
+     Int -- ^ Requested size of finite stream.
   -> Gen (Maybe a)
-genMaybe' = genMaybe 2
+  -> Gen (Stream a)
+genFiniteN n gen = UnsafeStream Finite <$> replicateM n gen
 
--- | Generate a finite 'Stream' of length @n@.
+-- | Generate a sized, finite 'Stream'.
 genFinite ::
-     Int           -- ^ Requested size of finite stream. Tip: use 'genMaybe'.
-  -> Gen (Maybe a)
+     Gen (Maybe a)
   -> Gen (Stream a)
-genFinite n gen = Stream Finite <$> replicateM n gen
+genFinite gen = UnsafeStream Finite <$> QC.listOf gen
 
 -- | Generate an infinite 'Stream'.
 genInfinite ::
-     Gen (Maybe a)  -- ^ Tip: use 'genMaybe'.
+     Gen (Maybe a)
   -> Gen (Stream a)
-genInfinite gen = Stream Infinite <$> QC.infiniteListOf gen
+genInfinite gen = UnsafeStream Infinite <$> QC.infiniteListOf gen

fs-sim/test/Main.hs

@@ -2,12 +2,14 @@ module Main (main) where
 
 import qualified Test.System.FS.Sim.Error
 import qualified Test.System.FS.Sim.FsTree
+import qualified Test.System.FS.Sim.Stream
 import qualified Test.System.FS.StateMachine
 import           Test.Tasty
 
 main :: IO ()
 main = defaultMain $ testGroup "fs-sim-test" [
       Test.System.FS.Sim.Error.tests
     , Test.System.FS.Sim.FsTree.tests
+    , Test.System.FS.Sim.Stream.tests
     , Test.System.FS.StateMachine.tests
     ]