{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE Rank2Types     #-}
-- | Monadic Stream Functions are synchronized stream functions
--   with side effects.
--
--   'MSF's are defined by a function
--   @unMSF :: MSF m a b -> a -> m (b, MSF m a b)@
--   that executes one step of a simulation, and produces an output in a
--   monadic context, and a continuation to be used for future steps.
--
--   'MSF's are a generalisation of the implementation mechanism used by Yampa,
--   Wormholes and other FRP and reactive implementations.
--
--   This modules defines only the minimal core. Hopefully, other functions can be
--   defined in terms of the functions in this module without accessing the
--   MSF constuctor.


-- NOTE TO IMPLEMENTORS:
--
-- This module contains the core. Only the core. It should be possible
-- to define every function and type outside this module, except for the
-- instances for ArrowLoop, ArrowChoice, etc., without access to the
-- internal constructor for MSF and the function 'unMSF'.
--
-- It's very hard to know what IS essential to framework and if we start
-- adding all the functions and instances that *may* be useful in one
-- module.
--
-- By separating some instances and functions in other modules, we can
-- easily understand what is the essential idea and then analyse how it
-- is affected by an extension. It also helps demonstrate that something
-- works for MSFs + ArrowChoice, or MSFs + ArrowLoop, etc.
--
-- To address potential violations of basic design principles (like 'not
-- having orphan instances'), the main module Data.MonadicStreamFunction
-- exports everything. Users should *never* import this module here
-- individually, but the main module instead.

module Data.MonadicStreamFunction.InternalCore where

-- External
import Control.Arrow
import Control.Applicative
import Control.Category (Category(..))
import Control.Monad
import Control.Monad.Base
import Control.Monad.Trans.Class
import Prelude hiding ((.), id, sum)

-- * Definitions

-- | Stepwise, side-effectful 'MSF's without implicit knowledge of time.
--
-- 'MSF's should be applied to streams or executed indefinitely or until they
-- terminate. See 'reactimate' and 'reactimateB' for details. In general,
-- calling the value constructor 'MSF' or the function 'unMSF' is discouraged.
data MSF m a b = MSF { MSF m a b -> a -> m (b, MSF m a b)
unMSF :: a -> m (b, MSF m a b) }

-- Instances

-- | Instance definition for 'Category'. Defines 'id' and '.'.
instance Monad m => Category (MSF m) where
  id :: MSF m a a
id = MSF m a a
forall a. MSF m a a
go
    where go :: MSF m b b
go = (b -> m (b, MSF m b b)) -> MSF m b b
forall (m :: * -> *) a b. (a -> m (b, MSF m a b)) -> MSF m a b
MSF ((b -> m (b, MSF m b b)) -> MSF m b b)
-> (b -> m (b, MSF m b b)) -> MSF m b b
forall a b. (a -> b) -> a -> b
$ \b
a -> (b, MSF m b b) -> m (b, MSF m b b)
forall (m :: * -> *) a. Monad m => a -> m a
return (b
a, MSF m b b
go)
  MSF m b c
sf2 . :: MSF m b c -> MSF m a b -> MSF m a c
. MSF m a b
sf1 = (a -> m (c, MSF m a c)) -> MSF m a c
forall (m :: * -> *) a b. (a -> m (b, MSF m a b)) -> MSF m a b
MSF ((a -> m (c, MSF m a c)) -> MSF m a c)
-> (a -> m (c, MSF m a c)) -> MSF m a c
forall a b. (a -> b) -> a -> b
$ \a
a -> do
    (b
b, MSF m a b
sf1') <- MSF m a b -> a -> m (b, MSF m a b)
forall (m :: * -> *) a b. MSF m a b -> a -> m (b, MSF m a b)
unMSF MSF m a b
sf1 a
a
    (c
c, MSF m b c
sf2') <- MSF m b c -> b -> m (c, MSF m b c)
forall (m :: * -> *) a b. MSF m a b -> a -> m (b, MSF m a b)
unMSF MSF m b c
sf2 b
b
    let sf' :: MSF m a c
sf' = MSF m b c
sf2' MSF m b c -> MSF m a b -> MSF m a c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. MSF m a b
sf1'
    c
c c -> m (c, MSF m a c) -> m (c, MSF m a c)
`seq` (c, MSF m a c) -> m (c, MSF m a c)
forall (m :: * -> *) a. Monad m => a -> m a
return (c
c, MSF m a c
sf')

-- * Monadic computations and 'MSF's

-- | Generic lifting of a morphism to the level of 'MSF's.
--
-- Natural transformation to the level of 'MSF's.
--
-- __Mathematical background:__ The type @a -> m (b, c)@ is a functor in @c@,
-- and @MSF m a b@ is its greatest fixpoint, i.e. it is isomorphic to the type
-- @a -> m (b, MSF m a b)@, by definition.
-- The types @m@, @a@ and @b@ are parameters of the functor.
-- Taking a fixpoint is functorial itself, meaning that a morphism
-- (a natural transformation) of two such functors gives a morphism
-- (an ordinary function) of their fixpoints.
--
-- This is in a sense the most general "abstract" lifting function,
-- i.e. the most general one that only changes input, output and side effect
-- types, and doesn't influence control flow.
-- Other handling functions like exception handling or 'ListT' broadcasting
-- necessarily change control flow.
morphGS :: Monad m2
        => (forall c . (a1 -> m1 (b1, c)) -> (a2 -> m2 (b2, c)))
          -- ^ The natural transformation. @mi@, @ai@ and @bi@ for @i = 1, 2@
          --   can be chosen freely, but @c@ must be universally quantified
        -> MSF m1 a1 b1
        -> MSF m2 a2 b2
morphGS :: (forall c. (a1 -> m1 (b1, c)) -> a2 -> m2 (b2, c))
-> MSF m1 a1 b1 -> MSF m2 a2 b2
morphGS forall c. (a1 -> m1 (b1, c)) -> a2 -> m2 (b2, c)
morph MSF m1 a1 b1
msf = (a2 -> m2 (b2, MSF m2 a2 b2)) -> MSF m2 a2 b2
forall (m :: * -> *) a b. (a -> m (b, MSF m a b)) -> MSF m a b
MSF ((a2 -> m2 (b2, MSF m2 a2 b2)) -> MSF m2 a2 b2)
-> (a2 -> m2 (b2, MSF m2 a2 b2)) -> MSF m2 a2 b2
forall a b. (a -> b) -> a -> b
$ \a2
a2 -> do
  (b2
b2, MSF m1 a1 b1
msf') <- (a1 -> m1 (b1, MSF m1 a1 b1)) -> a2 -> m2 (b2, MSF m1 a1 b1)
forall c. (a1 -> m1 (b1, c)) -> a2 -> m2 (b2, c)
morph (MSF m1 a1 b1 -> a1 -> m1 (b1, MSF m1 a1 b1)
forall (m :: * -> *) a b. MSF m a b -> a -> m (b, MSF m a b)
unMSF MSF m1 a1 b1
msf) a2
a2
  (b2, MSF m2 a2 b2) -> m2 (b2, MSF m2 a2 b2)
forall (m :: * -> *) a. Monad m => a -> m a
return (b2
b2, (forall c. (a1 -> m1 (b1, c)) -> a2 -> m2 (b2, c))
-> MSF m1 a1 b1 -> MSF m2 a2 b2
forall (m2 :: * -> *) a1 (m1 :: * -> *) b1 a2 b2.
Monad m2 =>
(forall c. (a1 -> m1 (b1, c)) -> a2 -> m2 (b2, c))
-> MSF m1 a1 b1 -> MSF m2 a2 b2
morphGS forall c. (a1 -> m1 (b1, c)) -> a2 -> m2 (b2, c)
morph MSF m1 a1 b1
msf')

-- * Feedback loops

-- | Well-formed looped connection of an output component as a future input.
feedback :: Monad m => c -> MSF m (a, c) (b, c) -> MSF m a b
feedback :: c -> MSF m (a, c) (b, c) -> MSF m a b
feedback c
c MSF m (a, c) (b, c)
sf = (a -> m (b, MSF m a b)) -> MSF m a b
forall (m :: * -> *) a b. (a -> m (b, MSF m a b)) -> MSF m a b
MSF ((a -> m (b, MSF m a b)) -> MSF m a b)
-> (a -> m (b, MSF m a b)) -> MSF m a b
forall a b. (a -> b) -> a -> b
$ \a
a -> do
  ((b
b', c
c'), MSF m (a, c) (b, c)
sf') <- MSF m (a, c) (b, c) -> (a, c) -> m ((b, c), MSF m (a, c) (b, c))
forall (m :: * -> *) a b. MSF m a b -> a -> m (b, MSF m a b)
unMSF MSF m (a, c) (b, c)
sf (a
a, c
c)
  (b, MSF m a b) -> m (b, MSF m a b)
forall (m :: * -> *) a. Monad m => a -> m a
return (b
b', c -> MSF m (a, c) (b, c) -> MSF m a b
forall (m :: * -> *) c a b.
Monad m =>
c -> MSF m (a, c) (b, c) -> MSF m a b
feedback c
c' MSF m (a, c) (b, c)
sf')

-- * Execution/simulation

-- | Apply a monadic stream function to a list.
--
-- Because the result is in a monad, it may be necessary to
-- traverse the whole list to evaluate the value in the results to WHNF.
-- For example, if the monad is the maybe monad, this may not produce anything
-- if the 'MSF' produces 'Nothing' at any point, so the output stream cannot
-- consumed progressively.
--
-- To explore the output progressively, use 'arrM' and '(>>>)'', together
-- with some action that consumes/actuates on the output.
--
-- This is called 'runSF' in Liu, Cheng, Hudak, "Causal Commutative Arrows and
-- Their Optimization"
embed :: Monad m => MSF m a b -> [a] -> m [b]
embed :: MSF m a b -> [a] -> m [b]
embed MSF m a b
_  []     = [b] -> m [b]
forall (m :: * -> *) a. Monad m => a -> m a
return []
embed MSF m a b
sf (a
a:[a]
as) = do
  (b
b, MSF m a b
sf') <- MSF m a b -> a -> m (b, MSF m a b)
forall (m :: * -> *) a b. MSF m a b -> a -> m (b, MSF m a b)
unMSF MSF m a b
sf a
a
  [b]
bs       <- MSF m a b -> [a] -> m [b]
forall (m :: * -> *) a b. Monad m => MSF m a b -> [a] -> m [b]
embed MSF m a b
sf' [a]
as
  [b] -> m [b]
forall (m :: * -> *) a. Monad m => a -> m a
return (b
bb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
bs)

-- | Run an 'MSF' indefinitely passing a unit-carrying input stream.
reactimate :: Monad m => MSF m () () -> m ()
reactimate :: MSF m () () -> m ()
reactimate MSF m () ()
sf = do
  (()
_, MSF m () ()
sf') <- MSF m () () -> () -> m ((), MSF m () ())
forall (m :: * -> *) a b. MSF m a b -> a -> m (b, MSF m a b)
unMSF MSF m () ()
sf ()
  MSF m () () -> m ()
forall (m :: * -> *). Monad m => MSF m () () -> m ()
reactimate MSF m () ()
sf'