skip to main content
research-article

Copatterns: programming infinite structures by observations

Published: 23 January 2013 Publication History

Abstract

Inductive datatypes provide mechanisms to define finite data such as finite lists and trees via constructors and allow programmers to analyze and manipulate finite data via pattern matching. In this paper, we develop a dual approach for working with infinite data structures such as streams. Infinite data inhabits coinductive datatypes which denote greatest fixpoints. Unlike finite data which is defined by constructors we define infinite data by observations. Dual to pattern matching, a tool for analyzing finite data, we develop the concept of copattern matching, which allows us to synthesize infinite data. This leads to a symmetric language design where pattern matching on finite and infinite data can be mixed.
We present a core language for programming with infinite structures by observations together with its operational semantics based on (co)pattern matching and describe coverage of copatterns. Our language naturally supports both call-by-name and call-by-value interpretations and can be seamlessly integrated into existing languages like Haskell and ML. We prove type soundness for our language and sketch how copatterns open new directions for solving problems in the interaction of coinductive and dependent types.

Supplementary Material

JPG File (r1d1_talk5.jpg)
MP4 File (r1d1_talk5.mp4)

References

[1]
M. Abadi and L. Cardelli. A theory of primitive objects. Untyped and first-order systems. In M. Hagiya and J. Mitchell, editors, Theoretical Aspects of Computer Software, volume 789 of Lect. Notes in Comput. Sci., pages 296--320. Springer, 1994.
[2]
A. Abel. Mixed inductive/coinductive types and strong normalization. In Z. Shao, editor, Proc. of the 5th Asian Symp. on Programming Languages and Systems, APLAS 2007, volume 4807 of Lect. Notes in Comput. Sci., pages 286--301. Springer, 2007. ISBN 978--3--540--76636-0.
[3]
A. Abel. Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types. Electr. Proc. in Theor. Comp. Sci., 77: 1--11, 2012. Proceedings of FICS 2012.
[4]
Agda team. The Agda Wiki, 2012.
[5]
T. Altenkirch and N. A. Danielsson. Termination checking in the presence of nested inductive and coinductive types. Short note supporting a talk given at PAR 2010, Workshop on Partiality and Recursion in Interactive Theorem Provers, FLoC 2010, 2010.
[6]
J.-M. Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2 (3): 297--347, 1992.
[7]
G. Barthe, M. J. Frade, E. Giménez, L. Pinto, and T. Uustalu. Type-based termination of recursive definitions. Math. Struct. in Comput. Sci., 14 (1): 97--141, 2004.
[8]
N. Benton, G. M. Bierman, V. de Paiva, and M. Hyland. A term calculus for intuitionistic linear logic. In M. Bezem and J. F. Groote, editors, Proc. of the 1st Int. Conf. on Typed Lambda Calculi and Applications, TLCA'93, volume 664 of phLect. Notes in Comput. Sci., pages 75--90. Springer, 1993. ISBN 3--540--56517--5.
[9]
A. Chlipala. Certified Programming with Dependent Types. MIT Press, June 2012. Unpublished draft.
[10]
R. Cockett and T. Fukushima. About charity. Technical report, Department of Computer Science, The University of Calgary, June 1992. Yellow Series Report No. 92/480/18.
[11]
T. Coquand. Pattern matching with dependent types. In B. Nordström, K. Pettersson, and G. Plotkin, editors, Types for Proofs and Programs (TYPES'92), Båstad, Sweden, pages 71--83, 1992.
[12]
T. Coquand. Infinite objects in type theory. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs (TYPES'93), volume 806 of phLect. Notes in Comput. Sci., pages 62--78. Springer, 1993.
[13]
P.-L. Curien and H. Herbelin. The duality of computation. In Proc. of the 5th ACM SIGPLAN Int. Conf. on Functional Programming (ICFP 2000), SIGPLAN Notices 35(9), pages 233--243. ACM Press, 2000. ISBN 1--58113--202--6.
[14]
N. A. Danielsson and T. Altenkirch. Subtyping, declaratively. In C. Bolduc, J. Desharnais, and B. Ktari, editors, Proc. of the 10th Int. Conf. on Mathematics of Program Construction, MPC 2010, volume 6120 of phLect. Notes in Comput. Sci., pages 100--118. Springer, 2010. ISBN 978--3--642--13320--6.
[15]
J. Dunfield and B. Pientka. Case analysis of higher-order data. Electr. Notes in Theor. Comp. Sci., 228: 69--84, 2009.
[16]
E. Giménez. phUn Calcul de Constructions Infinies et son application a la vérification de systèmes communicants. PhD thesis, Ecole Normale Supérieure de Lyon, Dec. 1996. Thèse d'université.
[17]
H. Goguen, C. McBride, and J. McKinna. Eliminating dependent pattern matching. In K. Futatsugi, J.-P. Jouannaud, and J. Meseguer, editors, Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday, volume 4060 of phLect. Notes in Comput. Sci., pages 521--540. Springer, 2006. ISBN 3--540--35462-X.
[18]
J. Granström. Reference and Computation in Intuitionistic Type Theory. PhD thesis, Mathematical Logic, Uppsala University, 2009.
[19]
T. Hagino. A typed lambda calculus with categorical type constructors. In D. H. Pitt, A. Poigné, and D. E. Rydeheard, editors, Category Theory and Computer Science, volume 283 of phLect. Notes in Comput. Sci., pages 140--157. Springer, 1987.
[20]
T. Hagino. Codatatypes in ML. phJ. Symb. Logic, 8 (6): 629--650, 1989.
[21]
J. Hughes, L. Pareto, and A. Sabry. Proving the correctness of reactive systems using sized types. In Proc. of the 23rd ACM Symp. on Principles of Programming Languages, POPL'96, pages 410--423, 1996.
[22]
INRIA. The Coq Proof Assistant Reference Manual. INRIA, version 8.3 edition, 2010.
[23]
J. Kennaway and F. de Vries. Infinitary Rewriting, volume 55 of phCambridge Tracts in Theoretical Computer Science, chapter Chapter 12 in Term Rewriting Systems, pages 668--711. Cambridge University Press, 2003.
[24]
D. Kimura and M. Tatsuta. Dual calculus with inductive and coinductive types. In R. Treinen, editor, Rewriting Techniques and Applications (RTA 2009), Brasília, Brazil, volume 5595 of Lect. Notes in Comput. Sci., pages 224--238. Springer, 2009. ISBN 978-3-642-02347-7.
[25]
N. R. Krishnaswami. Focusing on pattern matching. In Z. Shao and B. C. Pierce, editors, Proc. of the 36th ACM Symp. on Principles of Programming Languages, POPL 2009, pages 366--378. ACM Press, 2009. ISBN 978--1--60558--379--2.
[26]
D. R. Licata, N. Zeilberger, and R. Harper. Focusing on binding and computation. In F. Pfenning, editor, Proc. of the 23nd IEEE Symp. on Logic in Computer Science (LICS 2008), pages 241--252. IEEE Computer Soc. Press, 2008. ISBN 978-0--7695--3183-0. Long version available as Technical Report Carnegie Mellon University-CS-08--101.
[27]
C. McBride. Let's see how things unfold: Reconciling the infinite with the intensional. In A. Kurz, M. Lenisa, and A. Tarlecki, editors, 3rd Int. Conf. on Algebra and Coalgebra in Computer Science, CALCO 2009, volume 5728 of phLect. Notes in Comput. Sci., pages 113--126. Springer, 2009. ISBN 978--3--642-03740--5.
[28]
C. McBride and J. McKinna. The view from the left. J. Func. Program., 14 (1): 69--111, 2004.
[29]
R. Milner. A theory of type polymorphism in programming. J. Comput. Syst. Sci., 17: 348--375, Aug. 1978.
[30]
U. Norell. pTowards a Practical Programming Language Based on Dependent Type Theory. PhD thesis, Dept of Comput. Sci. and Engrg., Chalmers, Göteborg, Sweden, Sept. 2007.
[31]
N. Oury. Coinductive types and type preservation. Message on the coq-club mailing list, June 2008.
[32]
M. Parigot. Proofs of strong normalization for second order classical natural deduction. J. Symb. Logic, 62 (4): 1461--1479, 1997.
[33]
B. C. Pierce and D. N. Turner. Local type inference. In Proc. of the 25th ACM Symp. on Principles of Programming Languages, POPL'98, San Diego, California, 1998.
[34]
C. Schürmann and F. Pfenning. A coverage checking algorithm for LF. In D. Basin and B. Wolff, editors, Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003), volume 2758 of Lect. Notes in Comput. Sci., pages 120--135, Rome, Italy, September 2003. Springer.
[35]
A. Setzer. Coalgebras as types determined by their elimination rules. In P. Dybjer, S. Lindström, E. Palmgren, and G. Sundholm, editors, Epistemology versus ontology: Essays on the foundations of mathematics in honour of Per Martin-Löf. Springer, 2012. To appear.
[36]
C. Tuckey. Pattern matching in Charity. Master's thesis, The University of Calgary, July 1997.
[37]
J. Vouillon and P.-A. Melliès. Semantic types: A fresh look at the ideal model for types. In N. D. Jones and X. Leroy, editors, Proc. of the 31st ACM Symp. on Principles of Programming Languages, POPL 2004, pages 52--63. ACM Press, 2004. ISBN 1--58113--729-X.
[38]
P. Wadler. Call-by-value is dual to call-by-name. In C. Runciman and O. Shivers, editors, Proc. of the 8th ACM SIGPLAN Int. Conf. on Functional Programming (ICFP 2003), pages 189--201. ACM Press, 2003. ISBN 1--58113--756--7.
[39]
P. Wadler. Call-by-value is dual to call-by-name-reloaded. In J. Giesl, editor, Rewriting Techniques and Applications (RTA 2005), Nara, Japan, volume 3467 of Lect. Notes in Comput. Sci., pages 185--203. Springer, 2005. ISBN 3--540--25596--6.
[40]
A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115 (1): 38--94, 1994.
[41]
N. Zeilberger. Focusing and higher-order abstract syntax. In G. C. Necula and P. Wadler, editors, Proc. of the 35th ACM Symp. on Principles of Programming Languages, POPL 2008, pages 359--369. ACM Press, 2008. ISBN 978--1--59593--689--9.
[42]
N. Zeilberger. On the unity of duality. Ann. Pure Appl. Logic, 153 (1--3): 66--96, 2008.
[43]
N. Zeilberger. The Logical Basis of Evaluation Order and Pattern-Matching. PhD thesis, Carnegie Mellon University, 2009.

Cited By

View all
  • (2024)Grokking the Sequent Calculus (Functional Pearl)Proceedings of the ACM on Programming Languages10.1145/36746398:ICFP(395-425)Online publication date: 15-Aug-2024
  • (2024)Deriving Dependently-Typed OOP from First PrinciplesProceedings of the ACM on Programming Languages10.1145/36498468:OOPSLA1(983-1009)Online publication date: 29-Apr-2024
  • (2022)Introduction and elimination, left and rightProceedings of the ACM on Programming Languages10.1145/35476376:ICFP(438-465)Online publication date: 31-Aug-2022
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 48, Issue 1
POPL '13
January 2013
561 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2480359
Issue’s Table of Contents
  • cover image ACM Conferences
    POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
    January 2013
    586 pages
    ISBN:9781450318327
    DOI:10.1145/2429069
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013
Published in SIGPLAN Volume 48, Issue 1

Check for updates

Author Tags

  1. coinduction
  2. functional programming
  3. introduction vs. elimination
  4. message passing
  5. pattern matching

Qualifiers

  • Research-article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)93
  • Downloads (Last 6 weeks)10
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Grokking the Sequent Calculus (Functional Pearl)Proceedings of the ACM on Programming Languages10.1145/36746398:ICFP(395-425)Online publication date: 15-Aug-2024
  • (2024)Deriving Dependently-Typed OOP from First PrinciplesProceedings of the ACM on Programming Languages10.1145/36498468:OOPSLA1(983-1009)Online publication date: 29-Apr-2024
  • (2022)Introduction and elimination, left and rightProceedings of the ACM on Programming Languages10.1145/35476376:ICFP(438-465)Online publication date: 31-Aug-2022
  • (2022)Structural refinement typesProceedings of the 7th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3546196.3550163(15-27)Online publication date: 6-Sep-2022
  • (2021)Higher lensesProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470613(1-13)Online publication date: 29-Jun-2021
  • (2021)Cubical Agda: A dependently typed programming language with univalence and higher inductive typesJournal of Functional Programming10.1017/S095679682100003431Online publication date: 6-Apr-2021
  • (2020)Efficient lambda encodings for Mendler-style coinductive types in CedilleElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.317.5317(72-97)Online publication date: 1-May-2020
  • (2020)Transformations for Generating Type RefinementsFormal Methods. FM 2019 International Workshops10.1007/978-3-030-54997-8_24(371-387)Online publication date: 11-Aug-2020
  • (2019)Cubical agda: a dependently typed programming language with univalence and higher inductive typesProceedings of the ACM on Programming Languages10.1145/33416913:ICFP(1-29)Online publication date: 26-Jul-2019
  • (2019)Codata in ActionProgramming Languages and Systems10.1007/978-3-030-17184-1_5(119-146)Online publication date: 6-Apr-2019
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media