Batching transactions in durable storage

batching.u

unique ability Batch where
  increment : Nat -> () 

-- Like `State.transact`, but pauses the computation every `batchSize` calls to 
-- `Batch.increment` and commits the work so far in one transaction, then resumes
-- the rest of the computation.
State.transact.batched : Nat -> Database -> '{Batch, Transaction, Exception} a ->{State, Exception} a
State.transact.batched batchSize db b = 
  go : Nat -> Request {Batch} a -> Either ('{Batch,Transaction,Exception} a) a
  go acc = cases
    { a } -> Right a
    { Batch.increment by -> k } -> 
      acc' = acc + by
      if acc' >= batchSize then Left k
      else handle !k with go acc'
  loop : '{Batch, Transaction, Exception} a ->{State, Exception} a 
  loop b = match transact db '(handle !b with go 0) with
    Right a -> a
    Left b -> loop b 
  loop b

ex = transact.batched 100 db do
  c = Cell.named "hi" 0
  inc i = 
    Batch.increment 1
    Cell.write.tx c (Cell.read.tx c + 1)
  List.range 0 1000 |> List.foreach inc