Data.MSF.Running

Definitions

step : Monad m => MSF m i o -> i -> m (o, MSF m i o)

  Single step evaluation of monadic stream functions.
  This is used to drive a typical application using
  MSFs for processing input.

Totality: total
Visibility: export

embed : Monad m => List i -> MSF m i o -> m (List o)

  Uses the given MSF to process a list of input
  values. This is useful for testing MSFs.

Totality: total
Visibility: export

embedI : List i -> MSF Identity i o -> List o

  `embed` using the `Identity` monad.

Totality: total
Visibility: export

size : MSF m i o -> Nat

  Calculates the size (number of constructors)
  of a MSF. This is useful for testing and
  possibly optimizing applications.

Totality: total
Visibility: export

record Handler : (Type -> Type) -> Type -> Type

  An event handler typically used as an auto-implicit argument

Totality: total
Visibility: public export
Constructor: 

H : (e -> m ()) -> Handler m e

Projection: 

.handle_ : Handler m e -> e -> m ()

Hint: 

Contravariant (Handler m)

.handle_ : Handler m e -> e -> m ()

Totality: total
Visibility: public export

handle_ : Handler m e -> e -> m ()

Totality: total
Visibility: public export

handle : Handler m e => e -> m ()

Totality: total
Visibility: export

reactimate : HasIO m => (Handler m e -> m (MSF m e (), m ())) -> m (m ())

  Create a monadic stream function (the reactive behavior
  of an UI, for instance)
  by passing the given generation function `sf` an event handler
  that can be registered at reactive components.
  The MSF will then be invoked and
  evaluated whenever an event is fired.

Totality: total
Visibility: export

reactimateIni : HasIO m => e -> (Handler m e -> m (MSF m e (), m ())) -> m (m ())

  Like `reactimate`, but evaluates the `MSF` once at the beginning by
  passing it the given initial event.

Totality: total
Visibility: export