With regards to the following... "There are cases in which this parameterization costs convenience and gains nothing -- for example, the standard library function (randomIO :: Random a => IO a) cannot be implemented in Haskell without the unsafePerformIO hack, yet there's nothing semantically objectionable about it. Worse, we may weaken type checking by the translation, while gaining nothing: for example, the interface below cannot provide static guarantees like a == b <=> fromAtom a == fromAtom b if toAtom is parameterized by an "atom space"." Can we not make this guarantee with multiple Atom-spaces if we use the same local universal quantification trick used on the ST monad? IE add a type parameter 's' to the type of Atom? Keean.