custodian

Custodians, as Racket has them: a custodian has things in its custody — what a with holds — what ends a thing given to it, and the custodians made under it, and shutdown ends all of it at once. A custodian is the runtime’s object, as a thing a with holds is: the program holds it as a value, and it lives as long as the program can reach it, or a thing in its custody lives.

A with lets go of its hold when its body ends; where nothing else holds the thing — no thread it was given to — it is ended there, else it is ended when the last holder lets go of it (resource’s scoped). A with whose thing is let go of by a computation (resource’s held) is the special case whose policy is to release as its block is left. Either way the thing is in the custody of the custodian current: the one whose with the with is in, as Racket’s parameterize has it, or the root’s, outside every one. The custodian current is the runtime’s to carry, as Reader carries its value: a with of a custodian adds no effect to its body’s world, and what starts to run later — a continuation, a domain, a cml thread — keeps the one current where it was started.

import bytes as Bytes
import co
import custodian as Custodian
import exception
import resource
import std.net as Net

-- | each connection in a custodian of its own, which contains its
-- | failures: one that fails to close takes down its custodian alone
served : {e : HFunctor}
       -> {s : Type}
       -> {{nt : Net.net <: e}}
       -> {{cu : Custodian.custodian <: e}}
       -> {{ex : exception Net.NetError <: e}}
       -> With s Net.TcpListener
       -> Co e Unit
served l = do
  with k := Custodian.contained do
    with Net.accept l as c do
      _ <- Net.write c (Bytes.fromString "hello")
      pure ()
  served l

Operation	What it does
with k := custody do	the body run with k a custodian under the one the with is in; the things its withs hold in k’s custody
with k := contained do	the same, k containing its failures
make	a custodian, under the one it is made in
under c	a custodian under c: shut down with it
manage c stop	stop given to c, to run at its shutdown; False where c is shut down already, stop not kept
shutdown c	the things in c’s custody ended, every stop given to it run, once, in the order given, then those of the custodians under it; why each stop that failed did

A custodian manages no thread: a thread that took a thing in its custody finds the thing ended at its next operation on it (a socket’s EBADF), and is the one to deal with that.

A thing that fails to end — its with ending it, its last holder, or its custodian’s shutdown — is a failure of its custodian’s, never thrown to the with’s caller. The custodian is shut down, with those under it, and the failure goes to the one it is under; one made by contained says it and goes no further, the program going on; at the root, the failure is the program’s: said, and the program ended. A release run after its block was left (held’s) that fails is the same.

What a custodian is given is a computation, higher-order: it is of the world it was given in, the handlers between there and the program’s top level handled where it was given, and it runs where the shutdown is, after their scope may have ended — or, where a failure shut it down, on the domain that made the custodian, at its next operation. A handler that cannot let a computation out of its scope says so as it runs: attempt turns a throw that leaves one into abandon, which the shutdown then says in the list it comes to.

A custodian the program no longer reaches, and no thing in its custody holds, is let go of by the runtime: what it was given is dropped, not run, and what that kept alive is let go of as the program’s other values are — at once on the C backend, by the count of references, and whenever JavaScript’s collector comes to it in a page. A custodian under another is held by its parent: it lives as long as its parent does, unless the program holds it longer; where it outlives its parent, its failures go where its parent’s would.

Custodian

data Custodian

A custodian: the runtime’s object.

Ticket

data Ticket

A release the program’s top level keeps for a with (resource’s held): the runtime’s object, dropped by the with as its block is left, the release then run there. (Unkept is untended’s: kept by none.)

Owned

data Owned a = MkOwned a

A thing a with holds, of whatever type, given to a custodian.

Running

data Running (m : Type -> Type) x a = MkRunning (m a) (a -> x)

A computation run with a custodian current, and what comes after.

Asking

data Asking x
  = Made (Maybe Custodian) Bool (Custodian -> x)
  | ShutDown Custodian (List String -> x)
  | Dropped Ticket x
  | Own (Some Owned) x
  | Failed String x
  | Current (Maybe Custodian -> x)

The custodians’ operations that are given no computation: one made, under another — Nothing, the one current — and whether a failure stops at it; one shut down, why each stop that failed did; a release kept dropped; a thing a with holds given the one current; a failure of the one current’s, why said; and which one is current, Nothing the root’s.

Giving

data Giving (m : Type -> Type) x
  = Managed Custodian (Unit -> m Unit) (Bool -> x)
  | Kept (Unit -> m Unit) (Ticket -> x)
  | Under Custodian (Some (Running m x))

The custodians’ operations given a computation — a function of Unit, computed only where it is run, so that a handler between maps it without computing it: something given one, to run at its shutdown, False where it is shut down already; a release kept for a with, by the one current; and a computation run with one current, as Reader’s local runs one.

CustodianF

data CustodianF (m : Type -> Type) x = Asked (Asking x) | Given (Giving m x)

The custodians’ operations: those given no computation, and those given one. (Two kinds, so that a handler maps an operation by looking at two cases, its computations only where there are some.)

