Type-Indexed Rows Export

@inproceedings{citeulike:5404951, abstract = {Record calculi use labels to distinguish between the elements of products and sums. This paper presents a novel variation, type-indexed rows , in which labels are discarded and elements are indexed by their type alone. The calculus, \λ-TIR , can express tuples, recursive datatypes, monomorphic records, polymorphic extensible records, and closed-world style type-based overloading. Our motivating application of \λ-TIR , however, is to encode the "choice" types of XML, and the "unordered tuple" types of SGML. Indeed, \λ-TIR is the kernel of the language XM\λ, a lazy functional language with direct support for XML types ("DTDs") and terms ("documents").The system is built from rows, equality constraints, insertion constraints and constrained, or qualified, parametric polymorphism. The test for constraint satisfaction is complete, and for constraint entailment is only mildly incomplete. We present a type checking algorithm, and show how \λ-TIR may be implemented by a type-directed translation which replaces type-indexing by conventional natural-number indexing. Though not presented in this paper, we have also developed a constraint simplification algorithm and type inference system.}, address = {New York, NY, USA}, author = {Shields, Mark and Meijer, Erik}, booktitle = {POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, citeulike-article-id = {5404951}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=360204.360230}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/360204.360230}, doi = {10.1145/360204.360230}, isbn = {1-58113-336-7}, keywords = {equality, lambda-calculus, records, type-checking, type-indexed, xml}, location = {London, United Kingdom}, pages = {261--275}, posted-at = {2009-08-10 14:40:09}, priority = {2}, publisher = {ACM}, title = {Type-Indexed Rows}, url = {http://dx.doi.org/10.1145/360204.360230}, year = {2001} }

TY - CONF ID - citeulike:5404951 L3 - citeulike-article-id:5404951 N2 - Record calculi use labels to distinguish between the elements of products and sums. This paper presents a novel variation, type-indexed rows , in which labels are discarded and elements are indexed by their type alone. The calculus, λ-TIR , can express tuples, recursive datatypes, monomorphic records, polymorphic extensible records, and closed-world style type-based overloading. Our motivating application of λ-TIR , however, is to encode the "choice" types of XML, and the "unordered tuple" types of SGML. Indeed, λ-TIR is the kernel of the language XMλ, a lazy functional language with direct support for XML types ("DTDs") and terms ("documents").The system is built from rows, equality constraints, insertion constraints and constrained, or qualified, parametric polymorphism. The test for constraint satisfaction is complete, and for constraint entailment is only mildly incomplete. We present a type checking algorithm, and show how λ-TIR may be implemented by a type-directed translation which replaces type-indexing by conventional natural-number indexing. Though not presented in this paper, we have also developed a constraint simplification algorithm and type inference system. CY - London, United Kingdom SN - 1-58113-336-7 AD - New York, NY, USA EP - 275 TI - Type-Indexed Rows PB - ACM T2 - POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages SP - 261 KW - equality KW - lambda-calculus KW - records KW - type-checking KW - type-indexed KW - xml AU - Shields, Mark AU - Meijer, Erik PY - 2001/// UR - http://dx.doi.org/10.1145/360204.360230 ER -