Teleport

The checked mobility boundary: freezing a portable, single-use computation into an envelope, and placing that envelope wherever the installed transport puts it.

teleport does not call its argument. It seals the computation into bytes and hands them to place, the one operation of the Placement effect, so where a computation goes is the handler’s choice and never an argument here: the same source moves over a socket or lands in this process according to which transport is installed around it. The closure must capture only content-addressed code and portable data (@ portable) and be invoked at most once (@ once); the compiler proves that contract at every call site.

Nothing in this module runs a computation by calling it. A landing is always a decode of the envelope the sealing side produced, whether that envelope crossed a network or never left the process, so the same refusals are reachable on either route and a program cannot come to depend on staying put.

The envelope is a continuation, not a closure: it carries the machine state a suspend at the teleport call would have captured, so the landing side continues the sealing side’s run rather than starting a fresh one. That is what makes a sealing run’s output prefix followed by a landing run’s output suffix equal to the uninterrupted run. Compose it with Replay.record for a durable, replayable mobile run.

Types

MoveError

type MoveError
  = Unportable
  | Malformed
  | Foreign
  | Unsupported
  | Uncertified
  | Undelivered
  deriving (Eq, Show)

Why a computation could not be placed.

Unportable is a capture that cannot cross the boundary, refused while sealing rather than after the bytes have travelled. Malformed is an envelope that is not one, which includes one whose certificate no longer matches the captures it travelled with. Foreign is a well-formed envelope from other code: a continuation resolves its references by name against the definitions it was compiled with, so landing it against a different bundle is refused rather than silently resolved. Uncertified is a well-formed envelope from this very bundle that nothing proved portable, which is what a suspended run is: it carries the machine state a step budget stopped at, not a computation the compiler checked may travel. Unsupported is a host that cannot land continuations at all, which is every native binary.

Undelivered is the one refusal no runtime raises: it is a transport saying the envelope never reached the far side. It carries no reason because the reasons belong to the transport’s own vocabulary (a socket has a NetError, a queue has something else), and a mobility answer that named one of them would bind this module to that transport. A handler that wants the detail reports it itself; what it answers here is that placement did not happen.

Effects

Placement

effect Placement
  place(Bytes) : Result(Unit, MoveError)

Where a sealed computation goes.

The operation speaks in Bytes rather than in a closure, and that is deliberate: an envelope is inert, so a handler can length-frame it, write it to a socket, and answer for the write, none of which it could do with a live computation. It is also what keeps the effect genuinely re-handleable, since a transport written outside this module needs nothing from here but the bytes.

A handler answers for delivery, not for the computation: Ok(()) means the envelope reached the endpoint the transport chose, and what the landing side then prints is that side’s output, not this one’s return value.

Functions and Values

seal

seal : forall a. ((() -> a ! {IO}) @ {once, portable}) -> Result(Wire.Bytes, Teleport.MoveError) ! {IO}

Freeze a portable, single-use closure into an envelope.

The capture check happens here, before any bytes exist: a closure holding something that cannot cross is Unportable at the seal rather than Malformed after a trip over the network.

A closure may name top-level code and portable parameters, so the computation to move is written as a top-level function and sealed by name:

fn elsewhere() : Unit ! {IO} = println("elsewhere")

fn main() : Unit ! {IO} =
  match seal(elsewhere) of
    Err(x) => println(show(x))
    Ok(_envelope) => println("sealed")

land

land : (Wire.Bytes) -> Result(Unit, Teleport.MoveError) ! {IO}

Decode an envelope and run it to completion here.

The bundle identity and the portability certificate are both checked before a single step. An envelope built against other code is Foreign rather than a run whose by-name references resolve to definitions it never saw; one whose captures no longer hash to what was checked is Malformed; one that carries no such check is Uncertified. Output from the landing point on goes to this host’s sink.

Neither check asks who sent the envelope. Both digests are unkeyed and the bundle is derived from a program both sides already have, so what they establish is that the bytes are intact and belong to this code, never that the sender was entitled to place work here. Landing runs the computation the sender chose, with everything this program can do. That is what moving a computation means rather than a gap to be closed by decoding more carefully, so a host that takes envelopes off a socket picks its peers itself: bind such a receiver to loopback or a trusted network and treat the socket as the trust boundary. Authentication belongs in a transport handler that has a key, which the envelope format leaves room for and this version does not provide.

fn elsewhere() : Unit ! {IO} = println("elsewhere")

fn main() : Unit ! {IO} =
  match seal(elsewhere) of
    Err(x) => println(show(x))
    Ok(envelope) =>
      match land(envelope) of
        Err(x) => println(show(x))
        Ok(_done) => ()

teleport

teleport : forall a. ((() -> a ! {IO}) @ {once, portable}) -> Result(Unit, Teleport.MoveError) ! {IO, Teleport.Placement}

Seal a portable, single-use closure and place it.

The result reports delivery. It is Unit on success and not the closure’s value because across a real transport there is no value to return: the sealing process reaches place and the computation continues in another one, so a signature promising the closure’s result back would only be honest for transports that happen to stay local.

A closure over top-level code and portable parameters satisfies the contract; run_here below shows one running end to end.

Capturing a local binding is refused at compile time: a local does not travel, so the closure could not move to a fresh runtime:

let n = 6
teleport(\() -> n * 7)

run_here

run_here : forall e0 a. (() -> a ! {IO, Teleport.Placement, e0}) -> a ! {IO, e0}

Run action with placement landing in this process.

This is a transport, not a fallback: the computation is still sealed into an envelope and still landed by decoding it, so Unportable and Malformed are reachable here exactly as they are over a socket. What it does not exercise is a second process, which is the only thing that can show a continuation being resumed by a runtime that did not build it.

The cut is visible in the output: what the sealing side had already printed comes first, the landed suffix continues from the teleport call, and the placement’s own answer reports only that delivery succeeded.

fn suffix() : Unit ! {IO} = println("landed")

fn main() : Unit ! {IO} =
  let _before = println("sealed")
  println(show(run_here(\() -> teleport(suffix))))

prints sealed, then landed from the landed suffix, then Ok(()) for the delivery. Sealing needs the running program’s code identity, which a compiled or interpreted program has and a bare snippet evaluator does not, so this is shown rather than run here.