全機能的言語におけるストリーム融合

私が理解するように、ストリーム融合は、変換操作(colists)のリストへの変換、データと変換への冗長なcodataの最適化、ストリームの操作の融合、最後に結果のストリームのリストへの変換を行うことができます。

データからコードへの変換はトータルの動作ですが、逆の動作はありません。全機能プログラミング言語でストリーム融合の最適化は不可能ですか?

ベストアンサー

  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.

返信を残す

メールアドレスが公開されることはありません。 * が付いている欄は必須項目です