remote

An effect whose operations another program does: an API, shared by a client and a server, each of them a handler of the same effect. The client’s sends each operation, written (wire), through a transport, and goes on with the answer read; the server’s reads it, does it by the effect’s real handler and writes the answer; a test’s does both in one program, the bytes as they would go. Pure, for any backend: the transports are std.remote’s (C: an HTTP server, and a client by std.http) and browser.remote’s (a page’s fetch). Import it by a name, import remote as Remote. heff’s notes example is a page and a server sharing one effect so.

An API is written once, in a module both programs import: its effect, each operation’s index, name and types (operation), and two functions of its constructors — what each called is (call) and how each is served (serve) — which api puts together with the API’s name. Its fingerprint is a hash of the name and of every operation’s index, name and types, as their Wires’ shapes say them: a client and a server of different builds of it are told apart.

A frame is what goes each way, a header and what it carries:

b[“hw”, 1::8, kind::8, fingerprint::32, index::16, n::32, payload::binary-size(n)]

the wire’s version (1), what the frame is (0 a call, 1 its answer, 2 a failure), the API’s fingerprint, the operation’s index (of a failure, why: 1 another API, 2 no such operation, 3 its argument not read, 4 no frame), and the payload: the argument, the answer, or what the server says of the failure, a String as the wire writes it.

Operation

data Operation a b = MkOperation Int String

An operation of an API, as the wire names it: its index among the API’s operations and its name; what it takes, a, and what it gives back, b (a constructor of no argument takes a Unit).

operation

operation : {a b : Type} -> Int -> String -> Operation a b

Call

type Call x = { index : Int, argument : Bytes, answer : Bytes -> Maybe x }

An operation called: its index, its argument written, and its answer read and given to what the operation gives it to.

call

call : {a b x : Type}
     -> {{takes : Wire.Wire a}}
     -> {{gives : Wire.Wire b}}
     -> Operation a b
     -> a
     -> (b -> x)
     -> Call x

The operation o called with arg, its answer given to k (the constructor’s continuation).

Served

type Served x = { index : Int, signature : String, run : Bytes -> Maybe x }

An operation served: its index, its signature (of which the API’s fingerprint is made), and its argument read and made the operation, the answer written.

serve

serve : {a b x : Type}
      -> {{takes : Wire.Wire a}}
      -> {{gives : Wire.Wire b}}
      -> Operation a b
      -> (a -> (b -> Bytes) -> x)
      -> Served x

The operation o served: make is its constructor, given the argument read and what its answer is written by.

Api

theory Api (h : HFunctor) where
  name : String
  fingerprint : Int
  calls : {m : Type -> Type} -> {x : Type} -> h.f m x -> Call x
  serves : {m : Type -> Type} -> List (Served (h.f m Bytes))

An API: the effect h, its name, its fingerprint, each operation as it is called, and each as it is served, whatever computations the effect’s functor holds (none of an API’s operation is sent).

fnv

fnv : String -> Int

A text’s FNV-1a hash, 32 bits.

>>> fnv ""
2166136261
>>> fnv "a"
3826002220

fingerprintOf

fingerprintOf : String -> List String -> Int

An API’s fingerprint: its name and every operation’s signature, one a line, hashed.

api

api : (h : HFunctor)
    -> String
    -> ({m : Type -> Type} -> {x : Type} -> h.f m x -> Call x)
    -> ({m : Type -> Type} -> List (Served (h.f m Bytes)))
    -> Api h

The API of h, named: calls says what each operation called is (call), serves how each is served (serve).

signatures

signatures : {h : HFunctor} -> Api h -> List String

The API’s operations’ signatures, as its fingerprint is made of them.

version

version : Int

The wire’s version, in each frame: a frame of another is refused.

Kind

data Kind = Asked | Answered | Failed

What a frame is: a call, its answer, or a failure.

Frame

type Frame = { kind : Kind, fingerprint : Int, index : Int, payload : Bytes }

A frame read: what it is, the API’s fingerprint, the operation’s index (of a failure, why), and its payload.

frame

frame : Kind -> Int -> Int -> Bytes -> Bytes

A frame written.

>>> frame Asked 1 2 b["x"]
b["hw", 1, 0, 0, 0, 0, 1, 0, 2, 0, 0, 0, 1, "x"]

readFrame

readFrame : Bytes -> Either String Frame

A frame read: what it is, or why it is none.

>>> either (\why -> why) (\(f : Frame) -> show f.payload) (readFrame (frame Answered 7 0 b["ok"]))
"ok"
>>> either (\why -> why) (\(f : Frame) -> "a frame") (readFrame b["hw", 2, 0])
"a frame of the wire's version 2, not 1"

RemoteError

data RemoteError
  = Unreachable String
  | Mismatched String
  | Refused String
  | Malformed String

Why a call came to no answer: no answer came (the transport’s: no connection, a status that is no 200); the server is of another build of the API, or of the wire; it could not read the call (no such operation, its argument); or the answer could not be read.

instanceShowRemoteError

instance instanceShowRemoteError : Show RemoteError

Why, as a line.

named

named : String -> Int -> String

An API’s name and fingerprint, as a failure says them.

saidIn

saidIn : Bytes -> String

Transport

type Transport (e : HFunctor) =
  { exchange : Bytes -> Co e (Either RemoteError Bytes) }

A transport: a frame sent, and the frame that answers it, or why none came (Unreachable). HTTP’s POST is std.remote’s and browser.remote’s; loopback is a server in the same program.

sent

sent : {h : HFunctor}
     -> {e : HFunctor}
     -> {{failed : exception RemoteError <: e}}
     -> Api h
     -> Transport e
     -> {a : Type}
     -> h.f (Co e) a
     -> Co e a

An operation of the API sent by the transport, its answer read; where none came, or it could not be read, a throw of exception RemoteError.

remotely

remotely : {h : HFunctor}
         -> {e : HFunctor}
         -> {{failed : exception RemoteError <: e}}
         -> Api h
         -> Transport e
         -> {a : Type}
         -> Co (h <+> e) a
         -> Co e a

The client: h’s operations, each sent by the transport, the rest of the world done as it is. A call that came to no answer throws RemoteError (exception, in e): recover hears it, and attempt makes one no recover heard Left.

respond

respond : {h : HFunctor}
        -> {e : HFunctor}
        -> Api h
        -> ({a : Type} -> h.f (Co e) a -> Co e a)
        -> Bytes
        -> Co e Bytes

The server: a call’s frame answered, the operation done by alg, the effect’s real handler (as through takes one); a frame that is no call of this API’s answered by a failure, which the client throws.

loopback

loopback : {h : HFunctor}
         -> {e : HFunctor}
         -> Api h
         -> ({a : Type} -> h.f (Co e) a -> Co e a)
         -> Transport e

A transport to a server in the same program: each frame answered by respond, as a server would. (No network: a test’s.)

locally

locally : {h : HFunctor}
        -> {e : HFunctor}
        -> {{failed : exception RemoteError <: e}}
        -> Api h
        -> ({a : Type} -> h.f (Co e) a -> Co e a)
        -> {a : Type}
        -> Co (h <+> e) a
        -> Co e a

h’s operations done by alg, each through the wire as remotely sends one and respond answers it: what a test of a client runs, with no server.