Previous  Up  

Module Froc_sa


module Froc_sa: sig .. end
Self-adjusting computation

Overview

Froc_sa implements self-adjusting computation following Acar et al. Changeable values are presented as a monad, using ideas from Lwt.

A changeable is a value that can change over time. New changeables may be created from existing ones using bind or one of its variants. When a changeable changes, the changeables which depend on it are updated by running their update functions (i.e. the function passed to bind). The dependencies of a changeable are updated before the changeable is updated, so that the update function sees a consistent view of the dependencies.

Self-adjusting computation proceeds in phases: after an initial computation, call write to change some inputs, then propagate to make the result consistent again.

Most functions returning changeables take an optional eq argument, which gives an equality function on the value of the resulting changeable. A changeable is considered to have changed only when updated with a value which is not equal (according to the equality function) to the old value. The default equality holds if the values compare to 0 (incomparable values are always not equal). It is encouraged that changeables of the same type always be given the same equality.

val init : unit -> unit
Initialize the library; can be called again to reinitialize.

Changeables


type +'a t
Type of changeables of type 'a.
type -'a u
Type of writeables of type 'a.
val changeable : ?eq:('a -> 'a -> bool) -> 'a -> 'a t * 'a u
changeable v is a changeable with initial value v.
val return : 'a -> 'a t
return v is a constant changeable with value v.
val fail : exn -> 'a t
fail e is a constant changeable that fails with the exception e.
val bind : ?eq:('a -> 'a -> bool) ->
       'b t -> ('b -> 'a t) -> 'a t
bind c f behaves as f applied to the value of c. If c fails, bind c f also fails, with the same exception.
val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
c >>= f is an alternative notation for bind c f.
val blift : ?eq:('a -> 'a -> bool) -> 'b t -> ('b -> 'a) -> 'a t
blift c ?eq f is equivalent to bind c (fun v -> return ?eq (f v)), but is slightly more efficient.
val lift : ?eq:('a -> 'a -> bool) -> ('b -> 'a) -> 'b t -> 'a t
lift ?eq f c is equivalent to blift c ?eq f; it can be partially applied to lift a function to the monad without yet binding it to a changeable.
val catch : ?eq:('a -> 'a -> bool) ->
       (unit -> 'a t) -> (exn -> 'a t) -> 'a t
catch cf f behaves the same as cf() if cf() succeeds. If cf() fails with some exception e, catch cf f behaves as f e.
val catch_lift : ?eq:('a -> 'a -> bool) ->
       (unit -> 'a t) -> (exn -> 'a) -> 'a t
