Idris2Doc : Data.MSF.Switch

Data.MSF.Switch

(source)
Switching Combinators

Switches allow us to dynamically change the structure
(wiring) of a running network of stream functions.
Semantically, the react on discrete events, but
some of the switching primitives in this module use
the `Either` data type if it allows us to more exactly
describe the semantics of a switch.

Definitions

switchE : MSFmi (Eithereo) -> (e->MSFmio) ->MSFmio
  Produces output of the first MSF until it produces
a `Left`, in which case the event will be used to
create a new MSF, which will be immediately evaluated
and used henceforth.

This is a one-time switch, which is often used to
run an MSF a fixed number of times or until a certain
event occurs, after which the replacement will be used.

Note: It is unsafe to use this in a recursive setting,
as it would allow us to create an infinite loop
of streaming functions, all of which return `Left`s
forever. Luckily, the totality checker will prevent us
from doing this.

Totality: total
Visibility: export
switch : MSFmi (HList [o, Evente]) -> (e->MSFmio) ->MSFmio
  Produces output of the given MSF until it fires an event,
in which case a new MSF is created,
which will be evaluated immediately and used henceforth.

This uses `switchE` internally, so all restrictions mentioned
there apply.

Totality: total
Visibility: export
dSwitch : MSFmi (HList [o, Evente]) -> (e->MSFmio) ->MSFmio
  Produces output of the given MSF until it fires an event,
in which case a new MSF is created,
which will be used in all further evaluation steps.

Totality: total
Visibility: export
rSwitch : Monadm=>MSFmio->MSFm (HList [Event (MSFmio), i]) o
Totality: total
Visibility: export
drSwitch : Monadm=>MSFmio->MSFm (HList [Event (MSFmio), i]) o
Totality: total
Visibility: export
drswitchWhen : Monadm=>MSFmio->MSFmi (Evente) -> (e->MSFmio) ->MSFmio
  Produces output of the first MSF until the second
fires an event, in which case a new MSF is created,
which will be used in all futre evaluation cycles.

Totality: total
Visibility: export