Types for describing coordinated data structures

13 years 11 months ago
Types for describing coordinated data structures
Coordinated data structures are sets of (perhaps unbounded) data structures where the nodes of each structure may share 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 ex...
Michael F. Ringenburg, Dan Grossman
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where TLDI
Authors Michael F. Ringenburg, Dan Grossman
Comments (0)