Transactions

Tx m α is a transaction body of mode m that returns α. Bodies compose with do notation, raise and catch TypeDBError, and run IO (whose errors become TypeDBError.io).

Tx is an irreducible definition, not an abbreviation, so that Tx .read α and Tx .write α are different types: a body that writes cannot be passed where a read body is expected. Operations take an [Allows m need] instance, so a read-mode body cannot call one that needs a write.

Driver.runSync is the transactor: it opens the transaction, runs the body, commits a write or schema transaction when the body succeeds, and closes the transaction without committing when the body fails. A retry policy can re-run the whole body when the commit loses a conflict.

structure TypeDB.TxCtx : Type

What a transaction body runs against.

• driver : Driver
• handle : Native.TxHandle
• database : String
• mode : TxMode
• options : TxOptions

@[irreducible]

def TypeDB.Tx (_m : TxMode) (α : Type) : Type

A transaction body of mode m returning α: a reader over the transaction's context. It is irreducible, so Tx .read α and Tx .write α stay different types, while the compiler still sees a ReaderT over EIO and turns loops over it into plain loops.

Equations

• TypeDB.Tx _m α = ReaderT TypeDB.TxCtx (EIO TypeDB.TypeDBError) α

@[inline]

def TypeDB.Tx.mk {m : TxMode} {α : Type} (f : TxCtx → EIO TypeDBError α) : Tx m α

Equations

• TypeDB.Tx.mk f = f

@[inline]

def TypeDB.Tx.run {m : TxMode} {α : Type} (x : Tx m α) : TxCtx → EIO TypeDBError α

Equations

• x.run = x

@[instance_reducible]

instance TypeDB.Tx.instMonad {m : TxMode} : Monad (Tx m)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TypeDB.Tx.instMonadExceptOfTypeDBError {m : TxMode} : MonadExceptOf TypeDBError (Tx m)

Equations

• TypeDB.Tx.instMonadExceptOfTypeDBError = { throw := @TypeDB.Tx.instMonadExceptOfTypeDBError._aux_1 m, tryCatch := @TypeDB.Tx.instMonadExceptOfTypeDBError._aux_3 m }

@[instance_reducible]

instance TypeDB.Tx.instMonadFinally {m : TxMode} : MonadFinally (Tx m)

Equations