custodianThen

custodianThen : {m : Type -> Type}
              -> {x y : Type}
              -> (x -> y)
              -> CustodianF m x
              -> CustodianF m y

What comes after an operation, changed.

custodianBy

custodianBy : {m : Type -> Type}
            -> {n : Type -> Type}
            -> {x : Type}
            -> ({t : Type} -> m t -> n t)
            -> CustodianF m x
            -> CustodianF n x

What is given to run, put in another monad.

custodian

custodian : HFunctor

Custodians, the runtime’s: a provider at the program’s top level.

make

make : {e : HFunctor} -> {{cu : custodian <: e}} -> Co e Custodian

A custodian, under the one current: the root’s, outside every with of a custodian.

under

under : {e : HFunctor} -> {{cu : custodian <: e}} -> Custodian -> Co e Custodian

A custodian managed by parent: shut down with it.

manage

manage : {e : HFunctor}
       -> {{cu : custodian <: e}}
       -> Custodian
       -> Co e Unit
       -> Co e Bool

stop given to the custodian, to run at its shutdown, once: True; False where it is shut down already, stop not kept (to run otherwise, if the program will).

shutdown

shutdown : {e : HFunctor}
         -> {{cu : custodian <: e}}
         -> Custodian
         -> Co e (List String)

Everything given to the custodian run, once, in the order given, the things in its custody ended, then the custodians under it shut down too: why each stop that failed did. A thing that fails to end is a failure of the custodian’s. Shut down again, nothing is run; given more after, it is not kept.

owned

owned : {e : HFunctor}
      -> {{cu : custodian <: e}}
      -> {a : Type}
      -> a
      -> Co e Unit

x, a thing a with holds, in the custody of the custodian current: it is ended as that one is shut down, and a failure to end it is that one’s. (resource’s scoped gives it.)

failed

failed : {e : HFunctor} -> {{cu : custodian <: e}} -> String -> Co e Unit

A thing in the custody of the custodian current failed to end, as why says: the failure of that custodian’s. It is shut down, and the failure passed to the one it is under; one made to contain its failures says it there and goes no further, and the root says it, the program ended.

current

current : {e : HFunctor} -> {{cu : custodian <: e}} -> Co e (Maybe Custodian)

The custodian current: Nothing, the root’s.

custodied

custodied : {e : HFunctor}
          -> {a : Type}
          -> {{cu : custodian <: e}}
          -> Custodian
          -> Co e a
          -> Co e a

c run with k the custodian current, and after it the one current before: Racket’s parameterize of the current custodian, as Reader’s local is, by the handler of the one custodian — the runtime’s — not a variable. What c leaves to run later (a continuation kept, a thread or a domain started) keeps k.

kept

kept : {e : HFunctor} -> {{cu : custodian <: e}} -> Co e Unit -> Co e Ticket

release kept by the program’s top level, as a with enters its block: a computation of the world it is given in, the handlers between there and the top level as they are then. Dropped by the with as its block is left (dropped), it is never run by the runtime. Where the block is left otherwise — a throw heard outside it, a handler between that drops the continuation — the ticket goes with what held it, and the runtime runs the release then: at the next operation of the domain that kept it, on the C backend as the count of its references comes to none, in JavaScript as the collector comes to it. A release that fails there is a failure of the custodian whose custody the with was in.

dropped

dropped : {e : HFunctor} -> {{cu : custodian <: e}} -> Ticket -> Co e Unit

The release kept dropped, not run: the with’s block left as it was to be.

Custody

data Custody

What a with k := custody do makes: a custodian, which the things its body’s withs hold are in the custody of; True, one whose failures stop at it.

custody

custody : Custody

with k := custody do ss: ss run with k a custodian made under the one the with is in the custody of (the root’s, outside every other), and the things the withs in ss hold in its custody, the custodians made there under it. A failure of k’s passes on to the one it is under.

contained

contained : Custody

with k := contained do ss: as custody, but a failure of k’s goes no further: k is shut down, the failure said, and the program goes on.

instanceBinderCustody

instance instanceBinderCustody : Binder Custody

A with of a custodian: its name the custodian, its body in the world of the block around, and the with comes to what the body came to.

instanceHolderCustody

instance instanceHolderCustody : {e : HFunctor}
                               -> {{cu : custodian <: e}}
                               -> Holder
                                 e
                                 Custody
                                 (\s -> Custodian)
                                 (\w -> w)
                                 (\r -> r)

A custodian held by a with: made, and the body run with it the custodian current (custodied). It is not shut down as the body ends: the things in its custody are let go of by their own withs; the body shuts it down where it will (shutdown k), and a failure does.

untended

untended : {e : HFunctor} -> {a : Type} -> Co (custodian <+> e) a -> Co e a

c, its withs’ releases kept by none, for a world with no runtime under it (an interpreter’s, a handler’s own): each run as its block is left, one whose block a throw leaves lost; a release that fails, the program’s failure, an abandon.