Эквивалентен ли тип потоковых данных потокового пакета FreeT?

Question

Пакет streaming определяет тип Stream, который выглядит следующим образом:

data Stream f m r
  = Step !(f (Stream f m r))
 | Effect (m (Stream f m r))
 | Return r

Существует комментарий к типу Stream, которыйговорит следующее:

Тип данных Stream эквивалентен FreeT и может представлять любую эффективную последовательность шагов, где форма шагов или «команд»определяется первым (functor) параметром.

Мне интересно, как тип Stream эквивалентен FreeT?

Вот определение FreeT:

data FreeF f a b = Pure a | Free (f b)
newtype FreeT f m a = FreeT { runFreeT :: m (FreeF f a (FreeT f m a)) }

Похоже, что невозможно создать изоморфизм между этими двумя типами.

Если говорить точнее, я не вижу способа написать следующие две функции, которыеделает их изоморфизмом:

freeTToStream :: FreeT f m a -> Stream f m a
streamToFreeT :: Stream f m a -> FreeT f m a

Например, я не уверен, как выразить значение типа Return "hello" :: Stream f m String как FreeT.

Я думаю, это можно сделать такследующее, но Pure "hello" обязательно будет заключено в m, а в Return "hello" :: Stream f m String это не так:

FreeT $ pure $ Pure "hello" :: Applicative m => FreeT f m a

---

Можно ли считать Stream эквивалентным FreeT, даже если представляется невозможным создать изоморфизм между ними?

Answer 1

Ваш пример с Return и мой пример с вложенными конструкторами Effect не могут быть представлены FreeT с теми же параметрами f и m.Есть и другие контрпримеры.Основную разницу в типах данных лучше всего увидеть в волнообразном пространстве, где конструкторы данных удаляются и допускаются бесконечные типы.

И Stream f m a, и FreeT f m a предназначены для вложения a введите внутри группы конструкторов типа f и m.Stream допускает произвольное вложение f и m, тогда как FreeT является более жестким.У него всегда есть внешний m.Он содержит либо f и еще один m и повторяется, либо a и заканчивается.

Но это не значит, что между типами нет какой-либо эквивалентности.Вы можете показать некоторую эквивалентность, показав, что каждый тип может быть точно встроен в другой.

Встраивание Stream в FreeT может быть выполнено в конце одного наблюдения: если вы выберете f' и m', так что конструкторы типа f и m являются необязательными на каждом уровне, вы можете смоделировать произвольную вложенность f и m.Один быстрый способ сделать это - использовать Data.Functor.Sum, а затем написать функцию:

streamToFreeT :: Stream f m a -> FreeT (Sum Identity f) (Sum Identity m) a
streamToFreeT = undefined -- don't have a compiler nearby, not going to even try

Обратите внимание, что у типа не будет необходимых экземпляров для работы.Это можно исправить, переключив Sum Identity на более прямой тип, который на самом деле имеет соответствующий экземпляр Monad.

Преобразование в обратном направлении не требует какой-либо хитрости при смене типа.Более ограниченная форма FreeT уже встраивается непосредственно в Stream.

Я бы сказал, что это делает документацию правильной, хотя, возможно, в ней следует использовать более точный термин, чем "эквивалентный".Все, что вы можете создать с одним типом, вы можете создать с другим - но может быть некоторая дополнительная интерпретация встраивания и изменения переменных.

Answer 2

Есть некоторые небольшие различия, которые делают их буквально не эквивалентными.В частности, FreeT обеспечивает чередование f и m,

FreeT f m a = m (Either a (f (FreeT f m a) = m (Either a (f (m (...))))
                                          -- m            f  m  -- alternating

, тогда как Stream допускает заикание, например, мы можем построить следующее без Step между двумя Effect:

Effect (return (Effect (return (Return r))))

, который должен быть эквивалентен в некотором смысле

Return r

Таким образом, мы возьмем частное Stream по следующим уравнениям, которые сглаживаютслои Effect:

Effect (m >>= \a -> return (Effect (k a))) = Effect (m >>= k)
Effect (return x) = x

При этом частном изоморфизмы

freeT_stream :: (Functor f, Monad m) => FreeT f m a -> Stream f m a
freeT_stream (FreeT m) = Effect (m >>= \case
  Pure r -> return (Return r)
  Free f -> return (Step (fmap freeT_stream f))

stream_freeT :: (Functor f, Monad m) => Stream f m a -> FreeT f m a
stream_freeT = FreeT . go where
  go = \case
    Step f -> return (Free (fmap stream_freeT f))
    Effect m -> m >>= go
    Return r -> return (Pure r)

Обратите внимание на цикл go, чтобы сгладить несколько конструкторов Effect.

---

Псевдозащищенность: (freeT_stream . stream_freeT) = id

Идем по индукции по потоку x.Если честно, я вытаскиваю гипотезы индукции из воздуха.Есть, конечно, случаи, когда индукция не применима.Это зависит от того, что такое m и f, и может также быть некоторая нетривиальная настройка, чтобы гарантировать, что этот подход имеет смысл для фактор-типа.Но все еще должно быть много конкретных m и f, где эта схема применима.Я надеюсь, что есть некоторая категорическая интерпретация, которая переводит это псевдозащищенность во что-то значимое.

(freeT_stream . stream_freeT) x
= freeT_stream (FreeT (go x))
= Effect (go x >>= \case
    Pure r -> return (Return r)
    Free f -> return (Step (fmap freeT_stream f)))

Случай x = Step f, гипотеза индукции (IH) fmap (freeT_stream . stream_freeT) f = f:

= Effect (return (Step (fmap freeT_stream (fmap stream_freeT f))))
= Effect (return (Step f))  -- by IH
= Step f  -- by quotient

Случай x = Return r

= Effect (return (Return r))
= Return r   -- by quotient

Кейс x = Effect m, гипотеза индукции m >>= (return . freeT_stream . stream_freeT)) = m

= Effect ((m >>= go) >>= \case ...)
= Effect (m >>= \x' -> go x' >>= \case ...)  -- monad law
= Effect (m >>= \x' -> return (Effect (go x' >>= \case ...)))  -- by quotient
= Effect (m >>= \x' -> (return . freeT_stream . stream_freeT) x')  -- by the first two equations above in reverse
= Effect m  -- by IH

---

Обратное движение влево в качестве упражнения.