{-# LANGUAGE Rank2Types #-}
-- |
-- Copyright  : (c) Ivan Perez and Manuel Baerenz, 2016
-- License    : BSD3
-- Maintainer : ivan.perez@keera.co.uk
--
-- 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. By default, you should import
-- "Data.MonadicStreamFunction.Core" or "Data.MonadicStreamFunction" whenever
-- possible, and define your functions without accessing the MSF constuctor.
-- Those modules, as well as other modules in dunai, also provide convenient
-- instances. This module may be useful if you are extending dunai with
-- functionality that cannot be (conveniently) expressed using the existing
-- high-level API.

-- 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 imports
import Control.Category (Category (..))
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 { forall (m :: * -> *) a b. 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 :: forall a. MSF m a a
id = forall a. MSF m a a
go
    where
      go :: MSF m b b
go = forall (m :: * -> *) a b. (a -> m (b, MSF m a b)) -> MSF m a b
MSF forall a b. (a -> b) -> a -> b
$ \b
a -> forall (m :: * -> *) a. Monad m => a -> m a
return (b
a, MSF m b b
go)

  MSF m b c
sf2 . :: forall b c a. MSF m b c -> MSF m a b -> MSF m a c
. MSF m a b
sf1 = forall (m :: * -> *) a b. (a -> m (b, MSF m a b)) -> MSF m a b
MSF forall a b. (a -> b) -> a -> b
$ \a
a -> do
    (b
b, MSF m a b
sf1') <- 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') <- 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' 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 seq :: forall a b. a -> b -> b
`seq` 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 (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 = forall (m :: * -> *) a b. (a -> m (b, MSF m a b)) -> MSF m a b
MSF forall a b. (a -> b) -> a -> b
$ \a2
a2 -> do
  (b2
b2, MSF m1 a1 b1
msf') <- forall c. (a1 -> m1 (b1, c)) -> a2 -> m2 (b2, c)
morph (forall (m :: * -> *) a b. MSF m a b -> a -> m (b, MSF m a b)
unMSF MSF m1 a1 b1
msf) a2
a2
  forall (m :: * -> *) a. Monad m => a -> m a
return (b2
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 :: 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 = forall (m :: * -> *) a b. (a -> m (b, MSF m a b)) -> MSF m a b
MSF forall a b. (a -> b) -> a -> b
$ \a
a -> do
  ((b
b', c
c'), MSF m (a, c) (b, c)
sf') <- 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)
  forall (m :: * -> *) a. Monad m => a -> m a
return (b
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 :: forall (m :: * -> *) a b. Monad m => MSF m a b -> [a] -> m [b]
embed MSF m a 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') <- 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       <- forall (m :: * -> *) a b. Monad m => MSF m a b -> [a] -> m [b]
embed MSF m a b
sf' [a]
as
  forall (m :: * -> *) a. Monad m => a -> m a
return (b
bforall a. a -> [a] -> [a]
:[b]
bs)

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