Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
As I understand, stream fusion 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?
If all you have are are plain inductive and coinductive types, fusion is impossible, for the reason you point out.
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, and they have also recently been implemented in Agda.
