<ol>
<li><p>If all you have are are plain inductive and coinductive types, fusion is impossible, for the reason you point out.</p>
</li>
<li><p>However, it <em>is</em> possible if your type system supports <em>sized types</em>. These types let you track how big the elements of a type are. So you can use a coinductive representation, but instrument the type with size information, to guarantee that you can convert back to an inductive representation.</p>
<p>A reasonably gentle introduction to these ideas is in Hughes, Pareto and Sabry's paper <a href="https://www.cs.indiana.edu/%7Esabry/papers/reactive.ps" rel="noreferrer"><em>Proving the Correctness of Reactive Systems Using Sized Types</em></a>, and they have also recently been  <a href="https://agda.readthedocs.io/en/v2.5.2/language/sized-types.html" rel="noreferrer">implemented in Agda</a>.</p>
</li>
</ol>

CC BY-SA 4.0
2018-06-25T09:55:14.127Z
2018-06-25T09:55:14.127Z
2020-06-17T09:38:08.363Z
Neel Krishnaswami
<p>As I understand, <a href="http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.7401" rel="nofollow noreferrer">stream fusion</a> consists in converting operations on lists to operations on streams (colists), optimize redundant codata to data and back conversions, fuse operations on streams, and finally convert the resulting stream to a list again.</p>

<p>Data to codata conversion is a total operation, but the opposite is not. Is stream fusion optimization impossible in total functional programming languages?</p>

<functional-programming>
Stream fusion in total functional language
user3368561
# Stream fusion in total functional language

(Asked by: username_0 on 2018-06-22)

As I understand, [stream fusion](http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.7401) consists in converting operations on lists to operations on streams (colists), optimize redundant codata to data and back conversions, fuse operations on streams, and finally convert the resulting stream to a list again.

Data to codata conversion is a total operation, but the opposite is not. Is stream fusion optimization impossible in total functional programming languages?

**Tags:** functional-programming


---

## 1 answers

### Answer by username_1 on 2018-06-25. Score: 5 | Accepted answer

1. If all you have are are plain inductive and coinductive types, fusion is impossible, for the reason you point out.
2. However, it *is* possible if your type system supports *sized types*. These types let you track how big the elements of a type are. So you can use a coinductive representation, but instrument the type with size information, to guarantee that you can convert back to an inductive representation.

   A reasonably gentle introduction to these ideas is in Hughes, Pareto and Sabry's paper [*Proving the Correctness of Reactive Systems Using Sized Types*](https://www.cs.indiana.edu/%7Esabry/papers/reactive.ps), and they have also recently been [implemented in Agda](https://agda.readthedocs.io/en/v2.5.2/language/sized-types.html).


---

