Typed path polymorphism. (English) Zbl 1423.68089
Summary: Path polymorphism enables the definition of functions uniformly applicable to arbitrary recursively specified data structures. Path polymorphic function declarations rely on patterns of the form \(x\)\(y\) (i.e. the application of two variables), which decompose a data structure into its parts. We propose a static type system for a calculus that captures this feature, combining constants as types, union types and recursive types. The fundamental properties of Subject Reduction and Progress are addressed to guarantee well-behaved dynamics; they rely crucially on a novel notion of pattern compatibility. We also introduce an efficient type-checking algorithm by formulating a syntax-directed variant of the type system. This involves algorithms for checking type equivalence and subtyping, both based on coinductive characterizations of those relations.
Software:
cap-typecheckingReferences:
| [1] | Amadio, R. M.; Cardelli, L., Subtyping recursive types, ACM Trans. Program. Lang. Syst., 15, 4, 575-631 (1993) |
| [2] | Ariola, Z. M.; Klop, J. W., Equational term graph rewriting, Fund. Inform., 26, 3/4, 207-240 (1996) · Zbl 0854.68049 |
| [3] | Ayala-Rincón, M.; Bonelli, E.; Edi, J.; Viso, A. (2017), Typed path polymorphism. Extended report · Zbl 1423.68089 |
| [4] | Ayala-Rincón, M.; Bonelli, E.; Viso, A., Type soundness for path polymorphism, Electron. Notes Theor. Comput. Sci., 323, 235-251 (2016) · Zbl 1390.68170 |
| [5] | Barendregt, H. P.; Dekkers, W.; Statman, R., Lambda Calculus with Types. Perspectives in Logic (2013), Cambridge University Press · Zbl 1347.03001 |
| [6] | Brandt, M.; Henglein, F., Coinductive axiomatization of recursive type equality and subtyping, (de Groote, P., Proceedings of the TLCA ’97. Proceedings of the TLCA ’97, Nancy, France, April 2-4, 1997. Proceedings of the TLCA ’97. Proceedings of the TLCA ’97, Nancy, France, April 2-4, 1997, Lecture Notes in Computer Science, vol. 1210 (1997), Springer), 63-81 · Zbl 1063.03510 |
| [7] | Brandt, M.; Henglein, F., Coinductive axiomatization of recursive type equality and subtyping, Fund. Inform., 33, 4, 309-338 (1998) · Zbl 0902.68105 |
| [8] | Cardelli, L.; Martini, S.; Mitchell, J. C.; Scedrov, A., An extension of system F with subtyping, (Ito, T.; Meyer, A. R., Proceedings of the TACS ’91. Proceedings of the TACS ’91, Sendai, Japan, September 24-27, 1991. Proceedings of the TACS ’91. Proceedings of the TACS ’91, Sendai, Japan, September 24-27, 1991, Lecture Notes in Computer Science, vol. 526 (1991), Springer), 750-770 · Zbl 1496.03058 |
| [9] | Cardone, F., An algebraic approach to the interpretation of recursive types, (Raoult, J.-C., CAAP. CAAP, Lecture Notes in Computer Science, vol. 581 (1992), Springer), 66-85 |
| [10] | Cirstea, H.; Kirchner, C., The rewriting calculus – part I and II, Log. J. IGPL, 9, 3, 339-410 (2001) · Zbl 0986.03027 |
| [11] | Colazzo, D.; Ghelli, G., Subtyping recursion and parametric polymorphism in kernel fun, Inform. and Comput., 198, 2, 71-147 (2005) · Zbl 1156.68331 |
| [12] | Comon, H.; Dauchet, M.; Gilleron, R.; Jacquemard, F.; Lugiez, D.; Löding, C.; Tison, S.; Tommasi, M., Tree automata techniques and applications (2008) |
| [13] | Courcelle, B., Fundamental properties of infinite trees, Theoret. Comput. Sci., 25, 95-169 (1983) · Zbl 0521.68013 |
| [14] | Di Cosmo, R.; Pottier, F.; Rémy, D., Subtyping recursive types modulo associative commutative products, (Urzyczyn, P., Proceedings of the TLCA 2005. Proceedings of the TLCA 2005, Nara, Japan, April 21-23, 2005. Proceedings of the TLCA 2005. Proceedings of the TLCA 2005, Nara, Japan, April 21-23, 2005, Lecture Notes in Computer Science, vol. 3461 (2005), Springer), 179-193 · Zbl 1114.68029 |
| [15] | Downey, P. J.; Sethi, R.; Tarjan, R. E., Variations on the common subexpression problem, J. ACM, 27, 4, 758-771 (1980) · Zbl 0458.68026 |
| [16] | Edi, J.; Viso, A., Prototype implementation of efficient type-checker in scala (2016) |
| [17] | Edi, J.; Viso, A.; Bonelli, E., Efficient type checking for path polymorphism, (Uustalu, T., 21st International Conference on Types for Proofs and Programs. 21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia. 21st International Conference on Types for Proofs and Programs. 21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia, LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, vol. 69 (2015)), 6:1-6:23 · Zbl 1433.68094 |
| [18] | Jay, B., Pattern Calculus - Computing with Functions and Structures (2009), Springer · Zbl 1215.68055 |
| [19] | Jay, B.; Kesner, D., Pure pattern calculus, (Sestoft, P., ESOP. ESOP, Lecture Notes in Computer Science, vol. 3924 (2006), Springer), 100-114 · Zbl 1178.03039 |
| [20] | Jay, B.; Kesner, D., First-class patterns, J. Funct. Programming, 19, 2, 191-225 (2009) · Zbl 1163.68315 |
| [21] | Jim, T.; Palsberg, J., Type Inference in Systems of Recursive Types with Subtyping (1997) |
| [22] | Kahl, W., Basic pattern matching calculi: a fresh view on matching failure, (Kameyama, Y.; Stuckey, P. J., Proceedings of the Functional and Logic Programming, 7th International Symposium. Proceedings of the Functional and Logic Programming, 7th International Symposium, FLOPS 2004, Nara, Japan, April 7-9, 2004. Proceedings of the Functional and Logic Programming, 7th International Symposium. Proceedings of the Functional and Logic Programming, 7th International Symposium, FLOPS 2004, Nara, Japan, April 7-9, 2004, Lecture Notes in Computer Science, vol. 2998 (2004), Springer), 276-290 · Zbl 1122.68395 |
| [23] | Klop, J. W.; van Oostrom, V.; de Vrijer, R. C., Lambda calculus with patterns, Theoret. Comput. Sci., 398, 1-3, 16-31 (2008) · Zbl 1145.68012 |
| [24] | Kozen, D.; Palsberg, J.; Schwartzbach, M. I., Efficient recursive subtyping, Math. Structures Comput. Sci., 5, 1, 113-125 (1995) · Zbl 0840.03007 |
| [25] | Palsberg, J.; Zhao, T., Efficient and flexible matching of recursive types, Inform. and Comput., 171, 2, 364-387 (2001) · Zbl 1005.68043 |
| [26] | Petit, B., Semantics of typed lambda-calculus with constructors, Log. Methods Comput. Sci., 7, 1 (2011) · Zbl 1218.03019 |
| [27] | Pierce, B. C., Types and Programming Languages (2002), MIT Press · Zbl 0995.68018 |
| [28] | Vouillon, J., Subtyping union types, (Marcinkowski, J.; Tarlecki, A., CSL. CSL, Lecture Notes in Computer Science, vol. 3210 (2004), Springer), 415-429 · Zbl 1095.68026 |
| [29] | Zhao, T., Type Matching and Type Inference for Object-Oriented Systems (2002), Computer Science, Purdue University, Ph.D. thesis |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
