std.reference

For a cell of the world: made with its first value, read, written. A page’s events are each a run of their own, so what they share lives in the world between them — a cell, as an element (browser.dom’s Node) does. (A state threaded through one computation is state’s, handled in the language; a cell is the world’s, reference.provider.js.)

Reference

data Reference s = MkReference Int

A cell holding an s. (A number the provider gives it: a program only gets one from newReference.)

ReferenceF

data ReferenceF s (m : Type -> Type) x
  = NewReference s (Reference s -> x)
  | ReadReference (Reference s) (s -> x)
  | WriteReference (Reference s) s x

The operations: each says what it gives back by a function to the rest (x).

reference

reference : (s : Type) -> HFunctor

For cells of the world: made with a first value, read and written, shared by a page’s events.

newReference

newReference : {s : Type}
             -> {e : HFunctor}
             -> {{ev : reference s <: e}}
             -> s
             -> Co e (Reference s)

A new cell, holding st: in any effect the cells are in, by the evidence (as state’s get).

readReference

readReference : {s : Type}
              -> {e : HFunctor}
              -> {{ev : reference s <: e}}
              -> Reference s
              -> Co e s

What a cell holds.

writeReference

writeReference : {s : Type}
               -> {e : HFunctor}
               -> {{ev : reference s <: e}}
               -> Reference s
               -> s
               -> Co e Unit

… and it holds st now.