1 (* Persistent arrays. *)
 2 
 3 (* A persistent array presents itself as an immutable (hence, duplicable)
 4    array of duplicable elements. It can be read and updated; an update
 5    produces a new persistent array without altering the original one. *)
 6 
 7 (* The implementation is based on a single mutable array, difference lists,
 8    and a single lock, but these details do not appear in the interface. *)
 9 
10 abstract parray a
11 fact duplicable (parray a)
12 
13 (* Creation. *)
14 
15 val create: [a] duplicable a => (int, a) -> parray a
16 
17 (* Reading. *)
18 
19 val get: [a] duplicable a => (parray a, int) -> a
20 
21 (* Writing. *)
22 
23 val set: [a] duplicable a => (parray a, int, a) -> parray a
24