The HashCons Library


The HashCons Library supports the implementation of hash-consed representations of data structures. Such representations are useful to reduce space usage by sharing common substructures and to provide constant-time equality testing for large structures.

To use this library, you need to use a two-level definition of your data structures. For example, we might define a hash-cons representation of lambda terms as follows:

structure HC = HashCons

type var = HashConsString.obj

datatype term_node
  = VAR of var
  | LAM of (var * term)
  | APP of (term * term)
withtype term = term_node HC.obj

And you need to define an equality function on your terms (this function can use the hash-cons identity on subterms). For example, here is the equality function for our lambda terms:

fun eq (APP(t11, t12), APP(t21, t22)) = HC.same(t11, t21) andalso HC.same(t12, t22)
  | eq (LAM(x, t1), LAM(y, t2)) = HC.same(x, y) andalso HC.same(t1, t2)
  | eq (VAR x, VAR y) = HC.same(x, y)
  | eq _ = false

With the equality function defined, we can then create a hash-cons table:

val tbl = {eq = eq}

And define constructor functions:

val mkAPP = HC.cons2 tbl (0wx1, APP)
val mkLAM = HC.cons2 tbl (0wx3, LAM)
val mkVAR = HC.cons1 tbl (0wx7, VAR)
val var =

Note that we pick successive prime numbers for the constructor hash codes. Using these constructors, we can construct the representation of the identity function "\(\lambda{} x . x\)" as follows:

mkLAM(var "x", mkVAR(var "x"))

In addition to term construction, this library also supports finite sets and maps using the unique hash-cons codes as keys.


structure HashCons

The main module in the library, which defines the basic types and various utility functions.

structure HashConsAtom

Code to package the Atom.atom type as a hash-consed object.

structure HashConsMap

Implements finite maps keyed by hash-consed objects.

structure HashConsString

Code to package the string type as a hash-consed object.

structure HashConsSet

Implements finite sets of hash-consed objects.

functor HashConsGroundFn

A functor for implementing new leaf types as hash-consed objects.


For SML/NJ, include $/ in your CM file.

For use in MLton, include $(SML_LIB)/smlnj-lib/HashCons/ in your MLB file.