FS.Core

Reexports

Definitions

data Pull : (List Type -> Type -> Type) -> Type -> List Type -> Type -> Type

  A `Pull f o es r` is a - possibly infinite - series of effectful
  computations running in monad `f`, producing an arbitrary sequence
  of chunks of values of type `c o` along the way, that eventually
  terminates either with an error of type `HSum es` or with a result
  of type `r`.
  
  A `Pull` is a monad with relation to `r`, so a sequencing of `Pull`s
  via bind `(>>=)` means a sequencing of the chunks of output generated
  along the way. For instance, the following `Pull` will produce the
  values `[1,2,3,4,5,6]` when being run:
  
  ```idris2
  emit [1,2,3] >> emit [4,5,6]
  ```
  
  A `Pull` provides capabilities for safe resource management via
  `FS.Scope`s, allowing us to release allocated resources as soon as
  
   * the pull is exhausted and produces no more output.
   * evaluating the pull aborts with an error.
   * a pull will not longer be asked to produce additional values
     because an outer pull has been exhaused.
  
  The last case occurs for instance when we stop evaluating a `Stream`
  via `take` or `takeWhile`.
  
  About the effect type `f`: Most non-trivial `Pull`s and `Stream`s come
  with the potential of failure. In addition, running a `Pull` to completion
  requires (thread-local) mutable state to keep tracks of the evaluation
  scopes. Effect type `f` must therefore implement interface `Data.Linear.ELift1`
  at the very least. This still allows us to run a `Pull` or `Stream`
  as a pure computation, for instance when using `Control.Monad.Elin`.
  
  Most of the time, however, we are interested in streams that produce
  arbitrary side-effects, and an I/O monad such as `IO.Async` is required.
  
  A note on totality: Theoretically, we should be able define `Bind` as follows:
  
  ```idris
  Bind : Pull f o es r -> Inf (r -> Pull f o es s) -> Pull f o es s
  ```
  
  This would allow us to safely generate total, infinite streams of output
  and only running a `Pull` would be a non-total function. In practice, however,
  I found this approach to have various shortcomings: We'd need a custom
  bind operator for defining infinite pulls. That's not hard to implement, but
  I found it to be fairly limited and cumbersome to use, especially since
  type inference got very erratic. For the time being, I therefore decided
  to resort to `assert_total` when defining potentially infinite streams.
  It's not pretty, but it gets the job done.

Totality: total
Visibility: export
Constructors:

Val : r -> Pull f o es r

  Constructor for producing value of type `r`

Err : HSum es -> Pull f o es r

  Constructor for failing with an exception

Cons : o -> Inf (Pull f o es r) -> Pull f o es r

  Constructor for producing a chunk of output values

Act : Action f es r -> Pull f o es r

  Wraps an arbitrary effectful computation in a `Pull`

Uncons : Pull f o es r -> Pull f q es (Either r (o, Pull f o es r))

  Unwraps the given child `Pull` until it either produces
  a result or a chunk of output.

Att : Pull f o es r -> Pull f o fs (Result es r)

  Attempts to evaluate the underlying `Pull`, returning any error
  wrapped in a `Left` and a successful result in a `Right`. This is
  the primitive used for error handling.

Bind : Pull f o es r -> (r -> Pull f o es t) -> Pull f o es t

  Sequencing of `Pull`s via monadic bind `(>>=)`.

OScope : Interrupt f -> Pull f o es r -> Pull f o es r

  Runs the given `Pull` in a new child scope. The optional second argument
  is used to check, if the scope has been interrupted.

GScope : Pull f o es (Scope f)

  Internal: A pull for returning the current scope

IScope : Scope f -> Bool -> Pull f o es r -> Pull f o es r

  Internal: Forces the given pull to be evaluated in the given scope.
  
  This is used when evaluating pulls in parallel (for instance, when zipping
  or merging streams): Both pulls must be run in the outer scope to prevent
  the resources of the second pull to be release early when the first once
  is exhausted. See `stepLeg` and `StepLeg`.

OnIntr : Pull f o es r -> Lazy (Pull f o es r) -> Pull f o es r

  Continues with the second pull in case the first is interrupted.

Hints:

ELift1 s f => ELift1 s (Pull f o)

HasIO (f es) => HasIO (Pull f o es)

