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?

  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, and they have also recently been implemented in Agda.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.