Runtime.Local

Local mutable state confined to a scoped callback.

run gives its callback a fresh cell. The cell’s permission cannot leave the callback, so a computation that only uses local state is pure where it is called, and may run during compile-time evaluation.

Cell

type Cell e a =    { read : () ->{e} a    , write : a ->{e} ()    }Source

A mutable cell holding an a, accessed with permission e. A cell contains functions, so it cannot cross a task boundary.

Fields

read

read : () ->{e} aSource

The last value written, initially the one run was given.

write

write : a ->{e} ()Source

Replaces the value.

run

run : a -> (Cell {#s} a ->{#s} b) ->{e} bSource

Calls action with a fresh cell holding initial and returns its result. The result may not carry the cell’s permission; other effects of action pass through. Nested runs have independent cells.

import Runtime.Local

doubled =
    Runtime.Local.run 21 { cell ->
        cell.write (cell.read () * 2)
        cell.read ()
    }

doubled == 42