std.reactor

For outside operations begun now and finished later: what lets a scheduler’s threads go on while one of them waits on a socket, a name being resolved or an HTTP request. The C backend’s alone (its provider, and the runtime’s reactor): a page’s providers do not wait. Import it by a name, import std.reactor as Reactor. A scheduler waits on the world through it — cml’s scheduledWithReactor — and so does a program that starts several operations itself.

import std.reactor as Reactor
import std.duration as Duration
import std.time as Time

-- | three sleeps begun at once, waited for together: in about 100 ms
slept : {e : HFunctor} -> {{rx : Reactor.reactor <: e}} -> {{tm : Time.time <: e}} -> Co e Int
slept = do
  g <- Reactor.open
  _ <- Reactor.start g (bind (Time.sleep (Duration.milliseconds 100)) (\u -> pure 1))
  _ <- Reactor.start g (bind (Time.sleep (Duration.milliseconds 100)) (\u -> pure 2))
  _ <- Reactor.start g (bind (Time.sleep (Duration.milliseconds 100)) (\u -> pure 3))
  a <- Reactor.finished g True
  b <- Reactor.finished g True
  c <- Reactor.finished g True
  Reactor.close g
  pure (List.sum (a ++ b ++ c))

These wait in the reactor, where they are started in a group:

std.net’s read, write, accept and withConnection;
std.filesystem’s reads and writes of a pipe, a terminal or a socket;
std.process’s wait, and reads and writes of a command’s pipes;
std.http’s requests;
std.time’s sleep;
std.signal’s wait.

A regular file is read and written at once, the program waiting.

A group is opened, on a domain; each computation started in it — one of the world, run there until it is done or until an operation of these would wait, which is then pending, the rest of the computation kept with it — and the group asked which of those pending are finished, each its computation’s value, run to its end once its operation was done. finished g True waits for the first to finish, in one poll, or until another domain wakes it (wake). A group within another (openWithin) is pending and finishes among the other’s, and is closed apart, what is pending in it let go of. Where no group is being started in, an operation waits where it is, the whole program with it. Each thread of the system has its own reactor: a group is its domain’s, started in, asked and closed there alone, but woken from any.

A group within another is given up from any domain by what giving makes for it, a thing a custodian can have in its custody (Custodian.owned): ended — by the custodian’s shutdown, or as the program lets go of it — the group’s domain gives the group up at its next look at its finished: what of it is pending let go of, undone (a socket’s watch, a sleep’s timer, a signal’s or a command’s wait taken out), and the value giving was given finished in its place; where none of it is pending, closed alone. What a scheduler gives up by it is what has no use any more — an act awaited in a custody shut down — never what a thread or a behaviour is in the middle of.

A computation is started between a Begin and an End of its group, in the world’s own course, not held by an operation: a handler between the scheduler and the world — a state — sees what it does as it sees any other operation, and keeps it.

Group

data Group t = MkGroup Int

A group of computations started, each of which comes to a t.

Giving

data Giving

What gives up a group within another, from any domain: the runtime’s object.

Ending

type Ending x = (r : Type) -> ((t : Type) -> t -> (Maybe t -> x) -> r) -> r

A computation started come to its end: its value, given to what comes after its start, whatever it is.

Finished

type Finished x = (r : Type) -> ((t : Type) -> (List t -> x) -> r) -> r

What a group’s finished are given to, whatever they are.

endingWith

endingWith : {t x : Type} -> t -> (Maybe t -> x) -> Ending x

finishedWith

finishedWith : {t x : Type} -> (List t -> x) -> Finished x

ReactorF

data ReactorF (m : Type -> Type) x
  = Open (Maybe ((r : Type) -> ((t : Type) -> (String -> t) -> r) -> r)) (Int
                                                                          -> x)
  | Begin Int (Bool -> x)
  | End Int (Ending x)
  | Finish Int Bool (Finished x)
  | Close Int x
  | Within Int (Int -> x)
  | Wake Int x
  | Pending Int (Int -> x)
  | MakeGiving Int ((r : Type) -> ((t : Type) -> t -> r) -> r) (Giving -> x)
  | CloseGiving Giving x

reactor

reactor : HFunctor

For host operations begun now and finished later (a transfer, a socket readable): a group opened, operations begun in it and ended, a wait for one to finish, the group closed.

open

open : {e : HFunctor}
     -> {{rx : reactor <: e}}
     -> {t : Type}
     -> {failed : Maybe (String -> t) := Nothing}
     -> Co e (Group t)

A group of its own. failed, where it is given, is what a computation started in it that fails — abandons, or fails in the runtime — comes to, given why, among the group’s finished, the others going on; where it is not, the failure is the program’s.

start

start : {e : HFunctor}
      -> {{rx : reactor <: e}}
      -> {t : Type}
      -> Group t
      -> Co e t
      -> Co e (Maybe t)

c started in the group: run until it is done, Just its value; or until an operation of it would wait, Nothing, its value to be one of the group’s finished. Begun (True), c is run, and ended with its value; where it waits, its start is told so (False), and what comes after its wait is run once that is done, up to its end, its value then one of the group’s finished.

finished

finished : {e : HFunctor}
         -> {{rx : reactor <: e}}
         -> {t : Type}
         -> Group t
         -> Bool
         -> Co e (List t)

The group’s computations finished since it was last asked, in the order they were: where wait, waiting for one at least, while any of it is pending, or until the group is woken (wake); none where none is.

close

close : {e : HFunctor}
      -> {{rx : reactor <: e}}
      -> {t : Type}
      -> Group t
      -> Co e Unit

The group closed: what of it is pending let go of, undone — a socket being connected closed, a request let go of — and what of it is finished and not asked for.

openWithin

openWithin : {e : HFunctor}
           -> {{rx : reactor <: e}}
           -> {t : Type}
           -> Group t
           -> Co e (Group t)

A group within g, of the same domain: what is started in it is among g’s pending, and finishes among g’s finished; closed, what of it is pending is let go of, undone, and g stays open. So one of a group’s computations started is let go of alone, in a group of its own within it.

pending

pending : {e : HFunctor}
        -> {{rx : reactor <: e}}
        -> {t : Type}
        -> Group t
        -> Co e Int

How many of the group’s computations started are pending now: of the groups within it too.

wake

wake : {e : HFunctor}
     -> {{rx : reactor <: e}}
     -> {t : Type}
     -> Group t
     -> Co e Unit

The domain asking for the group’s finished woken, from any domain: its finished, waiting, comes back — with none, where none has finished — and where it is not waiting now, its next does, at once. A group’s number is no other domain’s, so the right one is woken; one closed is woken no more, nor one within another: its root is.

giving

giving : {e : HFunctor}
       -> {{rx : reactor <: e}}
       -> {t : Type}
       -> Group t
       -> t
       -> Co e Giving

What gives up g, a group within another, from any domain: ended — in a custodian’s custody, by its shutdown; or as the program lets go of it — the domain of g gives it up at its next look at its root’s finished: where any of it is pending then, it is closed, what is pending let go of, undone, and gave is among the root’s finished in its place; where none is, it is closed alone. So what counts what was started knows each is done, given up or not. A group closed is given up no more: closeGiving closes it, where it is done with, before the program lets go of what gives it up.

closeGiving

closeGiving : {e : HFunctor} -> {{rx : reactor <: e}} -> Giving -> Co e Unit

The group gv gives up closed, on its domain, as close closes it: given up no more.