Control.Fresh

The Fresh effect: a deterministic monotonic name supply (gensym).

fresh yields the next integer from a counter the code never threads; the handler starts it at 0 (or an explicit start) and increments by one each call, so a run’s names are a pure function of the order they are requested. gensym(prefix) builds a fresh string identifier. Opt-in: not in Base.

Effects

Fresh

effect Fresh
  fresh() : Int

Draw the next integer from the monotonic counter.

Functions and Values

run_fresh

run_fresh : forall e0 a. (() -> a ! {Control.Fresh.Fresh, e0}) -> a ! {e0}

Run action with a fresh-name counter starting at 0, discharging Fresh.

run_fresh(\() -> [gensym("tmp"), gensym("tmp")])

[tmp0, tmp1]

run_fresh_from

run_fresh_from : forall e0 a. (Int, () -> a ! {Control.Fresh.Fresh, e0}) -> a ! {e0}

Run action with the counter starting at start.

run_fresh_from(10, \() -> [fresh(), fresh()])

[10, 11]

gensym

gensym : (String) -> String ! {Control.Fresh.Fresh}

A fresh string identifier: prefix followed by the next counter value.