Guaranteeing safe destructive updates through a type system with uniqueness information for graphs
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.
KeywordsType System Uniqueness Type Reduction Rule Functional Program Functional Language
Unable to display preview. Download preview PDF.
- Achten P.M., J.H.G. van Groningen and M.J. Plasmeijer, High Level Specification of I/O in Functional Languages, in: Proc. of International Workshop on Functional Languages, Glasgow, UK, Springer Verlag, 1993.Google Scholar
- Bakel van, S., S. Smetsers and S. Brock, Partial Type Assignment in Left-Linear Term Rewriting Systems, in: Proc. of 17th Colloqium on Trees and Algebra in Programming (CAAP'92), pages 300–322, Rennes, France, Springer Verlag, LNCS 581, 1992.Google Scholar
- Barendregt H.P., M.C.J.D. van Eekelen, J.R.W. Glauert, J.R. Kennaway, M.J. Plasmeijer and M.R. Sleep, Term Graph Reduction, in: Proc. of Parallel Architectures and Languages Europe (PARLE), pages 141–158, Eindhoven, The Netherlands, Springer Verlag, LNCS 259 II, 1987.Google Scholar
- Barendsen Erik and Sjaak Smetsers, Graph Rewriting and Copying, Technical Report 92-20, University of Nijmegen, 1992.Google Scholar
- Guzmán Juan C. and Paul. Hudak, Single-Threaded Polymorphic Lambda Calculus, in: Proc. of Logic in Computer Science (LICS'90), pages 333–345, Phildelphia, IEEE Computer Society Press, 1991.Google Scholar
- Johnsson Thomas., Discussion Summary: which analysis?, in: Proc. of Functional Languages: Optimization For Parallelism, pages 4–5, Dagstuhl, Germany, Dagstuhl seminar, 1990.Google Scholar
- Milner R.A., Theory of Type Polymorphism in Programming, Journal of Computer and System Sciences, 17, 1978.Google Scholar
- Mycroft A., Abstract interpretation and optimising transformations for applicative programs, PhD thesis, University of Edinburgh, 1981.Google Scholar
- Wadler P., Linear types can change the world!, in: Proc. of Working Conference on Programming Concepts and Methods, pages 385–407, Israel, North Holland, 1990.Google Scholar