The following code shows a safe and sound implementation of a polymorphic heap with references and updates. The heap is capable of storing of polymorphic, functional and IO values. All operations are *statically* checked. An attempt to alter a heap reference with a value of a mismatched type leads to a _compile-time_ error. Everything is implemented in Haskell98 + multiparameter classes with functional dependencies + overlapping instances.
The problem you mention later, that the type of the heap returned is different from the type of the heap passed, is fatal. The following expression is untypeable: let heap = init_gh in let (mr,heap1) = if 1<2 then let (xr,h) = alloc_gh 42 heap in (Just xr,h) else (Nothing,heap) in case mr of Nothing -> "" Just r -> show (fetch_gh r heap1) Heaps should be more dynamic than this; the (type of the) *reference* should encode the type it points to, but the (type of the) *heap* should not. The question is still open... --KW 8-)