Подтвердить что ты не робот

Как работает Stream Fusion?

Единственными ресурсами в Stream Fusion, которые я могу найти, являются документы, представляющие его, которые на самом деле не являются лучшими источниками обучения. Как точно работает слияние потоков?

Более конкретно, поскольку эта часть paper не объясняла хорошо: как создаются со-структуры после списка → преобразование потока (т.е. maps f . maps g) сами складываются?

4b9b3361

ОТВЕТЫ

Ответ 1

Здесь определение maps из тезис Дункана Кутта (раздел 1.4.2):

maps :: (a → b) → Stream a → Stream b
maps f (Stream next0 s0) = Stream next s0
    where
        next s = case next0 s of
            Done → Done
            Skip s′ → Skip s′
            Yield x s′ → Yield (f x) s′

Теперь рассмотрим выражение

maps f . maps g

Компилятор может встроить (.), чтобы получить

\x -> maps f (maps g x)

Из определения Stream видно, что он имеет только один конструктор:

data Stream a = ∃ s . Stream (s → Step a s) s

Таким образом, предыдущий результат эквивалентен:

\(Stream next0 s) -> maps f (maps g (Stream next0 s))

Вложение maps g, что безопасно делать, поскольку maps не является рекурсивным (это ключевое понимание потока слияния):

\(Stream next0 s) -> maps f (Stream next1 s)
      where
          next1 s = case next0 s of
            Done → Done
            Skip s′ → Skip s′
            Yield x s′ → Yield (g x) s′

Вставка maps f:

\(Stream next0 s) -> Stream next2 s
      where
          next1 s = case next0 s of
            Done → Done
            Skip s′ → Skip s′
            Yield x s′ → Yield (g x) s′
          next2 s = case next1 s of
            Done → Done
            Skip s′ → Skip s′
            Yield x s′ → Yield (f x) s′

Далее мы можем встроить next1 в next2 и упростить выражения case с "case-of-case" - снова обратите внимание, что next1 не является рекурсивным - и удаляет теперь мертвый next1:

\(Stream next0 s) -> Stream next2 s
      where
          next2 s = case next0 s of
            Done → Done
            Skip s′ → Skip s′
            Yield x s′ → Yield (f (g x)) s′

Ключевым моментом является то, что эти шаги представляют собой небольшие небольшие оптимизации, которые имеют смысл в изоляции и которые не требуют специального знания компилятора самого слияния потоков или функции Stream или maps.