Types for describing coordinated data structures

ABSTRACT

Coordinated data structures are sets of (perhaps unbounded) data structures where the nodes of each structure may share abstract types with the corresponding nodes of the other structures. For example, consider a list of arguments, and a separate list of functions, where the n-th function of the second list should be applied only to the n-th argument of the first list. We can guarantee that this invariant is obeyed by coordinating the two lists, such that the type of the n-th argument is existentially Quantified and identical to the argument type of the n-th function. In this paper, we describe a minimal set of features sufficient for a type system to support coordinated data structures. We also demonstrate that two known type systems (Crary and Weirich's LX [6] and Xi, Chen and Chen's guarded recursive datatypes [24]) have these features, even though the systems were developed for other purposes. We illustrate the power of coordinated data structures as a programming idiom with three examples: (1) a list of function closures stored as a list of environments and a separate list of code pointers, (2) a "tagless" list, and (3) a red-black tree where the values and colors are stored in separate trees that are guaranteed to have the same shape.

REFERENCES

• 1: Alexander Aiken , Edward L. Wimmers , T. K. Lakshman, Soft typing with conditional types, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177847]
• 2: Andrew W. Appel, Foundational Proof-Carrying Code, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.247, June 16-19, 2001
• 3: Juan Chen , Dinghao Wu , Andrew W. Appel , Hai Fang, A provably sound TAL for back-end optimization, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 4: Thomas H. Cormen , Clifford Stein , Ronald L. Rivest , Charles E. Leiserson, Introduction to Algorithms, McGraw-Hill Higher Education, 2001
• 5: Karl Crary, Toward a foundational typed assembly language, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.198-212, January 15-17, 2003, New Orleans, Louisiana, USA
• 6: Karl Crary , Stephanie Weirich, Flexible type analysis, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.233-248, September 27-29, 1999, Paris, France
• 7: Cormac Flanagan , Martín Abadi, Types for Safe Locking, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.91-108, March 22-28, 1999
• 8: Dan Grossman, Type-safe multithreading in cyclone, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 9: Dan Grossman , Greg Morrisett , Trevor Jim , Michael Hicks , Yanling Wang , James Cheney, Region-based memory management in cyclone, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 10: Nadeem A. Hamid , Zhong Shao , Valery Trifonov , Stefan Monnier , Zhaozhong Ni, A Syntactic Approach to Foundational Proof-Carrying Code, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.89-100, July 22-25, 2002
• 11: Ralf Hinze. Fun with phantom types. In Jeremy Gibbons and Oege de Moor, editors, The Fun of Programming, pages 245--262. Palgrave Macmillan, 2003.
• 12: Yasuhiko Minamide , Greg Morrisett , Robert Harper, Typed closure conversion, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.271-283, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237791]
• 13: Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic typed assembly language. In 2nd ACM Workshop on Compiler Support for System Software, pages 25--35, 1999. INRIA Technical Report 0288, 1999.
• 14: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999 [doi>10.1145/319301.319345]
• 15: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 16: Chris Okasaki, From fast exponentiation to square matrices: an adventure in types, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.28-35, September 27-29, 1999, Paris, France
• 17: François Pottier , Nadji Gauthier, Polymorphic typed defunctionalization, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.89-98, January 14-16, 2004, Venice, Italy
• 18: Francois Pottier and Yann Régis-Gianas. Towards efficient, typed LR parsers. Submitted to thephJournal of Functional Programming, September 2004.
• 19: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 20: Michael F. Ringenburg and Dan Grossman. Type safety and erasure proofs for "A type system for coordinated data structures". Technical Report 2004-07-03, University of Washington, 2004.
• 21: Mads Tofte , Jean-Pierre Talpin, Region-based memory management, Information and Computation, v.132 n.2, p.109-176, Feb. 1, 1997 [doi>10.1006/inco.1996.2613]
• 22: Mitchell Wand, Type inference for record concatenation and multiple inheritance, Information and Computation, v.93 n.1, p.1-15, July 1991 [doi>10.1016/0890-5401(91)90050-C]
• 23: Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]
• 24: Hongwei Xi , Chiyan Chen , Gang Chen, Guarded recursive datatype constructors, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.224-235, January 15-17, 2003, New Orleans, Louisiana, USA
• 25: Hongwei Xi , Robert Harper, A dependently typed assembly language, Proceedings of the sixth ACM SIGPLAN international conference on Functional programming, September 03-05, 2001, Florence, Italy
• 26: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]
• 27: http://www.cs.washington.edu/homes/miker/coord/.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

Keywords:
coordinated data structures