Abstract
Bundy and Richardson [4] developed a method for reasoning about functions manipulating lists which is based on separating shape from content, and then exploiting a mathematically convenient representation for expressing shape-only manipulations. Later, Prince et al. [7] extended the technique to other data structures, and gave it a more formal basis via the theory of containers. All these results are restricted to fully polymorphic functions. For example, functions using equality tests on list elements are out of reach. We remedy this situation by developing new abstractions and representations for less polymorphic functions. In Haskell speak, we extend the earlier approach to be applicable in the presence of (certain) type class constraints.
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
Abbott, M., Altenkirch, T., Ghani, N.: Categories of Containers. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 23–38. Springer, Heidelberg (2003)
Abbott, M., Altenkirch, T., Ghani, N.: Containers: Constructing strictly positive types. Theoretical Computer Science 342(1), 3–27 (2005)
Bernardy, J.-P., Jansson, P., Claessen, K.: Testing Polymorphic Properties. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 125–144. Springer, Heidelberg (2010)
Bundy, A., Richardson, J.: Proofs about Lists Using Ellipsis. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS, vol. 1705, pp. 1–12. Springer, Heidelberg (1999)
Jay, C.B.: A semantics for shape. Science of Computer Programming 25(2-3), 251–283 (1995)
Peyton Jones, S.L. (ed.): Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press (2003)
Prince, R., Ghani, N., McBride, C.: Proving Properties about Lists Using Containers. In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol. 4989, pp. 97–112. Springer, Heidelberg (2008)
Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Proc. of Information Processing, pp. 513–523. Elsevier (1983)
Wadler, P.: Theorems for free! In: Proc. of FPCA 1989, pp. 347–359. ACM (1989)
Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Proc. of POPL 1989, pp. 60–76. ACM (1989)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 IFIP International Federation for Information Processing
About this paper
Cite this paper
Seidel, D., Voigtländer, J. (2012). Proving Properties about Functions on Lists Involving Element Tests. In: Mossakowski, T., Kreowski, HJ. (eds) Recent Trends in Algebraic Development Techniques. WADT 2010. Lecture Notes in Computer Science, vol 7137. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28412-0_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-28412-0_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28411-3
Online ISBN: 978-3-642-28412-0
eBook Packages: Computer ScienceComputer Science (R0)