Idris2Doc : System.Concurrency.Linear

System.Concurrency.Linear

Definitions

fork1 : L IO () -@ L IO ThreadID
  Run a linear computation in a separate thread

Visibility: export
concurrently : L IO a -@ L1 IO (L IO a)
  Run a computation concurrently to the current thread.
This returns a receiver for the value.

Visibility: export
concurrently1 : L1 IO a -@ L1 IO (L1 IO a)
  Run a computation concurrently to the current thread.
This returns a receiver for the value. A typical usage
pattern is showcased by the implementation of `par1`:
in a do block start executing a series of actions
concurrently and then collect the results with a series
of receiving steps.

do recva <- concurrently1 ioa
recvb <- concurrently1 iob
a <- recva
b <- recvb
pure1 (a # b)

Visibility: export
par1 : L1 IO a -@ (L1 IO b -@ L1 IO (LPair a b))
  Run two linear computations concurrently and return the results.

Visibility: export
par : L IO a -@ (L IO b -@ L IO (a, b))
  Run two unrestricted computations in parallel and return the results.

Visibility: export