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.