research-article

Copatterns: programming infinite structures by observations

Authors:

Brigitte Pientka,

David Thibodeau,

Anton SetzerAuthors Info & Claims

POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 27 - 38

https://doi.org/10.1145/2429069.2429075

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)

Download
14.33 KB

MP4 File (r1d1_talk5.mp4)

Download
272.29 MB

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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[15]

J. Dunfield and B. Pientka. Case analysis of higher-order data. Electr. Notes in Theor. Comp. Sci., 228: 69--84, 2009.

Digital Library

[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.

Digital Library

[20]

T. Hagino. Codatatypes in ML. phJ. Symb. Logic, 8 (6): 629--650, 1989.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[28]

C. McBride and J. McKinna. The view from the left. J. Func. Program., 14 (1): 69--111, 2004.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[40]

A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115 (1): 38--94, 1994.

Digital Library

[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.

Digital Library

[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.

Digital Library

Cited By

Todorov IBach Poulsen CAlves SCockx J(2024)Modal μ-Calculus for Free in AgdaProceedings of the 9th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3678000.3678202(16-28)Online publication date: 28-Aug-2024
https://dl.acm.org/doi/10.1145/3678000.3678202
Downen P(2024)Call-by-Unboxed-ValueProceedings of the ACM on Programming Languages10.1145/36746548:ICFP(845-879)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674654
Binder DTzschentke MMüller MOstermann K(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
https://dl.acm.org/doi/10.1145/3674639
Show More Cited By

Index Terms

Copatterns: programming infinite structures by observations
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Data types and structures
        Patterns
        Recursion
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Program schemes
      2. Type structures

Recommendations

Wellfounded recursion with copatterns: a unified approach to termination and productivity
ICFP '13: Proceedings of the 18th ACM SIGPLAN international conference on Functional programming

In this paper, we study strong normalization of a core language based on System F-omega which supports programming with finite and infinite structures. Building on our prior work, finite data such as finite lists and trees are defined via constructors ...
Copatterns: programming infinite structures by observations
POPL '13

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 ...
Wellfounded recursion with copatterns: a unified approach to termination and productivity
ICFP '13

In this paper, we study strong normalization of a core language based on System F-omega which supports programming with finite and infinite structures. Building on our prior work, finite data such as finite lists and trees are defined via constructors ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

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

General Chair:
Roberto Giacobazzi
Università di Verona, Italy
,
Program Chair:
Radhia Cousot
École normale supérieure CNRS & INRIA, France

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

Copyright © 2013 ACM.

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]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '13

Sponsor:

SIGPLAN

POPL '13: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 23 - 25, 2013

Rome, Italy

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

96
Total Citations
View Citations
1,098
Total Downloads

Downloads (Last 12 months)88
Downloads (Last 6 weeks)6

Reflects downloads up to 21 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Todorov IBach Poulsen CAlves SCockx J(2024)Modal μ-Calculus for Free in AgdaProceedings of the 9th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3678000.3678202(16-28)Online publication date: 28-Aug-2024
https://dl.acm.org/doi/10.1145/3678000.3678202
Downen P(2024)Call-by-Unboxed-ValueProceedings of the ACM on Programming Languages10.1145/36746548:ICFP(845-879)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674654
Binder DTzschentke MMüller MOstermann K(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
https://dl.acm.org/doi/10.1145/3674639
Binder DSkupin ISüberkrüb TOstermann K(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
https://dl.acm.org/doi/10.1145/3649846
Allais GKeller GWang M(2024)Scoped and Typed Staging by EvaluationProceedings of the 2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation10.1145/3635800.3636964(83-93)Online publication date: 11-Jan-2024
https://dl.acm.org/doi/10.1145/3635800.3636964
Carbone MCastro-Perez DFerreira FGheri LJacobsen FMomigliano APadovani LScalas ATirore DVassor MYoshida NZackon D(2024)The Concurrent Calculi Formalisation BenchmarkCoordination Models and Languages10.1007/978-3-031-62697-5_9(149-158)Online publication date: 17-Jun-2024
https://dl.acm.org/doi/10.1007/978-3-031-62697-5_9
Yuan YGuest SGriffis EPotter HMoon DOmar C(2023)Live Pattern Matching with Typed HolesProceedings of the ACM on Programming Languages10.1145/35860487:OOPSLA1(609-635)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586048
Rioux NHuang XOliveira BZdancewic S(2023)A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈Proceedings of the ACM on Programming Languages10.1145/35712117:POPL(515-543)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571211
DOWNEN PARIOLA Z(2023)Classical (co)recursion: MechanicsJournal of Functional Programming10.1017/S095679682200016833Online publication date: 4-Apr-2023
https://doi.org/10.1017/S0956796822000168
Zúñiga ABel-Enguix G(2022)On Coevaluation Behavior and EquivalenceMathematics10.3390/math1020380010:20(3800)Online publication date: 14-Oct-2022
https://doi.org/10.3390/math10203800
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents