From c4d947cc808bf99a387cac2b33e7db69b4fbd1a9 Mon Sep 17 00:00:00 2001 From: Noel Welsh Date: Thu, 13 Jun 2024 11:30:34 +0100 Subject: [PATCH] Bibliography for codata --- src/bib/scala-with-cats.bib | 66 ++++++++++++++++++++++++++++++++- src/pages/codata/conclusions.md | 11 +++--- 2 files changed, 71 insertions(+), 6 deletions(-) diff --git a/src/bib/scala-with-cats.bib b/src/bib/scala-with-cats.bib index 43c75ed7..cb712da3 100644 --- a/src/bib/scala-with-cats.bib +++ b/src/bib/scala-with-cats.bib @@ -223,5 +223,69 @@ @article{10.1145/291251.289455 @Unpublished{mcbride01:deriv, author = {Conor McBride}, title = {The Derivative of a Regular Type is its Type of One-Hole Contexts}, - date = 2001, + year = 2001, url = {http://strictlypositive.org/diff.pdf}} + + +@article{HAGINO1989629, +title = {Codatatypes in ML}, +journal = {Journal of Symbolic Computation}, +volume = {8}, +number = {6}, +pages = {629-650}, +year = {1989}, +issn = {0747-7171}, +doi = {https://doi.org/10.1016/S0747-7171(89)80065-3}, +url = {https://www.sciencedirect.com/science/article/pii/S0747717189800653}, +author = {Tatsuya Hagino}, +abstract = {A new data type declaration mechanism of defining codatatypes is introduced to a functional programming language ML. Codatatypes are dual to datatypes for which ML already has a mechanism of defining. Sums and finite lists are defined as datatypes, but their duals, products and infinite lists, could not be defined in ML. This new facility gives ML the missing half of data types and makes ML symmetric. Categorical and domain-theoretic characterization of codatatypes are also given.} +} + +@inproceedings{downen2019codata, + title={Codata in action}, + author={Downen, Paul and Sullivan, Zachary and Ariola, Zena M and Peyton Jones, Simon}, + booktitle={European Symposium on Programming}, + pages={119--146}, + year={2019}, + organization={Springer International Publishing Cham}, + url={https://www.microsoft.com/en-us/research/uploads/prod/2020/01/CoDataInAction.pdf} +} + +@techreport {DRP-201905-Sullivan, + type = {Directed Research Project}, + author = {Zachary Sullivan}, + title = {Exploring Codata: The Relation to Object-Orientation}, + institution = {University of Oregon, Computer and Information Sciences Department}, + number = DRP-201905-Sullivan, + month = 5, + year = 2019, + url={https://www.cs.uoregon.edu/Reports/DRP-201905-Sullivan.pdf} +} + +@inproceedings{wadler1998add, + title={How to add laziness to a strict language without even being odd}, + author={Wadler, Philiip and Taha, Walid and MacQueen, David}, + booktitle={SML'98, The SML workshop}, + year={1998}, + url={https://www.diva-portal.org/smash/get/diva2:413532/FULLTEXT01.pdf} +} + +@article{DBLP:journals/corr/abs-2103-06913, + author = {Paul Downen and Zena M. Ariola}, + title = {Classical (Co)Recursion: Programming}, + journal = {CoRR}, + volume = {abs/2103.06913}, + year = {2021}, + url = {https://arxiv.org/abs/2103.06913}, + eprinttype = {arXiv}, + eprint = {2103.06913}, + timestamp = {Thu, 14 Oct 2021 09:14:34 +0200}, + biburl = {https://dblp.org/rec/journals/corr/abs-2103-06913.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@unpublished{kiselyov05:beyond, + author = {Oleg Kiselyov}, + title = {Beyond Church encoding: Boehm-Berarducci isomorphism of algebraic data types and polymorphic lambda-terms}, + year = 2005, + url = {https://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html}} diff --git a/src/pages/codata/conclusions.md b/src/pages/codata/conclusions.md index 3d981669..720f2573 100644 --- a/src/pages/codata/conclusions.md +++ b/src/pages/codata/conclusions.md @@ -6,9 +6,10 @@ We have two strategies for implementing methods using codata: structural corecur We saw that data is connected to codata via fold: any data can instead be implemented as codata with a single destructor that is the fold for that data. The reverse is also: we can enumerate all potential pairs of inputs and outputs of destructors to represent codata as data. However this does not mean that data and codata are equivalent. We have seen many examples of codata representing infinite structures, such as sets of all even numbers and streams of all natural numbers. We have also seen that data and codata offer different forms of extensibility: data makes it easy to add new functions, but adding new elements requires changing existing code, while it is easy to add new elements to codata but we change existing code if we add new functions. -The earliest reference I could find to codata in programming languages is [Codatatypes in ML]( https://www.sciencedirect.com/science/article/pii/S0747717189800653), which dates from 1989. This is much more recent than algebraic data, which I think explains why codata is relatively unknown. There are some excellent recent papers that deal with codata. I highly recommend [Codata in Action](https://www.microsoft.com/en-us/research/uploads/prod/2020/01/CoDataInAction.pdf), which inspired large portions of this chaper. [Exploring Codata: The Relation to Object-Orientation](https://www.cs.uoregon.edu/Reports/DRP-201905-Sullivan.pdf) is also worthwhile. -[How to Add Laziness to a Strict Language Without Even Being Odd] (http://hh.diva-portal.org/smash/record.jsf?pid=diva2%3A413532&dswid=-2514) is an older paper that discusses the implementation of streams, and in particular the difference between a not-quite-lazy-enough implementation they label odd and the version we saw, which they call even. These correspond to `Stream` and `LazyList` in the Scala standard library respectively. -[Classical (Co)Recursion: Programming](https://arxiv.org/pdf/2103.06913.pdf) is an interesting survey of corecursion in different languages, and covers many of the same examples that I used here. -Finally, if you really want to get into the weeds of the relationship between data and codata, [Beyond Church encoding: Boehm-Berarducci isomorphism of algebraic data types and polymorphic lambda-terms]( https://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html) is for you. - +The earliest reference I could find to codata in programming languages is @HAGINO1989629. This is much more recent than algebraic data, which I think explains why codata is relatively unknown. There are some excellent recent papers that deal with codata. +I highly recommend *Codata in Action* [@downen2019codata], which inspired large portions of this chapter. +*Exploring Codata: The Relation to Object-Orientation* [@DRP-201905-Sullivan] is also worthwhile. +*How to Add Laziness to a Strict Language Without Even Being Odd* [@wadler1998add] is an older paper that discusses the implementation of streams, and in particular the difference between a not-quite-lazy-enough implementation they label odd and the version we saw, which they call even. These correspond to `Stream` and `LazyList` in the Scala standard library respectively. +*Classical (Co)Recursion: Programming* [@DBLP:journals/corr/abs-2103-06913] is an interesting survey of corecursion in different languages, and covers many of the same examples that I used here. +Finally, if you really want to get into the weeds of the relationship between data and codata, *Beyond Church encoding: Boehm-Berarducci isomorphism of algebraic data types and polymorphic lambda-terms* [@kiselyov05:beyond] is for you.