Guaranteeing safe destructive updates through a type system with uniqueness information for graphs
Sjaak Smetsers, Erik Barendsen, M.C.J.D. van Eekelen, Rinus Plasmeijer · 1994
In this paper we present a type system for graph rewrite systems: uniqueness typing . It employs usage information to deduce whether an object is `unique' at a certain moment, i.e. is only locally accessible. In a type of a function it can be specified that the function requires a unique argument object. The correctness of type assignment guarantees that no external access on the original object will take place in the future. The presented type system is proven to be correct. We illustrate the power of the system by defining an elegant quicksort algorithm that performs the sorting in situ on the data structure. 1. Introduction Some operations on complex data structures (such as arrays) cannot be implemented efficiently without allowing a form of destructive updating. For convenience, we speak about those functions as `destructively using' their arguments. In case of graph-like implementations of functional languages without any precautions, this destructive usage is dangerous: on the ...