Data.Linear.Sink

Reexports

Definitions

record Sink : Type -> Type

  A `Sink` is a primitive consumer of values.

Totality: total
Visibility: public export
Constructor: 

S : (o -> IO1 ()) -> Sink o

Projection: 

.sink1 : Sink o -> o -> IO1 ()

Hints:

Contravariant Sink

Monoid (Sink a)

Semigroup (Sink a)

.sink1 : Sink o -> o -> IO1 ()

Totality: total
Visibility: public export

sink1 : Sink o -> o -> IO1 ()

Totality: total
Visibility: public export

cmap : (b -> a) -> Sink a -> Sink b

  A `Sink` is a contravariant functor.

Totality: total
Visibility: export

snocSink1 : (0 a : Type) -> IO1 (Sink a, IO1 (List a))

  Create a `Sink` that collects values in a mutable
  reference holding a `SnocList`.
  
  The current content of the sink can be read and cleared
  by invoking the given linear action.
  
  The returned sink is thread-safe: Values from multiple
  threads can be written to it.

Totality: total
Visibility: export

sink : HasIO io => Sink a => a -> io ()

Totality: total
Visibility: export

sinkAs : HasIO io => (0 a : Type) -> Sink a => a -> io ()

Totality: total
Visibility: export

sinkTo : HasIO io => Sink a -> a -> io ()

Totality: total
Visibility: export

onceSink : Once World t -> Sink t

Totality: total
Visibility: export

deferredSink : Deferred World t -> Sink t

Totality: total
Visibility: export