The SML/NJ Library Reference Manual


The UREF signature

The UREF signature defines the interface to a union/find data type with ref-like interface. An implementation of this interface consists of the uref type constructor, with operations for creating a new uref, getting the contents of an element, checking for equality of two elements, and for joining two elements. The uref type is analogous to ref as expressed in the following table:
Type
Operation 'a ref 'a uref
Introduction ref uRef
Elimination ! !!
Equality = equal
Update := update
Union n.a. union , link, unify
The main difference between references and urefs is in the union operation. Without union, references and urefs can be used interchangebly (except in pattern matching). An assignment to a reference changes only the contents of the reference, but not the reference itself. In particular, any two references that were different (in the sense of the equality predicate = returning false) before an assignment will still be so. Their contents may or may not be equal after the assignment, though. In contrast, applying the union operations ( link, union, unify) to two uref elements makes the two elements themselves equal (in the sense of the predicate equal returning true). As a consequence their contents will also be identical: in the case of link and union it will be the contents of one of the two unioned elements, in the case of unify the contents is determined by a supplied unification function.


Synopsis

signature UREF
structure SimpleURef : UREF
structure URef : UREF

Interface

type 'a uref
val uRef : 'a -> 'a uref
val equal : ('a uref * 'a uref) -> bool
val !! : 'a uref -> 'a
val update : ('a uref * 'a) -> unit
val unify : (('a * 'a) -> 'a) -> ('a uref * 'a uref) -> unit
val union : ('a uref * 'a uref) -> unit
val link : ('a uref * 'a uref) -> unit

Description

type 'a uref
The type constructor for union/find references.

uRef a
creates a new, distinct, uref cell.

equal (ur1, ur2)
returns true if and only if ur1 and ur2 are either made by the same call to uRef, or if they have been unioned by a call to unify, union or link .

!! ur
returns the contents of ur.

update (ur, x)
updates the contents of ur to be x. This update affects all urefs that have been unioned with ur.

unify f (ur1, ur2)
makes ur1 and ur2 equal, and updates their value to be the result of f(!!ur1, !!ur2). The function f is evaluated prior to unioning the urefs, so if it raises an exception, no union takes place.

union (ur1, ur2)
makes ur1 and ur2 equal; the contents of the unioned element is the contents of one of ur1 and ur2 before the union operation. After unioning, the elements ur1 and ur2 will be congruent in the sense that they are interchangeable in any context.

link (ur1, ur2)
makes ur1 and ur2 equal; the contents of the linked element is the contents of ur2 before the link operation.


Discussion

There are two implementations of the UREF signature provided by the library: the SimpleURef structure represents urefs using a standard union/find data structure with path compression. The URef structure adds ranks to balance union operations.


[ INDEX | TOP | Parent | Root ]

Last Modified May 29, 1996
Copyright © 1996 AT&T Research