Unison tickers sketch

tickers.u

type Counter a = { value : a,
                   tick : (a -> a) }

tock : (state -> Counter a)
          -> (Counter a -> state -> state)
          -> state 
          -> (a, state)

tock sc css s =
    c = sc s
    v = Counter.value c
    c' = Counter.value.modify (Counter.tick c) c
    s' = css c' s
    (v, s')

adder = Counter 1 Nat.increment

> tock id const adder

ability Ticker where
    tick : (state -> Counter a)
           -> (Counter a -> state -> state)
           -> a

Ticker.withCounters.handler state =
    cases
        { Ticker.tick sc css -> k } ->
            match (tock sc css state) with
            (v, state') ->
                handle k v
                with Ticker.withCounters.handler state'
        { v } -> v

Ticker.withCounters c x =
    handle !x with Ticker.withCounters.handler c

c = '(Ticker.tick id const)

> withCounters adder '[!c, !c, !c]

type MyCounter = { c1 : Counter Nat,
                   c2 : Counter Nat }

counters = MyCounter (Counter 1 Nat.increment)
                     (Counter 10 (c -> c + 10))

tick1 = '(Ticker.tick c1 c1.set)
tick2 = '(Ticker.tick c2 c2.set)

> withCounters counters '[!tick1, !tick2, !tick1, !tick2]