Ambivalent types for principal type inference with GADTs. (English) Zbl 1426.68046
Shan, Chung-chieh (ed.), Programming languages and systems. 11th Asian symposium, APLAS 2013, Melbourne, VIC, Australia, December 9–11, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8301, 257-272 (2013).
Summary: GADTs, short for generalized algebraic datatypes, which allow constructors of algebraic datatypes to be non-surjective, have many useful applications. However, pattern matching on GADTs introduces local type equality assumptions, which are a source of ambiguities that may destroy principal types-and must be resolved by type annotations. We introduce ambivalent types to tighten the definition of ambiguities and better confine them, so that type inference has principal types, remains monotonic, and requires fewer type annotations.
For the entire collection see [Zbl 1298.68034].
For the entire collection see [Zbl 1298.68034].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q65 | Abstract data types; algebraic specification |
References:
| [1] | Baars, A.I., Swierstra, S.D.: Typing dynamic typing. In: ICFP 2002: Proceedings of the 7th ACM SIGPLAN International Conference on Functional Programming, pp. 157-166. ACM Press (2002) · Zbl 1322.68035 |
| [2] | Cheney, J., Hinze, R.: First-class phantom types. Computer and Information Science Technical Report TR2003-1901, Cornell University (2003) |
| [3] | Garrigue, J.; Ueda, K., A certified implementation of ML with structural polymorphism, Programming Languages and Systems, 360-375 (2010), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-17164-2_25 |
| [4] | Garrigue, J.: Monomophic let in OCaml? (September 2013), Blog article at: http://gallium.inria.fr/blog/monomorphic_let/ |
| [5] | Garrigue, J.; Rémy, D., Semi-explicit first-class polymorphism for ML, Information and Computation, 155, 134-171 (1999) · Zbl 1045.68526 · doi:10.1006/inco.1999.2830 |
| [6] | Garrigue, J., Rémy, D.: Ambivalent types for principal type inference with GADTs (June 2013), Available electronically at http://gallium.inria.fr/ remy/gadts/ · Zbl 1426.68046 |
| [7] | Le Botlan, D.; Rémy, D., Recasting MLF, Information and Computation, 207, 6, 726-785 (2009) · Zbl 1167.68014 · doi:10.1016/j.ic.2008.12.006 |
| [8] | Leroy, X., Doligez, D., Frisch, A., Garrigue, J., Rémy, D., Vouillon, J.: The OCaml system release 4.00, Documentation and user’s manual. Projet Gallium, INRIA (July 2012) |
| [9] | Lin, C.-K.; Sheard, T., Pointwise generalized algebraic data types, Proceedings of the 5th ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI 2010, 51-62 (2010), New York: ACM, New York |
| [10] | Milner, R., A theory of type polymorphism in programming, Journal of Computer and System Sciences, 17, 348-375 (1978) · Zbl 0388.68003 · doi:10.1016/0022-0000(78)90014-4 |
| [11] | Pottier, F., Régis-Gianas, Y.: Stratified type inference for generalized algebraic data types. In: Proceedings of the 33rd ACM Symposium on Principles of Programming Languages (POPL 2006), Charleston, South Carolina, pp. 232-244 (January 2006) · Zbl 1369.68114 |
| [12] | Schrijvers, T.; Peyton Jones, S.; Sulzmann, M.; Vytiniotis, D., Complete and decidable type inference for gadts, Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming, ICFP 2009, 341-352 (2009), New York: ACM, New York · Zbl 1302.68190 |
| [13] | Sheard, T.; Linger, N.; Horváth, Z.; Plasmeijer, R.; Soós, A.; Zsók, V., Programming in Omega, Central European Functional Programming School, 158-227 (2008), Heidelberg: Springer, Heidelberg · Zbl 1170.68419 · doi:10.1007/978-3-540-88059-2_5 |
| [14] | Simonet, V., Pottier, F.: A constraint-based approach to guarded algebraic data types. ACM Transactions on Programming Languages and Systems 29(1) (January 2007) |
| [15] | Vytiniotis, D.; Peyton Jones, S.; Schrijvers, T.; Sulzmann, M., OutsideIn(X) Modular type inference with local assumptions, Journal of Functional Programming, 21, 4-5, 333-412 (2011) · Zbl 1262.68034 · doi:10.1017/S0956796811000098 |
| [16] | Xi, H.; Chen, C.; Chen, G., Guarded recursive datatype constructors, Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2003, 224-235 (2003), New York: ACM, New York · Zbl 1321.68161 · doi:10.1145/604131.604150 |
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.
