We argue that abstract datatypes — with public interfaces hiding private implementations — represent a form of codata rather than ordinary data, and hence that proof methods for corecursive programs are the appropriate techniques to use for reasoning with them. In particular, we show that the universal properties of unfold operators are perfectly suited for the task. We illustrate with solutions to two problems the solution to a problem in the recent literature.


Pattern Match Universal Property Proof Method Abstract Data Type Recursive Type 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bird, R.: Unfolding pointer algorithms. Journal of Functional Programming 11(3), 347–358 (2001)CrossRefzbMATHGoogle Scholar
  2. 2.
    Bird, R.S.: Introduction to Functional Programming Using Haskell. Prentice-Hall, Englewood Cliffs (1998)Google Scholar
  3. 3.
    Böhm, C., Berarducci, A.: Automatic synthesis of typed λ-programs on term algebras. Theoretical Computer Science 39, 135–154 (1985)CrossRefMathSciNetzbMATHGoogle Scholar
  4. 4.
    Bruce, K., Cardelli, L., Castagna, G.: The Hopkins Object Group, Gary T. Leavens, and Benjamin Pierce. On binary methods. Theory and Practice of Object Systems 1(3), 221–242 (1995)Google Scholar
  5. 5.
    Burton, F.W., Cameron, R.D.: Pattern matching with abstract data types. Journal of Functional Programming 3(2), 171–190 (1993)MathSciNetGoogle Scholar
  6. 6.
    Burton, W., Meijer, E., Sansom, P., Thompson, S., Wadler, P.: Views: An extension to Haskell pattern matching (October 1996),
  7. 7.
    Cockett, R., Fukushima, T.: About Charity. Department of Computer Science, University of Calgary (May 1992)Google Scholar
  8. 8.
    Cook, W.R.: Object-oriented programming versus abstract data types. In: de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1990. LNCS, vol. 489, pp. 151–178. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  9. 9.
    Coutts, D., Leshchinskiy, R., Stewart, D.: Stream fusion: From lists to streams to nothing at all. In: International Conference on Functional Programming, pp. 315–326 (2007)Google Scholar
  10. 10.
    Dijkstra, E.W.: The humble programmer. Communications of the ACM 15(10), 859–866 (1972), CrossRefGoogle Scholar
  11. 11.
    Emir, B., Odersky, M., Williams, J.: Matching Objects with Patterns. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 273–298. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  12. 12.
    Erwig, M.: Categorical Programming with Abstract Data Types. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol. 1548, pp. 406–421. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  13. 13.
    Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1995)Google Scholar
  14. 14.
    Gibbons, J.: Datatype-generic programming. In: Backhouse, R., Gibbons, J., Hinze, R., Jeuring, J. (eds.) SSDGP 2006. LNCS, vol. 4719. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  15. 15.
    Gibbons, J., Hutton, G.: Proof methods for corecursive programs. Fundamenta Informaticae 66(4), 353–366 (2005)MathSciNetzbMATHGoogle Scholar
  16. 16.
    Gibbons, J., Jones, G.: The under-appreciated unfold. In: International Conference on Functional Programming, Baltimore, Maryland, pp. 273–279 (September 1998)Google Scholar
  17. 17.
    Gill, A.: Cheap Deforestation for Non-strict Functional Languages. PhD thesis, Glasgow (1998)Google Scholar
  18. 18.
    Gill, A., Launchbury, J., Jones, S.P.: A short cut to deforestation. In: Functional Programming Languages and Computer Architecture (1993)Google Scholar
  19. 19.
    Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Tracts in Theoretical Computer Science, vol. 7. Cambridge University Press, Cambridge (1989), zbMATHGoogle Scholar
  20. 20.
    Goguen, J., Malcolm, G.: Hidden coinduction: Behavioural correctness proofs for objects. Mathematical Structures in Computer Science 9, 287–319 (1999)CrossRefMathSciNetzbMATHGoogle Scholar
  21. 21.
    Gordon, A.D.: A tutorial on co-induction and functional programming. In: Glasgow Workshop on Functional Programming (1994)Google Scholar
  22. 22.
    Howe, D.: Free on-line dictionary of computing (1993),
  23. 23.
    Jacobs, B.: Objects and classes, coalgebraically. In: Freitag, B., Jones, C.B., Lengauer, C., Schek, H.-J. (eds.) Object-Orientation with Parallelism and Persistence, pp. 83–103. Kluwer, Dordrecht (1996)Google Scholar
  24. 24.
    Jacobs, B.: Coalgebras in specification and verification for object-oriented languages. Newsletter of the Dutch Association for Theoretical Computer Science (NVTI) 3, 15–27 (1999)Google Scholar
  25. 25.
    Jacobs, B., Rutten, J.: A tutorial on (co)algebras and (co)induction. Bulletin of the European Association for Theoretical Computer Science (62), 222–259 (1997)zbMATHGoogle Scholar
  26. 26.
    Kamin, S.: Final data types and their specification. ACM Transactions on Programming Languages and Systems 5(1), 97–123 (1983)CrossRefzbMATHGoogle Scholar
  27. 27.
    R.B. Kieburtz.: Codata and comonads in Haskell. Oregon Graduate Institute (unpublished manuscript, 1999)Google Scholar
  28. 28.
    Läufer, K., Odersky, M.: An extension of ML with first-class abstract types. In: SIGPLAN Workshop on ML and its Applications (June 1992)Google Scholar
  29. 29.
    Läufer, K., Odersky, M.: Polymorphic type inference and abstract data types. ACM Transactions on Programming Languages and Systems 16(5), 1411–1430 (1994)CrossRefGoogle Scholar
  30. 30.
    Liskov, B., Zilles, S.: Programming with abstract data types. In: ACM SIGPLAN Symposium on Very High Level Languages, pp. 50–59. ACM Press, New York (1974)CrossRefGoogle Scholar
  31. 31.
    Mitchell, J.C.: On the equivalence of data representations. In: Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pp. 305–329. Academic Press Professional, Inc., San Diego (1991)Google Scholar
  32. 32.
    Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. ACM Transactions on Programming Languages and Systems 10(3), 470–502 (1988)CrossRefGoogle Scholar
  33. 33.
    Németh, L.: Catamorphism Based Program Transformations for Non-Strict Functional Languages. PhD thesis, Department of Computing Science, University of Glasgow (2000)Google Scholar
  34. 34.
    Okasaki, C.: Views for Standard ML. In: SIGPLAN Workshop in ML, pp. 14–23 (1998)Google Scholar
  35. 35.
    Gostanza, P.P., Peña, R., Núñez, M.: A new look at pattern matching in abstract data types. In: International Conference on Functional Programming, pp. 110–121. ACM Press, New York (1996)Google Scholar
  36. 36.
    Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)CrossRefGoogle Scholar
  37. 37.
    Parnas, D.L.: On the criteria to be used in decomposing systems into modules. Communications of the ACM 15(12), 1053–1058 (1972)CrossRefGoogle Scholar
  38. 38.
    Paterson, R.: Haskell hierarchical libraries: Data.Sequence (accessed, 2007),
  39. 39.
    Jones, S.P.: Explicit quantification in Haskell (1998),
  40. 40.
    Jones, S.P.: The Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, Cambridge (2003)Google Scholar
  41. 41.
    Jones, S.P.: View patterns: Lightweight views for Haskell (January 2007),
  42. 42.
    Jones, S.P., Tolmach, A., Hoare, T.: Playing by the rules: Rewriting as a practical optimisation technique in GHC. In: Hinze, R. (ed.) Haskell Workshop (2001)Google Scholar
  43. 43.
    Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)Google Scholar
  44. 44.
    Plotkin, G., Abadi, M.: A logic for parametric polymorphism. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 361–375. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  45. 45.
    Reichel, H.: An approach to object semantics based on terminal co-algebras. Mathematical Structures in Computer Science 5, 129–152 (1995)MathSciNetzbMATHCrossRefGoogle Scholar
  46. 46.
    Reynolds, J.C.: Towards a theory of type structure. In: Robinet, B. (ed.) Programming Symposium. LNCS, vol. 19, pp. 408–425. Springer, Heidelberg (1974)Google Scholar
  47. 47.
    Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Information Processing, vol. 83, pp. 513–523. Elsevier, Amsterdam (1983)Google Scholar
  48. 48.
    Svenningsson, J.: Shortcut fusion for accumulating parameters and zip-like functions. In: International Conference on Functional Programming (2002)Google Scholar
  49. 49.
    Syme, D., Neverov, G., Margetson, J.: Extensible pattern matching via a lightweight language extension. In: International Conference on Functional Programming, pp. 29–40 (2007)Google Scholar
  50. 50.
    Thompson, S.: Higher-order + polymorphic = reusable. Technical Report 224, University of Kent at Canterbury (May 1997),
  51. 51.
    Tullsen, M.: First Class Patterns. In: Pontelli, E., Santos Costa, V. (eds.) PADL 2000. LNCS, vol. 1753, pp. 1–15. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  52. 52.
    Turner, D.A.: Elementary strong functional programming. In: Hartel, P.H., Plasmeijer, R. (eds.) FPLE 1995. LNCS, vol. 1022. Springer, Heidelberg (1995)Google Scholar
  53. 53.
    Turner, D.A.: Total functional programming. Journal of Universal Computer Science 10(7), 751–768 (2004)MathSciNetGoogle Scholar
  54. 54.
    Ungar, D., Smith, R.B.: Self: The power of simplicity. In: Object-Oriented Programming: Systems, Languages and Applications, pp. 227–242 (1987)Google Scholar
  55. 55.
    Wadler, P.: A critique of Abelson and Sussman: Why calculating is better than scheming. SIGPLAN Notices 22(3), 8 (1987)CrossRefGoogle Scholar
  56. 56.
    Wadler, P.: Views: A way for mattern matching to cohabit with data abstraction. In: Principles of Programming Languages, pp. 307–313. ACM Press, New York (1987)Google Scholar
  57. 57.
    Wadler, P.: Theorems for free! In: Functional Programming Languages and Computer Architecture, pp. 347–359. ACM, New York (1989)CrossRefGoogle Scholar
  58. 58.
    Wadler, P.: Recursive types for free! (July 1990) (unpublished manuscript),
  59. 59.
    Wand, M.: Final algebra semantics and data type extensions. Journal of Computer and System Sciences 19, 27–44 (1979)CrossRefMathSciNetzbMATHGoogle Scholar
  60. 60.
    Wang, D.C., Murphy VII, T.: Programming with recursion schemes. Agere Systems/Carnegie Mellon University (unpublished manuscript, 2002)Google Scholar
  61. 61.
    Wang, M., Gibbons, J.: Translucent abstraction: Algebraic datatypes with safe views (April 2008) (submitted)Google Scholar
  62. 62.
    Wraith, G.: A note on categorical datatypes. In: Pitt, D.H., Rydeheard, D.E., Dyjber, P., Pitts, A.M., Poigné, A. (eds.) Category Theory and Computer Science. LNCS, vol. 389. Springer, Heidelberg (1989)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Jeremy Gibbons
    • 1
  1. 1.Computing LaboratoryOxford University 

Personalised recommendations