Hi everyone! I’m currently working on a little research project where we have been investigating reasoning about imperative code in OCaml, as part of which, I have been looking for interesting uses of mutability in recursive data structures.
Through careful use of Sherlocode and scanning the standard libraries, the obvious examples that I have found have been:
Singly/doubly linked lists
AVL Tree
Beyond these, I was wondering if anyone had any interesting examples they had run into in their own code of using mutability with recursive datatypes? Think something of the form:
type t = A of { ... mutable field: c ... }
and ...
and c = ... t ..
Or anything of a similar form that combines mutability with recursive instances of a type?
(* The concrete type of a future. Future's are mutable, but once they are
determined they become immutable. A future has a state which starts as
undetermined, can become determined or an alias. An alias is a future that
needs to exist because some unknown computation will eventually become its
value, and once that computation is found out, we set the future to an
alias to that future. *)
type 'a u = { mutable state : 'a state }
and 'a state =
[ 'a Abb_intf.Future.Set.t
| `Undet of 'a undet
| `Alias of 'a u
]
(* An undetermined has an optional function, which is some work to be
executed, watchers are executed when this undetermined future becomes
determined, deps are futures that are not required to be executed before
this future is determined but in some meaningful way connected to it, the
abort function is what to do if this future is aborted, and finally num_ops
is how many operations have been performed on this future. The definition
of an "operation" is kind of vague but basically it corresponds to mutating
this undetermined future in some way. *)
and 'a undet = {
mutable f : (State.t -> State.t) option;
mutable watchers : 'a Watcher.t list;
mutable deps : dep list;
abort : abort;
mutable num_ops : int;
}
There are three patterns for writing a compiler (speaking at a ridiculously high level):
immutable AST, with each analysis pass constructing a new AST (of a new type with new slots for the results of the analysis): sometimes called the “nanopass” method
immutable AST, with a unique index in each node, used to index into (perhaps hash-)tables for storing/retrieving results of analyses
mutable AST with slots for analysis results, that start off empty and are filled-in by those passes
In implementing an attribute-grammar evaluator, I chose methods 2, 3, but eventually discarded 2 in favor of 3.
Of course, an AST is nearly-always a recursive data-type.
The ancient CIL library (or our maintained fork) uses an extensive mix of recursive ADTs and records with mutable fields, for better or worse. For some things it also uses unique IDs and physical equality, so it’s anything but elegant.
Following on @orbitz example, Lwt also has some “recursive mutability” in its promises. In the same vein, the Incremental / Self-Adjusting Computations (SAC) / Functional Reactive Programming (FRP) are mostly built around a directed (acyclic) graph of mutable nodes (see note, react, lwd, ocurrent, incremental, etc etc)
For datastructures, the efficient construction of suffix tries involves (mutable) suffix links and children (see for example Filliâtre’s implementation of Ukkonen’s algorithm)… also Knuth’s dancing links for a fancier example of double-linked lists, or skip lists.
