LIPIcs.TYPES.2015.6.pdf
- Filesize: 0.7 MB
- 24 pages
Document
Efficient Type Checking for Path Polymorphism
Authors
-
Part of:
Volume:
21st International Conference on Types for Proofs and Programs (TYPES 2015)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Types for Proofs and Programs (TYPES) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2018-03-15
Cite AsGet BibTex
Juan Edi, Andrés Viso, and Eduardo Bonelli. Efficient Type Checking for Path Polymorphism. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.TYPES.2015.6
https://doi.org/10.4230/LIPIcs.TYPES.2015.6
Abstract
A type system combining type application, constants as types, union types (associative, commutative and idempotent) and recursive types has recently been proposed for statically typing path polymorphism, the ability to define functions that can operate uniformly over
recursively specified applicative data structures. A typical pattern such functions resort to is \dataterm{x}{y} which decomposes a compound, in other words any applicative tree structure, into its parts. We study type-checking for this type system in two stages. First we propose algorithms for checking type equivalence and subtyping based on coinductive characterizations of those relations. We then formulate a syntax-directed presentation and prove its equivalence with the original one. This yields a type-checking algorithm which unfortunately has exponential time complexity in the worst case. A second algorithm is then proposed, based on automata techniques, which yields a polynomial-time type-checking algorithm.
Keywords
- lambda-calculus
- pattern matching
- path polymorphism
- type checking
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Roberto M. Amadio and Luca Cardelli. Subtyping recursive types. ACM Trans. Program. Lang. Syst., 15(4):575-631, 1993. URL: http://dx.doi.org/10.1145/155183.155231.
- H. Barendregt, W. Dekkers, and R. Statman. Lambda Calculus with Types. Perspectives in Logic. Cambridge University Press, 2013. URL: http://dx.doi.org/10.1017/cbo9781139032636.
- M. Brandt and F. Henglein. Coinductive axiomatization of recursive type equality and subtyping. Fundam. Inf., 33(4):309-338, 1998. URL: http://dx.doi.org/10.3233/fi-1998-33401.
- Luca Cardelli, Simone Martini, John C. Mitchell, and Andre Scedrov. An extension of system F with subtyping. In Takayasu Ito and Albert R. Meyer, editors, Theoretical Aspects of Computer Software, International Conference TACS '91, Sendai, Japan, September 24-27, 1991, Proceedings, volume 526 of Lecture Notes in Computer Science, pages 750-770. Springer, 1991. URL: http://dx.doi.org/10.1007/3-540-54415-1_73.
- Dario Colazzo and Giorgio Ghelli. Subtyping recursion and parametric polymorphism in kernel Fun. Inf. Comput., 198(2):71-147, 2005. URL: http://dx.doi.org/10.1016/j.ic.2004.11.003.
- Roberto Di Cosmo, François Pottier, and Didier Rémy. Subtyping recursive types modulo associative commutative products. In Pawel Urzyczyn, editor, Typed Lambda Calculi and Applications, 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005, Proceedings, volume 3461 of Lecture Notes in Computer Science, pages 179-193. Springer, 2005. URL: http://dx.doi.org/10.1007/11417170_14.
- Peter J. Downey, Ravi Sethi, and Robert Endre Tarjan. Variations on the common subexpression problem. J. ACM, 27(4):758-771, 1980. URL: http://dx.doi.org/10.1145/322217.322228.
- J. Edi and A. Viso. Prototype implementation of efficient type-checker in Scala. URL: https://github.com/juanedi/cap-typechecking.
- J. Edi, A. Viso, and E. Bonelli. Efficient type checking for path polymorphism, 2017. arXiv preprint 1704.09026. URL: http://arxiv.org/abs/1704.09026.
- B. Jay and D. Kesner. First-class patterns. J. Funct. Program., 19(2):191-225, 2009. URL: http://dx.doi.org/10.1017/s0956796808007144.
- Barry Jay. Pattern Calculus - Computing with Functions and Structures. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-540-89185-7.
- T. Jim and J. Palsberg. Type inference in systems of recursive types with subtyping, 1999. Draft. URL: http://web.cs.ucla.edu/~palsberg/draft/jim-palsberg99.pdf.
- Jan Willem Klop, Vincent van Oostrom, and Roel C. de Vrijer. Lambda calculus with patterns. Theor. Comput. Sci., 398(1-3):16-31, 2008. URL: http://dx.doi.org/10.1016/j.tcs.2008.01.019.
- D. Kozen, J. Palsberg, and M. I. Schwartzbach. Efficient recursive subtyping. Math. Struct. Comput. Sci., 5(1):113-125, 1995. URL: http://dx.doi.org/10.1017/s0960129500000657.
- Jens Palsberg and Tian Zhao. Efficient and flexible matching of recursive types. Inf. Comput., 171(2):364-387, 2001. URL: http://dx.doi.org/10.1006/inco.2001.3090.
-
B. C. Pierce. Types and Programming Languages. MIT Press, 2002.
- V. van Oostrom. Lambda calculus with patterns. Technical Report IR-228, Vrije Universiteit Amsterdam, 1990. URL: http://www.phil.uu.nl/~oostrom/publication/pdf/IR-228.pdf.
- Andrés Viso, Eduardo Bonelli, and Mauricio Ayala-Rincón. Type soundness for path polymorphism. Electr. Notes Theor. Comput. Sci., 323:235-251, 2016. URL: http://dx.doi.org/10.1016/j.entcs.2016.06.015.
- Jerome Vouillon. Subtyping union types. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings, volume 3210 of Lecture Notes in Computer Science, pages 415-429. Springer, 2004. URL: http://dx.doi.org/10.1007/978-3-540-30124-0_32.
- T. Zhao. Type Matching and Type Inference for Object-Oriented Systems. PhD thesis, Purdue University, 2002. URL: http://docs.lib.purdue.edu/dissertations/AAI3099873/.