catch_lift cf ?eq f is equivalent to catch cf (fun e -> return ?eq (f e)), but is slightly more efficient.
val try_bind : ?eq:('a -> 'a -> bool) ->
       (unit -> 'b t) ->
       ('b -> 'a t) -> (exn -> 'a t) -> 'a t
try_bind cf f g behaves as bind (cf()) f if cf() succeeds. If cf() fails with exception e, try_bind cf f g behaves as g e.
val try_bind_lift : ?eq:('a -> 'a -> bool) ->
       (unit -> 'b t) -> ('b -> 'a) -> (exn -> 'a) -> 'a t
try_bind_lift cf ?eq f g is equivalent to try_bind cf (fun v -> return ?eq (f v)) (fun e -> return ?eq (g e)), but is slightly more efficient.
val read : 'a t -> 'a
read c returns the value of c, or raises an exception if c fails.
val write : 'a u -> 'a -> unit
write w v updates the value of the associated changeable c. Changeables that depend on c will not be consistent until you call propagate.
val write_exn : 'a u -> exn -> unit
write_exn w e updates the associated changeable c to fail with exception e. Changeables that depend on c will not be consistent until you call propagate.
val propagate : unit -> unit
Process any outstanding changes so all changeables are consistent.
val memo : ?size:int ->
       ?hash:('a -> int) -> ?eq:('a -> 'a -> bool) -> unit -> ('a -> 'b) -> 'a -> 'b
memo f creates a memo function f' from f. When f' x is called from within an update function, there may be either a hit or a miss. A hit happens when some f' x' was called in the previous run of the update function, when eq x x', and no later call has already hit (that is, hits must happen in the same order as the calls happened in the previous run). On a miss, f' x calls f x and stores its value for possible reuse. On a hit, f' x returns the value of the previous call, and any updates necessary to make the value consistent are executed.

The main point of memo is to avoid needless recomputation in cases where a computation is executed in an update function for some changeable, but does not actually use the changeables's value. For example, in 

       let g = memo () fun x -> ... in
       c >>= fun _ -> g 7
the returned changeable is indifferent to the value of c. Without memo it would be recomputed every time c changes; with memo it is computed only the first time.

The unit argument makes it possible to memoize a recursive function, using the following idiom: 

     let m = memo () in (* creates the memo table *)
       let rec f x = ... m f y in
       let f x = m f x

The default hash function is not appropriate for changeables (since they contain mutable data); hash should be used instead.

val hash : 'a t -> int
A hash function for changeables,

Variations


val bindN : ?eq:('a -> 'a -> bool) ->
       'b t list -> ('b list -> 'a t) -> 'a t
val liftN : ?eq:('a -> 'a -> bool) ->
       ('b list -> 'a) -> 'b t list -> 'a t
val liftN : ?eq:('a -> 'a -> bool) ->
       ('b list -> 'a) -> 'b t list -> 'a t
val bind2 : ?eq:('a -> 'a -> bool) ->
       'b t -> 'c t -> ('b -> 'c -> 'a t) -> 'a t
val blift2 : ?eq:('a -> 'a -> bool) ->
       'b t -> 'c t -> ('b -> 'c -> 'a) -> 'a t
val lift2 : ?eq:('a -> 'a -> bool) ->
       ('b -> 'c -> 'a) -> 'b t -> 'c t -> 'a t
val bind3 : ?eq:('a -> 'a -> bool) ->
       'b t ->
       'c t ->
       'd t -> ('b -> 'c -> 'd -> 'a t) -> 'a t
val blift3 : ?eq:('a -> 'a -> bool) ->
       'b t ->
       'c t -> 'd t -> ('b -> 'c -> 'd -> 'a) -> 'a t
val lift3 : ?eq:('a -> 'a -> bool) ->
       ('b -> 'c -> 'd -> 'a) ->
       'b t -> 'c t -> 'd t -> 'a t
val bind4 : ?eq:('a -> 'a -> bool) ->
       'b t ->
       'c t ->
       'd t ->
       'e t -> ('b -> 'c -> 'd -> 'e -> 'a t) -> 'a t
val blift4 : ?eq:('a -> 'a -> bool) ->
       'b t ->
       'c t ->
       'd t -> 'e t -> ('b -> 'c -> 'd -> 'e -> 'a) -> 'a t
val lift4 : ?eq:('a -> 'a -> bool) ->
       ('b -> 'c -> 'd -> 'e -> 'a) ->
       'b t -> 'c t -> 'd t -> 'e t -> 'a t
val bind5 : ?eq:('a -> 'a -> bool) ->
       'b t ->
       'c t ->
       'd t ->
       'e t ->
       'f t -> ('b -> 'c -> 'd -> 'e -> 'f -> 'a t) -> 'a t
val blift5 : ?eq:('a -> 'a -> bool) ->
       'b t ->
       'c t ->
       'd t ->
       'e t ->
       'f t -> ('b -> 'c -> 'd -> 'e -> 'f -> 'a) -> 'a t
val lift5 : ?eq:('a -> 'a -> bool) ->
       ('b -> 'c -> 'd -> 'e -> 'f -> 'a) ->
       'b t ->
       'c t -> 'd t -> 'e t -> 'f t -> 'a t
val bind6 : ?eq:('a -> 'a -> bool) ->
       'b t ->
       'c t ->
       'd t ->
       'e t ->
       'f t ->
       'g t ->
       ('b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'a t) -> 'a t
val blift6 : ?eq:('a -> 'a -> bool) ->
       'b t ->
       'c t ->
       'd t ->
       'e t ->
       'f t ->
       'g t -> ('b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'a) -> 'a t
val lift6 : ?eq:('a -> 'a -> bool) ->
       ('b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'a) ->
       'b t ->
       'c t ->
       'd t -> 'e t -> 'f t -> 'g t -> 'a t
val bind7 : ?eq:('a -> 'a -> bool) ->
       'b t ->
       'c t ->
       'd t ->
       'e t ->
       'f t ->
       'g t ->
       'h t ->
       ('b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'a t) -> 'a t
val blift7 : ?eq:('a -> 'a -> bool) ->
       'b t ->
       'c t ->
       'd t ->
       'e t ->
       'f t ->
       'g t ->
       'h t ->
       ('b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'a) -> 'a t
val lift7 : ?eq:('a -> 'a -> bool) ->
       ('b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'a) ->
       'b t ->
       'c t ->
       'd t ->
       'e t -> 'f t -> 'g t -> 'h t -> 'a t

Debugging


val set_debug : (string -> unit) -> unit
Set a function for showing library debugging.