MErr (Pull f o)

0 Stream : (List Type -> Type -> Type) -> List Type -> Type -> Type

  Alias for a `Pull` with a trivial return type.

Totality: total
Visibility: public export

0 EmptyPull : (List Type -> Type -> Type) -> List Type -> Type -> Type

  Alias for a `Pull` that cannot produce any output.

Totality: total
Visibility: public export

0 EmptyStream : (List Type -> Type -> Type) -> List Type -> Type

  Alias for a `Pull` that cannot produce any output.

Totality: total
Visibility: public export

record StepLeg : (List Type -> Type -> Type) -> List Type -> Type -> Type

  A (partially evaluated) `Pull` plus the scope it should be
  evaluated in.

Totality: total
Visibility: public export
Constructor: 

SL : o -> Pull f o es () -> Scope f -> StepLeg f es o

Projections:

.out : StepLeg f es o -> o

.pull : StepLeg f es o -> Pull f o es ()

.scope : StepLeg f es o -> Scope f

.out : StepLeg f es o -> o

Totality: total
Visibility: public export

out : StepLeg f es o -> o

Totality: total
Visibility: public export

.pull : StepLeg f es o -> Pull f o es ()

Totality: total
Visibility: public export

pull : StepLeg f es o -> Pull f o es ()

Totality: total
Visibility: public export

.scope : StepLeg f es o -> Scope f

Totality: total
Visibility: public export

scope : StepLeg f es o -> Scope f

Totality: total
Visibility: public export

exec : f es r -> Pull f o es r

  Lifts the given effectful computation into a `Pull`.

Totality: total
Visibility: export

acquire : f es r -> (r -> f [] ()) -> Pull f o es r

  Acquires a resource that will be released once the current
  scope is cleaned up.

Totality: total
Visibility: export

cons : o -> Inf (Pull f o es r) -> Pull f o es r

  Prepends the given output to a pull.

Totality: total
Visibility: export

emit : o -> Stream f es o

  Emits a single chunk of output.

Totality: total
Visibility: export

uncons : Pull f o es r -> Pull f q es (Either r (o, Pull f o es r))

  Unwraps a `pull` either returning its final result or
  its first output together with the remainder of the pull.

Totality: total
Visibility: export

scope : Pull f o es (Scope f)

  Returns the current evaluation scope.
  
  This is an internal primitive that can be used to implement
  new combinators and topologies.

Totality: total
Visibility: export

newScope : Pull f o es r -> Pull f o es r

  Creates a new scope for running the given `Pull` in

Totality: total
Visibility: export

inScope : Scope f -> Pull f o es r -> Pull f o es r

  Forces the given `Pull` to be evaluated in the given scope.
  
  This is an internal primitive that can be used to implement
  new combinators and topologies.

Totality: total
Visibility: export

att : Pull f o es r -> Pull f o fs (Result es r)

  Error handling primitive: Wraps a successful result in a `Right`
  and an error in a `Left`.

Totality: total
Visibility: export

interruptOn : Deferred World (Result es ()) -> Stream (Async e) es o -> Stream (Async e) es o

  Runs the given pull in a new child scope and interrupts
  its evaluation once the given `Deferred` is completed.

Totality: total
Visibility: export

interruptOnAny : Deferred World a -> Stream (Async e) es o -> Stream (Async e) es o

  Runs the given pull in a new child scope and interrupts
  its evaluation once the given `Deferred` is completed.

Totality: total
Visibility: export

pull : MCancel f => Target s f => Pull f Void es r -> f [] (Outcome es r)

  Runs a `Pull` to completion, eventually producing
  a value of type `r`.
  
  Note: In case of an infinite stream, this will loop forever.
        In order to cancel the evaluation, consider using
        `Async` and racing it with a cancelation thread (for instance,
        by waiting for an operating system signal).

Visibility: export

mpull : MCancel f => Target s f => Monoid r => Pull f Void [] r -> f [] r

  Like `pull` but without the possibility of failure. Returns `neutral`
  in case the stream was interrupted.

Visibility: export

pullIn : Scope f -> Pull f Void es r -> f [] (Outcome es r)

  Runs a Pull to completion in the given scope, without
  closing the scope. Use this when the pull was generated from
  an outer scope that is still in use.

Visibility: export