FS.Scope

Definitions

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

  An interruption handler.
  
  This is used for cross-stream interruption when running streams in
  parallel. For instance, when nondeterministically merging two streams
  A and B (see `FS.Concurrent.merge`), A and B will be run in parallel
  each on its own fiber. Both should be interrupted if downstream terminates,
  for instance because the number of emitted values have been limited via
  a call to `take`.
  
  Implementation detail: When running a stream, we check on each iteration
  whether the current scope has been interrupted or not. In addition, in
  case of wrapped effectful computations - which might be potentially long
  running (think of a timer or waiting for a connection or a mouse click) -
  the wrapped effect is raced against the stream being interrupted.

Totality: total
Visibility: public export
Constructors:

None : Interrupt f

I : Deferred World a -> Interrupt (Async e)

interface Target : Type -> (List Type -> Type -> Type) -> Type

  Target effect of stream compilation.
  
  Effect type `f` (of type `List Type -> Type -> Type`) can be used to
  run (= evaluate) streams in state thread `s`.
  Currently, this is either `Elin s` for running synchronous streams in state
  effect `s`, or `Async e` for running streams concurrently.
  
  If `s` is universally quantified, `Elin s` streams can be converted to pure
  functions making use of local mutable state, resource management, and error
  handling. If `s` equals `World`, `Elin World` can be used as a regular
  (synchronous) monad with error handling.

Parameters: s, f
Constraints: ELift1 s f
Methods:

combineInterrupts : Interrupt f -> Interrupt f -> F1 s (Interrupt f, List (f [] ()))

  Combines two interruption handlers

isInterrupted : Interrupt f -> f [] Bool

  Returns `True` if the stream has been interrupted.

raceInterrupt : Interrupt f -> f es a -> f [] (Outcome es a)

  Races an effectful computation against stream interruption

Implementations:

Target s (Elin s)

Target World (Async e)

combineInterrupts : Target s f => Interrupt f -> Interrupt f -> F1 s (Interrupt f, List (f [] ()))

  Combines two interruption handlers

Totality: total
Visibility: public export

isInterrupted : Target s f => Interrupt f -> f [] Bool

  Returns `True` if the stream has been interrupted.

Totality: total
Visibility: public export

raceInterrupt : Target s f => Interrupt f -> f es a -> f [] (Outcome es a)

  Races an effectful computation against stream interruption

Totality: total
Visibility: public export

record ScopeID : Type

  IDs for comparing and ordering scopes. This is for internal
  use only. In particular, looking at the internal representation
  of a `ScopeID` via `Show` is *not* referentially transparent and
  should be used for debugging purposes only.

Totality: total
Visibility: export
Constructor: 

SID : Nat -> ScopeID

Projection: 

.val : ScopeID -> Nat

Hints:

Eq ScopeID

Ord ScopeID

Show ScopeID

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

  State of scopes of a running stream.

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

  Cancelation scopes
  
  Functional streams are evaluated in scopes, which are organized as
  a tree, just like stream evaluation can be thought of as a tree:
  Sequencing of streams means nesting in the resulting scope tree,
  while parallel evaluation (for instance, when zipping or merging
  streams) means branching. Once a stream is exhausted,
  it's scope is cleaned up and all resources allocated in this scope
  are released, including the resources of all child scope.
  
  In addition to (internal) cancelation, streams can be run concurrently,
  in which case the can be interrupted by an external event such as
  the exhaustion of a timer or the termination of another stream.
  At every evaluation step of a stream we check, if the current scope
  has been canceled. If this is the case, evaluation of the stream
  is aborted.
  
  Just like `Pull`s and `Stream`s, a `Scope` is parameterized by its
  effect type.

Totality: total
Visibility: public export
Constructor: 

S : ScopeID -> ScopeID -> List ScopeID -> Interrupt f -> Ref tstate (ScopeST f) -> Target tstate f => Scope f

Projections:

.ancestors : Scope f -> List ScopeID

  parent scopes `([parent, grand-parent, ... , root])`

.id : Scope f -> ScopeID

  this scope's unique identifier

.interrupt : Scope f -> Interrupt f

  Handler to check for stream interruption

.root : Scope f -> ScopeID

  ID of this scope's root scope

.state : ({rec:0} : Scope f) -> Ref (tstate {rec:0}) (ScopeST f)

.tgt : ({rec:0} : Scope f) -> Target (tstate {rec:0}) f

0 .tstate : Scope f -> Type

Hint: 

Interpolation (Scope f)

0 .tstate : Scope f -> Type

Totality: total
Visibility: public export

0 tstate : Scope f -> Type

Totality: total
Visibility: public export

.id : Scope f -> ScopeID

  this scope's unique identifier

Totality: total
Visibility: public export

id : Scope f -> ScopeID

  this scope's unique identifier

Totality: total
Visibility: public export

.root : Scope f -> ScopeID

  ID of this scope's root scope

Totality: total
Visibility: public export

root : Scope f -> ScopeID

  ID of this scope's root scope

Totality: total
Visibility: public export

.ancestors : Scope f -> List ScopeID

  parent scopes `([parent, grand-parent, ... , root])`

Totality: total
Visibility: public export

ancestors : Scope f -> List ScopeID

  parent scopes `([parent, grand-parent, ... , root])`

Totality: total
Visibility: public export

.interrupt : Scope f -> Interrupt f

  Handler to check for stream interruption

Totality: total
Visibility: public export

interrupt : Scope f -> Interrupt f

  Handler to check for stream interruption

Totality: total
Visibility: public export

.state : ({rec:0} : Scope f) -> Ref (tstate {rec:0}) (ScopeST f)

Totality: total
Visibility: public export

state : ({rec:0} : Scope f) -> Ref (tstate {rec:0}) (ScopeST f)

Totality: total
Visibility: public export

.tgt : ({rec:0} : Scope f) -> Target (tstate {rec:0}) f

Totality: total
Visibility: public export

tgt : ({rec:0} : Scope f) -> Target (tstate {rec:0}) f

Totality: total
Visibility: public export

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

Totality: total
Visibility: export
Constructor: 

N : Scope f -> List (Hook f) -> SortedSet ScopeID -> Node f

Projections:

.children : Node f -> SortedSet ScopeID

  list of child scopes

.cleanup : Node f -> List (Hook f)

  optional cleanup hook for a resource allocated in this scope

.scope : Node f -> Scope f

  The immutable scope state.

openScope : Target s f => STRef s f -> Interrupt f -> Scope f -> F1 s (Scope f)

  Opens and returns a new child scope for the given parent
  scope.
  
  If the parent scope has already been closed, its closest
  open ancestor will be used as the new scope's parent instead.

Totality: total
Visibility: export

addHook : Scope f -> f [] () -> f [] ()

  Adds a new cleanup hook to the given scope or its closest
  open parent scope.

Totality: total
Visibility: export

close : Target s f => STRef s f -> Bool -> ScopeID -> f [] ()

  Closes the scope of the given ID plus all its child scopes,
  releasing all allocated resources in reverse order of allocation
  along the way.

Totality: total
Visibility: export

lease : Scope f -> f [] (f [] ())

  Leases all cleanup hooks from this scope as well as its direct
  children and ancestors.
  
  Invoke the given action to release them again.

Totality: total
Visibility: export

newScope : Target s f => f [] (Scope f)

  Creates a new root scope and returns it together with the set of
  scopes for the given effect type.

Totality: total
Visibility: export

printScope : Scope f -> String

Totality: total
Visibility: export

logScope : HasIO (f es) => String -> Scope f -> f es ()

Totality: total
Visibility: export