• TypeDB.Tx.instMonadFinally = { tryFinally' := @TypeDB.Tx.instMonadFinally._aux_1 m }

@[instance_reducible]

instance TypeDB.Tx.instMonadLiftEIOTypeDBError {m : TxMode} : MonadLift (EIO TypeDBError) (Tx m)

Equations

• TypeDB.Tx.instMonadLiftEIOTypeDBError = { monadLift := @TypeDB.Tx.instMonadLiftEIOTypeDBError._aux_1 m }

@[instance_reducible]

instance TypeDB.Tx.instMonadLiftIO {m : TxMode} : MonadLift IO (Tx m)

Equations

• TypeDB.Tx.instMonadLiftIO = { monadLift := fun {α : Type} (x : IO α) => TypeDB.Tx.mk fun (x_1 : TypeDB.TxCtx) => liftM x }

@[instance_reducible]

instance TypeDB.Tx.instMonadLiftBaseIO {m : TxMode} : MonadLift BaseIO (Tx m)

Equations

• TypeDB.Tx.instMonadLiftBaseIO = { monadLift := fun {α : Type} (x : BaseIO α) => TypeDB.Tx.mk fun (x_1 : TypeDB.TxCtx) => liftM x }

@[inline]

def TypeDB.Tx.widen {m n : TxMode} {α : Type} [m.Allows n] (x : Tx n α) : Tx m α

Runs a body of a weaker mode inside a stronger transaction.

Equations

• x.widen = TypeDB.Tx.mk x.run

@[instance_reducible]

instance TypeDB.Tx.instMonadLiftReadWrite : MonadLift (Tx TxMode.read) (Tx TxMode.write)

Equations

• TypeDB.Tx.instMonadLiftReadWrite = { monadLift := fun {α : Type} => TypeDB.Tx.widen }

@[instance_reducible]

instance TypeDB.Tx.instMonadLiftReadSchema : MonadLift (Tx TxMode.read) (Tx TxMode.schema)

Equations

• TypeDB.Tx.instMonadLiftReadSchema = { monadLift := fun {α : Type} => TypeDB.Tx.widen }

@[instance_reducible]

instance TypeDB.Tx.instMonadLiftWriteSchema : MonadLift (Tx TxMode.write) (Tx TxMode.schema)

Equations

• TypeDB.Tx.instMonadLiftWriteSchema = { monadLift := fun {α : Type} => TypeDB.Tx.widen }

@[instance_reducible]

instance TypeDB.Tx.instInhabited {m : TxMode} {α : Type} : Inhabited (Tx m α)

Equations

• TypeDB.Tx.instInhabited = { default := TypeDB.Tx.mk fun (x : TypeDB.TxCtx) => throw (TypeDB.TypeDBError.internal "uninhabited transaction body") }

@[inline]

def TypeDB.Tx.ctx {m : TxMode} : Tx m TxCtx

The transaction's context.

Equations

• TypeDB.Tx.ctx = TypeDB.Tx.mk pure

@[inline]

def TypeDB.Tx.native {m : TxMode} {α : Type} (x : Native.NIO α) : Tx m α

Runs a native call, classifying its error.

Equations

• TypeDB.Tx.native x = liftM (TypeDB.native x)

@[inline]

def TypeDB.Tx.fail {m : TxMode} {α : Type} (e : TypeDBError) : Tx m α

Raises a typed error.

Equations

• TypeDB.Tx.fail e = throw e

def TypeDB.Tx.rollback {m : TxMode} [m.Allows TxMode.write] : Tx m Unit

Rolls back the writes made so far without ending the transaction.

Equations

• TypeDB.Tx.rollback = do let __do_lift ← TypeDB.Tx.ctx TypeDB.Tx.native (TypeDB.Native.txRollback __do_lift.handle)

@[reducible, inline]

abbrev TypeDB.MonadTypeDB (m : TxMode) (n : Type → Type) : Type 1

Transactions that may implement Tx m operations, for user monad stacks such as ReaderT Env (Tx .write). Any monad with a MonadLiftT (Tx m) instance qualifies.

Equations

• TypeDB.MonadTypeDB m n = MonadLiftT (TypeDB.Tx m) n

inductive TypeDB.Backoff : Type

Backoff between retries.

• none : Backoff
• constant (ms : Nat) : Backoff
• exponential (baseMs : Nat) (maxMs : Nat := 5000) : Backoff

  base · 2^attempt milliseconds, capped at maxMs.

def TypeDB.instReprBackoff.repr : Backoff → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• TypeDB.instReprBackoff.repr TypeDB.Backoff.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TypeDB.Backoff.none")).group prec✝

@[instance_reducible]

instance TypeDB.instReprBackoff : Repr Backoff

Equations

• TypeDB.instReprBackoff = { reprPrec := TypeDB.instReprBackoff.repr }

@[instance_reducible]

instance TypeDB.instInhabitedBackoff : Inhabited Backoff

Equations

• TypeDB.instInhabitedBackoff = { default := TypeDB.instInhabitedBackoff.default }

inductive TypeDB.RetryPolicy : Type

When run re-runs a transaction body.

• never : RetryPolicy
• conflicts (retries : Nat) (backoff : Backoff := Backoff.exponential 20) : RetryPolicy

  Re-run on commit conflicts, at most retries times. Other errors are never retried.

def TypeDB.instReprRetryPolicy.repr : RetryPolicy → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• TypeDB.instReprRetryPolicy.repr TypeDB.RetryPolicy.never prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TypeDB.RetryPolicy.never")).group prec✝

@[instance_reducible]

instance TypeDB.instReprRetryPolicy : Repr RetryPolicy

Equations

• TypeDB.instReprRetryPolicy = { reprPrec := TypeDB.instReprRetryPolicy.repr }

@[instance_reducible]

instance TypeDB.instInhabitedRetryPolicy : Inhabited RetryPolicy

Equations

• TypeDB.instInhabitedRetryPolicy = { default := TypeDB.instInhabitedRetryPolicy.default }

def TypeDB.RetryPolicy.delayMs : Backoff → Nat → Nat

Equations

• TypeDB.RetryPolicy.delayMs TypeDB.Backoff.none x✝ = 0
• TypeDB.RetryPolicy.delayMs (TypeDB.Backoff.constant ms) x✝ = ms
• TypeDB.RetryPolicy.delayMs (TypeDB.Backoff.exponential b cap) x✝ = min cap (b * 2 ^ x✝)

def TypeDB.Driver.runOnce {α : Type} (d : Driver) (db : String) (mode : TxMode) (body : Tx mode α) (opts : TxOptions := { }) : EIO TypeDBError α

Opens one transaction, runs body, and commits (write and schema mode) or closes (read mode). If the body fails, the transaction is closed without committing and the error is returned.

Equations

• One or more equations did not get rendered due to their size.

def TypeDB.Driver.runSync {α : Type} (d : Driver) (db : String) (mode : TxMode) (body : Tx mode α) (retry : RetryPolicy := RetryPolicy.never) (opts : TxOptions := { }) : EIO TypeDBError α

Runs a transaction on the calling thread, retrying the whole body on commit conflicts if retry says so.

Equations

• d.runSync db mode body TypeDB.RetryPolicy.never opts = d.runOnce db mode body opts
• d.runSync db mode body (TypeDB.RetryPolicy.conflicts a a_1) opts = TypeDB.Driver.runSync.go d db mode body opts a_1 0 a

def TypeDB.Driver.runSync.go {α : Type} (d : Driver) (db : String) (mode : TxMode) (body : Tx mode α) (opts : TxOptions) (backoff : Backoff) (attempt : Nat) : Nat → EIO TypeDBError α

fuel is the number of retries left.

Equations

• One or more equations did not get rendered due to their size.
• TypeDB.Driver.runSync.go d db mode body opts backoff attempt 0 = d.runOnce db mode body opts