Bosatsu packages

Yichus/Transaction

Builtin package (resource transaction.bosatsu). This is the complete package source used by this build. The export list names its public API; definitions below give the types and behavior.

New to the API? Start with Make a calculator or Build an API, then use this page to look up a definition.

package Yichus/Transaction

from Yichus/Data import Db
from Yichus/IO import IO
from Yichus/Service import Reply, TryAgain

export (
  Scope, TxTable, Txn, Outcome(),
  replied,
  tx_table, tx_pure, tx_bind, tx_map_abort, tx_abort, tx_read, tx_next_id, tx_insert, tx_write, tx_delete,
  tx_database_time_millis, tx_new_token,
  transaction
)

exposes (Yichus/Data, Yichus/IO, Yichus/Service)

# The runtime creates a fresh scope for each attempt. There is no Scope
# constructor, IO-to-Txn lift, or public Txn interpreter.
# Scope and table row parameters are invariant; transaction error and result
# parameters are covariant. Declare those kinds at the runtime boundary.
external type Scope[s: *]
external type TxTable[s: *, a: *]
external type Txn[s: *, e: +*, a: +*]

enum Outcome[e, a]:
  Committed(value: a)
  Aborted(reason: e)
  RetryExhausted
  CommitUnknown

external def tx_table[s, a](scope: Scope[s], name: String) -> TxTable[s, a]
external def tx_pure[s, e, a](value: a) -> Txn[s, e, a]
external def tx_bind[s, e, a, b](plan: Txn[s, e, a], next: a -> Txn[s, e, b]) -> Txn[s, e, b]
# Translate only an abort from plan. A successful value passes through, and
# a later abort in the caller's continuation is outside this mapping.
external def tx_map_abort[s, e, f, a](plan: Txn[s, e, a], map: e -> f) -> Txn[s, f, a]
external def tx_abort[s, e, a](reason: e) -> Txn[s, e, a]
external def tx_read[s, e, a](tbl: TxTable[s, a], key: String) -> Txn[s, e, Option[a]]
# Allocate the table's next id inside this attempt. An abort or serialization
# retry rolls the allocation back with the rest of the transaction.
external def tx_next_id[s, e, a](tbl: TxTable[s, a]) -> Txn[s, e, String]
# Insert the row only when its key is absent. An existing row is left unchanged,
# and Unit deliberately does not reveal whether the key was already present.
external def tx_insert[s, e, a](tbl: TxTable[s, a], key: String, value: a) -> Txn[s, e, Unit]
external def tx_write[s, e, a](tbl: TxTable[s, a], key: String, value: a) -> Txn[s, e, Unit]
external def tx_delete[s, e, a](tbl: TxTable[s, a], key: String) -> Txn[s, e, Unit]
# Unix epoch milliseconds read from the database transaction. Every read in
# one attempt returns the same value. A serialization retry is a new attempt
# and may observe a later value.
external def tx_database_time_millis[s, e](scope: Scope[s]) -> Txn[s, e, Int]
# A fresh unguessable token: 24 bytes from a cryptographically secure
# generator, written as 32 base64url characters (A-Z, a-z, 0-9, - and _)
# with no padding. Every call returns a new token, so two calls in one
# attempt differ. A serialization retry is a new attempt and mints new
# tokens, so a token from an attempt that was retried is never seen. It
# reads and writes no table.
external def tx_new_token[s, e](scope: Scope[s]) -> Txn[s, e, String]

# s cannot occur in the returned a or e: the caller supplies a computation
# valid for EVERY scope, while its result and error types remain fixed.
external def transaction[e, a](db: Db, plan: forall s. Scope[s] -> Txn[s, e, a]) -> IO[Outcome[e, a]]

# A transaction's outcome as a handler's Reply: a commit answers `done`'s
# reply and an abort `refused`'s. RetryExhausted answers TryAgain: nothing
# was saved, so the same request can run again. CommitUnknown answers
# `unconfirmed`, the caller's choice, because only the command knows
# whether running it twice is safe: TryAgain when a resend finds its own
# committed result (the plan first reads a row keyed by the request, or a
# create replays the row it made), otherwise a refusal that tells the
# caller to check before sending the request again.
def replied[e, a, r, b](outcome: Outcome[e, a], done: a -> Reply[r, b], refused: e -> Reply[r, b], unconfirmed: Reply[r, b]) -> Reply[r, b]:
  match outcome:
    case Committed(value): done(value)
    case Aborted(reason): refused(reason)
    case RetryExhausted: TryAgain("the service was busy with other changes to the same data; send the request again")
    case CommitUnknown: unconfirmed