Abstract
The efficient representation and manipulation of data is one of the fundamental tasks in the construction of large software systems. Parametric polymorphism has been one of the most successful approaches to date but, as of yet, has not been applicable to programming with quotient datatypes such as unordered pairs, cyclic lists, bags etc. This paper provides the basis for writing polymorphic programs over quotient datatypes by extending our recently developed theory of containers.
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.
References
Abbott, M.: Categories of Containers. PhD thesis, University of Leicester (2003)
Abbott, M., Altenkirch, T., Ghani, N.: Categories of containers. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 23–38. Springer, Heidelberg (2003a)
Abbott, M., Altenkirch, T., Ghani, N., McBride, C.: Derivatives of containers. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol. 2701, pp. 16–30. Springer, Heidelberg (2003b)
Altenkirch, T., McBride, C.: Generic programming within dependently typed programming. In: Generic Programming, 2003. Proceedings of the IFIP TC2 Working Conference on Generic Programming (2003)
Bainbridge, E.S., Freyd, P.J., Scedrov, A., Scott, P.J.: Functorial polymorphism, preliminary report. In: Huet, G. (ed.) Logical Foundations of Functional Programming, ch. 14, pp. 315–327. Addison-Wesley, Reading (1990)
Borceux, F.: Handbook of Categorical Algebra. Encyclopedia of Mathematics. CUP (1994)
Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding (extended abstract). In: Proc. 14th LICS Conf., pp. 193–202. IEEE, Computer Society Press, Los Alamitos (1999)
Fiore, M.P., Leinster, T.: Objects of categories as complex numbers. Advances in Mathematics (2004) (to appear)
Hofmann, M.: On the interpretation of type theory in locally cartesian closed categories. In: CSL, pp. 427–441 (1994)
Hofmann, M.: A simple model of quotient types. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 216–234. Springer, Heidelberg (1995)
Jacobs, B.: Categorical Logic and Type Theory, vol. 141. Elsevier, Amsterdam (1999)
Jay, C.B.: A semantics for shape. Science of Computer Programming 25, 251–283 (1995)
Jay, C.B., Cockett, J.R.B.: Shapely types and shape polymorphism. In: Sannella, D. (ed.) ESOP 1994. LNCS, vol. 788, pp. 302–316. Springer, Heidelberg (1994)
Joyal, A.: Foncteurs analytiques et espéces de structures. In: Combinatoire énumérative. LNM, vol. 1234, pp. 126–159 (1986)
Mac Lane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics, vol. 5. Springer, Heidelberg (1971)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abbott, M., Altenkirch, T., Ghani, N., McBride, C. (2004). Constructing Polymorphic Programs with Quotient Types. In: Kozen, D. (eds) Mathematics of Program Construction. MPC 2004. Lecture Notes in Computer Science, vol 3125. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27764-4_2
Download citation
DOI: https://doi.org/10.1007/978-3-540-27764-4_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22380-1
Online ISBN: 978-3-540-27764-4
eBook Packages: Springer Book Archive