Skip to content

Commit

Permalink
Bibliography for codata
Browse files Browse the repository at this point in the history
  • Loading branch information
noelwelsh committed Jun 13, 2024
1 parent c623e92 commit c4d947c
Show file tree
Hide file tree
Showing 2 changed files with 71 additions and 6 deletions.
66 changes: 65 additions & 1 deletion src/bib/scala-with-cats.bib
Original file line number Diff line number Diff line change
Expand Up @@ -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}}
11 changes: 6 additions & 5 deletions src/pages/codata/conclusions.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.

0 comments on commit c4d947c

Please sign in to comment.