Abstract
Many have recognized the need for genericity in programming and program transformation. Genericity over data types has been achieved with polymorphism. Genericity over type constructors, often called polytypism, is an area of active research. This paper proposes that another kind of genericity is needed: genericity over the length of tuples. Untyped languages allow for such genericity but typed languages do not (except for languages allowing dependent types). The contribution of this paper is to present the “zip calculus,” a typed lambda calculus that provides genericity over the length of tuples and yet does not require the full generality of dependent types.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This research was supported in part by NSF under Grant Number CCR-9706747.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Augustsson, L.: Cayenne — a language with dependent types. In: Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP 1998). ACM SIGPLAN Notices, vol. 34(1), pp. 239–250. ACM, New York (1999)
Barendregt, H.P.: Lambda calculi with types. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science. Oxford University Press, Oxford (1992)
Bird, R., de Moor, O.: Algebra of Programming. Prentice Hall, Englewood Cliffs (1997)
Gaster, B.R., Jones, M.P.: A polymorphic type system for extensible records and variants. Technical report NOTTCS-TR-96-3, University of Nottingham, Languages and Programming Group, Department of Computer Science, Nottingham NG7 2RD, UK (November 1996)
Hoogendijk, P.F.: A Generic Theory of Datatypes. PhD thesis, Dept. of Math. and Computing Science, Eindhoven Univ. of Technology (1997)
Hudak, P., Jones, S.P., Wadler, P.: Report on the programming language Haskell. SIGPLAN Notices 27(5) (May 1992)
Huet, G., Lang, B.: Proving and applying program transformations expressed with second order patterns. Acta Informatica 11, 31–55 (1978)
Jansson, P., Jeuring, J.: PolyP - a polytypic programming language extension. In: POPL 1997: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 470–482. ACM Press, New York (1997)
Jay, C.B., Bellè, G., Moggi, E.: Functorial ML. Journal of Functional Programming 8(6), 573–619 (1998)
Malcolm, G.R.: Data structures and program transformation. Science of Computer Programming 14, 255–279 (1990)
Malcolm, G.: Algebraic Data Types and Program Transformation. PhD thesis, University of Groningen (1990)
Meertens, L.: Algorithmics - towards programming as a mathematical activity. In: de Bakker, J.W., Hazewinkel, E.M., Lenstra, J.K. (eds.) Proceedings of the CWI Symposium on Mathematics and Computer Science, CWI Monographs. vol. 1, pp. 289–334. North-Holland, Amsterdam (1986)
Meijer, E., Fokkinga, M., Paterson, R.: Functional programming with bananas, lenses, envelopes and barbed wire. In: Hughes, J. (ed.) FPCA 1991. LNCS, vol. 523, pp. 124–144. Springer, Heidelberg (1991)
Ohori, A.: A polymorphic record calculus and its compilation. ACM Transactions on Programming Languages and Systems 17(6), 844–895 (1995)
Jones, S.P., Meijer, E.: Henk: a typed intermediate language. In: Proc. 1997 ACM SIGPLAN Workshop on Types in Compilation (TIC 1997), Amsterdam, The Netherlands (June 1997)
Tullsen, M.: First class patterns. In: Pontelli, E., Santos Costa, V. (eds.) PADL 2000. LNCS, vol. 1753, pp. 1–15. Springer, Heidelberg (2000)
Van Benthem Jutting, L.S., McKinna, J., Pollack, R.: Checking algorithms for pure type systems. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 19–61. Springer, Heidelberg (1994)
Wadler, P.: Theorems for free! In: Functional Programming Languages and Computer Architecture. Springer, Heidelberg (1989)
Wand, M.: Complete type inference for simple objects. In: Proc. IEEE Symp. on Logic in Computer Science, pp. 37–44 (1987); Corrigendum. In: Proc. IEEE Symp. on Logic in Computer Science, p. 132 (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tullsen, M. (2000). The Zip Calculus. In: Backhouse, R., Oliveira, J.N. (eds) Mathematics of Program Construction. MPC 2000. Lecture Notes in Computer Science, vol 1837. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722010_3
Download citation
DOI: https://doi.org/10.1007/10722010_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67727-7
Online ISBN: 978-3-540-45025-2
eBook Packages: Springer Book Archive