Abstract
We present a typical synergy between dynamic types (dynamics) and generalised algebraic datatypes (GADTs). The former provides a clean approach to integrating dynamic typing in a statically typed language. It allows values to be wrapped together with their type in a uniform package, deferring type unification until run time using a pattern match annotated with the desired type. The latter allows for the explicit specification of constructor types, as to enforce their structural validity. In contrast to ADTs, GADTs are heterogeneous structures since each constructor type is implicitly universally quantified. Unfortunately, pattern matching only enforces structural validity and does not provide instantiation information on polymorphic types. Consequently, functions that manipulate such values, such as a type-safe update function, are cumbersome due to boilerplate type representation administration. In this paper we focus on improving such functions by providing a new GADT annotation via a natural synergy with dynamics. We formally define the semantics of the annotation and touch on novel other applications of this technique such as type dispatching and enforcing type equality invariants on GADT values.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abadi, M., Cardelli, L., Pierce, B., Plotkin, G.: Dynamic typing in a statically typed language. ACM Transactions on Programming Languages and Systems 13(2), 237–268 (1991)
Abadi, M., Cardelli, L., Pierce, B., Rémy, D., Taylor, R.: Dynamic typing in polymorphic languages. Journal of Functional Programming 5(1), 81–110 (1994)
Baars, A., Swierstra, D.: Typing dynamic typing. In: Peyton Jones, S. (ed.) Proceedings of the 7th International Conference on Functional Programming, ICFP 2002, Pittsburgh, PA, USA, pp. 157–166. ACM, New York (2002)
Cartwright, R., Donahue, J.: The semantics of lazy (and industrious) evaluation. In: Proceedings of the 2nd Symposium on LISP and Functional Programming, LFP 1982, Pittsburgh, PA, USA, pp. 253–264. ACM, New York (1982)
Cheney, J., Hinze, R.: A lightweight implementation of generics and dynamics. In: Chakravarty, M. (ed.) Proceedings of the 6th Haskell Workshop, Haskell ’02, Pittsburgh, PA, USA, pp. 90–104. ACM, New York (2002)
Cheney, J., Hinze, R.: First-class phantom types. Technical Report TR2003-1901, Cornell University (2003)
Johann, P., Ghani, N.: Foundations for structured programming with GADTs. In: Necula, G., Wadler, P. (eds.) Proceedings of the 35th Symposium on Principles of Programming Languages, POPL 2008, San Francisco, CA, USA, pp. 297–308. ACM, New York (2008)
Kiselyov, O., Lämmel, R., Schupke, K.: Strongly typed heterogeneous collections. In: Nilsson, H. (ed.) Proceedings of the 8th Haskell Workshop, Haskell 2004, Snowbird, UT, USA, pp. 96–107. ACM, New York (2004)
Läufer, K., Odersky, M.: Polymorphic type inference and abstract data types. ACM Transactions on Programming Languages and Systems 16(5), 1411–1430 (1994)
Peyton Jones, S.L., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unification-based type inference for GADTs. In: Lawall, J. (ed.) Proceedings of the 11th International Conference on Functional Programming, ICFP 2006, Portland, Oregon, USA, pp. 50–61. ACM, New York (2006)
Pil, M.: Dynamic types and type dependent functions. In: Koopman, P., Clack, C. (eds.) IFL 1999. LNCS, vol. 1868, pp. 169–185. Springer, Heidelberg (2000)
Schrijvers, T., Peyton Jones, S., Sulzmann, M., Vytiniotis, D.: Complete and decidable type inference for GADTs. In: Hutton, G., Tolmach, A. (eds.) Proceedings of the 14th International Conference on Functional Programming, ICFP 2009, Edinburgh, Scotland, pp. 341–352. ACM, New York (2009)
Vervoort, M., Plasmeijer, R.: Lazy dynamic input/output in the lazy functional language Clean. In: Trinder, P., Michaelson, G.J., Peña, R. (eds.) IFL 2003. LNCS, vol. 3145, pp. 101–117. Springer, Heidelberg (2004)
Xi, H., Chen, C., Chen, G.: Guarded recursive datatype constructors. In: Morrisett, G., Aiken, A. (eds.) Proceedings of the 30th Symposium on Principles of Programming Languages, POPL 2003, New Orleans, LA, USA, pp. 224–235. ACM, New York (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van Noort, T., Achten, P., Plasmeijer, R. (2010). A Typical Synergy. In: Morazán, M.T., Scholz, SB. (eds) Implementation and Application of Functional Languages. IFL 2009. Lecture Notes in Computer Science, vol 6041. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16478-1_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-16478-1_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16477-4
Online ISBN: 978-3-642-16478-1
eBook Packages: Computer ScienceComputer Science (R0)