resource

A host’s thing held by a with, the same for every effect: an open file, a socket, a process, a canvas — what must be let go of. Each has its own with: withProcess, Net.withConnection, std.file’s with f := File.open path do, and so on. In a do block a with is a statement, with withProcess c as p do, the statements under it its body. Each one:

1. acquires the thing;
2. runs the body with it (scoped’s, a With s r in a region s of its own);
3. lets go of it when the body ends;
4. comes to what the body came to.

The thing lives as long as the program can reach it, in the custody of a custodian (the custodian module): the one whose with of a custodian the with is in, or the root’s. Letting go of it, a with ends it there where it held it alone; where the body gave it to another — a thread spawned in the body, given the With s r by value — it is ended once the last holder lets go of it, the with not waiting. That is scoped’s policy. A thing let go of by a computation of the program’s, a held’s, has the other: it is let go of as the block is left, whoever holds it still.

import co
import exception
import std.process

ran : {e : HFunctor}
    -> {{sys : process <: e}}
    -> {{fx : exception ProcessError <: e}}
    -> Invocation
    -> Co e Ran
ran c = do
  with withProcess c as p do
    wait p

The body is polymorphic in s, and what it comes to is of a type bound outside it, so a With s r cannot leave the body: withProcess c (\p -> val p) is a type error (E0311).

There is one With for every effect, so a with of one effect may hand its thing to an operation of another by value — a <canvas> found by browser.dom, drawn on by browser.gpu — and neither keeps it.

A with comes to what its body came to, and nothing else: a thing not acquired is no answer of the body’s, so it is thrown, over the exception effect, the body not run — a with asks for exception err besides its own effect, and try can catch it. A release that fails is no answer of the body’s either, nor the caller’s to catch: it is a failure of the thing’s custodian’s, whether the with ended the thing or its last holder did, later — the custodian shut down, and the failure passed up, at the root the program’s, said, and the program ended. So a with asks for custodian too. held is the with of a thing that is always had and let go of by a computation — a port of a standard stream, a handle on the page’s document — which throws nothing; its release is kept by the program’s top level meanwhile, and runs however the block is left.

The thing is the host’s own, a foreign value with a finalizer, so a body left otherwise — a throw heard outside it, a handler between that drops the continuation — lets go of it where the program drops its last reference to it; scoped adds nothing for that.

With is exposed without its tag: no program makes one, and scoped acquire release body and held acquire release body are the only ways to make one in a region of its own; beside w x has x in the region w’s thing is had in, as std.net’s accepted has a connection in its listener’s. A library wraps one around its own operations acquiring and releasing the thing, as std.process does:

withProcess : {e : HFunctor} -> {a : Type} -> {{ev : process <: e}}
            -> {{ex : exception ProcessError <: e}}
            -> Invocation
            -> ({s : Type} -> With s Started -> Co e a)
            -> Co e a
withProcess c body = scoped (op (ev (Start (spawnOf c) (\s -> s))) val)
                            (\s -> op (ev (Release s (\r -> r))) val) body

wait : {e : HFunctor} -> {s : Type} -> {{ev : process <: e}}
     -> With s Started -> Co e Ran
wait p = op (ev (Wait (inside p) (\r -> r))) val

• Its operations take the With s a, and give the thing to a provider operation by inside, which takes it out for that operation and nothing else.
• It may export its bare acquire and release too, as std.file does (open, close; its with of a binding, with f := File.open path do, is scoped around them, its body given the file itself): where the provider lets go of a thing once, an operation on it after is the effect’s error (a file’s, EBADF), never one on a thing acquired since, and its operations then take the thing itself.
• What lives as long as the program, such as a GPU device, is held by a with at the top of main.

The provider’s side, how it opens and closes the thing, is its scoped operations.

With

data With s a

A host’s thing, held in the region s by a with (scoped, held).

inside

inside : {s a : Type} -> With s a -> a

The thing a with holds, for a provider operation given it: a library’s operation on a With s a takes it out here and gives it to the operation, and nothing else does.

beside

beside : {s a b : Type} -> With s a -> b -> With s b

A thing had in the region s that w’s thing is had in: for a thing a library gets by another’s — a connection by its listener — which lives no longer than that one’s with, and is let go of by the library’s own operation, or by the program dropping it.

scoped

scoped : {e : HFunctor}
       -> {err r a : Type}
       -> {{ex : exception err <: e}}
       -> {{cu : Custodian.custodian <: e}}
       -> {{sh : Show err}}
       -> Co e (Either err r)
       -> (r -> Co e (Either err Unit))
       -> ({s : Type} -> With s r -> Co e a)
       -> Co e a

The thing acquire gives, held by body in a region of its own — it is not kept past it — and let go of by release when body ends: what it came to. release is the with letting go of its hold, the provider’s to say: it ends the thing where the with held it alone, and else leaves it to the last holder, ended as that one lets go of it — a thread the body gave it to. The thing is in the custody of the custodian whose custody the with is in (the custodian module’s custody; the root’s, outside every one). A thing not acquired is thrown, the body not run. One not released, whenever it is ended — release coming to a Left, or its provider failing to end it later — is that custodian’s failure, said as show says the Left: never thrown to the caller. Should body be left otherwise — a throw heard outside it, a handler between that drops the continuation — the thing is let go of where the program drops its last reference to it, as its provider says.

held

held : {e : HFunctor}
     -> {r a : Type}
     -> {{cu : Custodian.custodian <: e}}
     -> Co e r
     -> (r -> Co e Unit)
     -> ({s : Type} -> With s r -> Co e a)
     -> Co e a

The thing acquire gives, which it always does, held by body in a region of its own and let go of by release as the block is left, whoever holds it still: what the body came to. The release is a computation, kept meanwhile by the program’s top level (the custodian’s kept): where the block is left otherwise — a throw heard outside it, a handler between that drops the continuation — the runtime runs it once that is known, at the next operation of the domain that kept it (C), or as the collector comes to it (JavaScript). The with of a port of a standard stream, or of the page’s document.

had

had : {e : HFunctor}
    -> {r a : Type}
    -> r
    -> ({s : Type} -> With s r -> Co e a)
    -> Co e a

x, held by body in a region of its own, nothing done as it ends: for a library whose thing is let go of otherwise, after the body, by an operation of its own.