Functional pearl: Streams and unique fixed points
Streams, infinite sequences of elements, live in a coworld: they are given by a coinductive data type, operations on streams are implemented by corecursive programs, and proofs are conducted using coinduction. But there is more to it: suitably restricted, stream equations possess unique solutions, a...
| Main Author: | |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
2008
|
| _version_ | 1797070148515921920 |
|---|---|
| author | Hinze, R |
| author_facet | Hinze, R |
| author_sort | Hinze, R |
| collection | OXFORD |
| description | Streams, infinite sequences of elements, live in a coworld: they are given by a coinductive data type, operations on streams are implemented by corecursive programs, and proofs are conducted using coinduction. But there is more to it: suitably restricted, stream equations possess unique solutions, a fact that is not very widely appreciated. We show that this property gives rise to a simple and attractive proof technique essentially bringing equational reasoning to the coworld. In fact, we redevelop the theory of recurrences, finite calculus and generating functions using streams and stream operators building on the cornerstone of unique solutions. The development is constructive: streams and stream operators are implemented in Haskell, usually by one-liners. The resulting calculus or library, if you wish, is elegant and fun to use. Finally, we rephrase the proof of uniqueness using generalised algebraic data types. Copyright © 2008 ACM. |
| first_indexed | 2024-03-06T22:34:51Z |
| format | Journal article |
| id | oxford-uuid:5989fde2-afa7-422e-a961-f350c172f6eb |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T22:34:51Z |
| publishDate | 2008 |
| record_format | dspace |
| spelling | oxford-uuid:5989fde2-afa7-422e-a961-f350c172f6eb2022-03-26T17:10:16ZFunctional pearl: Streams and unique fixed pointsJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:5989fde2-afa7-422e-a961-f350c172f6ebEnglishSymplectic Elements at Oxford2008Hinze, RStreams, infinite sequences of elements, live in a coworld: they are given by a coinductive data type, operations on streams are implemented by corecursive programs, and proofs are conducted using coinduction. But there is more to it: suitably restricted, stream equations possess unique solutions, a fact that is not very widely appreciated. We show that this property gives rise to a simple and attractive proof technique essentially bringing equational reasoning to the coworld. In fact, we redevelop the theory of recurrences, finite calculus and generating functions using streams and stream operators building on the cornerstone of unique solutions. The development is constructive: streams and stream operators are implemented in Haskell, usually by one-liners. The resulting calculus or library, if you wish, is elegant and fun to use. Finally, we rephrase the proof of uniqueness using generalised algebraic data types. Copyright © 2008 ACM. |
| spellingShingle | Hinze, R Functional pearl: Streams and unique fixed points |
| title | Functional pearl: Streams and unique fixed points |
| title_full | Functional pearl: Streams and unique fixed points |
| title_fullStr | Functional pearl: Streams and unique fixed points |
| title_full_unstemmed | Functional pearl: Streams and unique fixed points |
| title_short | Functional pearl: Streams and unique fixed points |
| title_sort | functional pearl streams and unique fixed points |
| work_keys_str_mv | AT hinzer functionalpearlstreamsanduniquefixedpoints |