The HashCons Library

Overview

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 = HC.new {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 = HW.mk

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.

Contents

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.

Usage

For SML/NJ, include $/hash-cons-lib.cm in your CM file.

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