Idris2Doc : Data.MSF.Core

Data.MSF.Core

(source)
Provides a data type for Monadic Stream Functions (MSFs)
together with associated interface implementations and
some core functionality.

An MSF is an effectful computation from an input of type `i`
to an output of type `o`, that can be described using a rich
library of combinators and evaluated using function
`Data.MSF.Running.step`,
which not only produces an output for every input value
but also a new MSF to be used in the next evaluation step.

Reexports

importpublic Data.MSF.Event

Definitions

0FanList : (Type->Type) ->Type->ListType->Type
  A heterogeneous list of MSFs all of which
accept the same input type. This is used for
broadcasting an input value across several MSFs,
collecting the result as an n-ary product.
See also function `fan`.

Totality: total
Visibility: public export
0CollectList : (Type->Type) ->ListType->Type->Type
  A heterogeneous list of MSFs all of which
produce the same type of outup. This is used for
choosing a single MSF for producing a result based
on an n-ary sum as input. See also function `collect`.

Totality: total
Visibility: public export
dataParList : (Type->Type) ->ListType->ListType->Type
  A heterogeneous list of MSFs. This is used both
for running several unrelated MSFs in parallel, in
which case it takes an n-ary product as input
and produces an n-ary product as output (see
function `par`), as well as for selecting a single
MSF to run based on an n-ary sum as input, in which
case a value of an n-ary sum is produced as output
(see function `choice` for this use case).

Totality: total
Visibility: public export
Constructors:
Nil : ParListm [] []
(::) : MSFmio->ParListmisos->ParListm (i::is) (o::os)
dataMSF : (Type->Type) ->Type->Type->Type
Totality: total
Visibility: public export
Constructors:
Id : MSFmii
  The identity MSF
Const : o->MSFmio
  The constant MSF
Arr : (i->o) ->MSFmio
  Lifts a pure function to an MSF
Lifted : (i->mo) ->MSFmio
  Lifts an effectful computation to an MSF
Seq : MSFmix->MSFmxo->MSFmio
  Sequencing of MSFs
Par : ParListmisos->MSFm (HListis) (HListos)
  Parallelising MSFs
Fan : FanListmios->MSFmi (HListos)
  Broadcasting a value to a list of MSFs
all taking the same input
Choice : ParListmisos->MSFm (HSumis) (HSumos)
  Choosing an MSF based on an n-ary sum as input
Collect : CollectListmiso->MSFm (HSumis) o
  Choosing an MSF (all of which produce the same output)
based on an n-ary sum as input
Loop : s->MSFm (HList [s, i]) (HList [s, o]) ->MSFmio
  Feedback loops (stateful computations)
Switch : MSFmi (Eithereo) -> (e->MSFmio) ->MSFmio
  Single time switching: Upon the first event,
the second stream function is calculated,
evaluated immediately and used henceforth.

Hints:
Applicative (MSFmi)
Fractionalo=>Fractional (MSFmio)
FromStringo=>FromString (MSFmio)
Functor (MSFmi)
Integralo=>Integral (MSFmio)
Monoido=>Monoid (MSFmio)
Nego=>Neg (MSFmio)
Numo=>Num (MSFmio)
Semigroupo=>Semigroup (MSFmio)
id : MSFmii
  The identity MSF

Totality: total
Visibility: export
const : o->MSFmio
  A constant MSF

Totality: total
Visibility: export
arr : (i->o) ->MSFmio
  Lifting a pure function to an MSF

Totality: total
Visibility: export
arrM : (i->mo) ->MSFmio
  Lifting an effectful computation to an MSF

Totality: total
Visibility: export
constM : mo->MSFmio
  Lifting a value in a context to an MSF

Totality: total
Visibility: export
(>>>) : MSFmix->MSFmxo->MSFmio
  Sequencing of MSFs

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 1
par : ParListmisos->MSFm (HListis) (HListos)
  Runs a bundle of MSFs in parallel. This is
a generalization of `(***)` from `Control.Arrow`.

Totality: total
Visibility: export
fan : FanListmios->MSFmi (HListos)
  Broadcasts an input value across a list of MSFs,
all of which must accept the same type of input.
This is a generalization of `(&&&)` from `Control.Arrow`.

Totality: total
Visibility: export
elementwise2 : (o1->o2->o3) ->MSFmio1->MSFmio2->MSFmio3
  Apply a binary function to the result of running
two MSFs in parallel.

Totality: total
Visibility: export
choice : ParListmisos->MSFm (HSumis) (HSumos)
  Choose an MSF to run depending the input value
This is a generalization of `(+++)` from `Control.Arrow`.

Totality: total
Visibility: export
collect : CollectListmiso->MSFm (HSumis) o
  Choose an MSF all of which produce the same output.
This is a generalization of `(\|/)` from `Control.Arrow`.

Totality: total
Visibility: export
feedback : s->MSFm (HList [s, i]) (HList [s, o]) ->MSFmio
  Feedback loops: Given an initial state value,
we can feedback the result of each evaluation
step and us it as the new state for the next step.

Totality: total
Visibility: export