Как эффективно преобразовать индуктивный тип в коиндуктивный тип (без рекурсии)?

Question

> {-# LANGUAGE DeriveFunctor, Rank2Types, ExistentialQuantification #-}

Любой индуктивный тип определяется так

> newtype Ind f = Ind {flipinduct :: forall r. (f r -> r) -> r}
> induction = flip flipinduct

induction имеет тип (f a -> a) -> Ind f -> a, Существует двойное понятие, называемое коиндукция.

> data CoInd f = forall r. Coinduction (r -> f r) r
> coinduction = Coinduction

coinduction имеет тип (a -> f a) -> a -> CoInd f, Обратите внимание, как induction а также coinduction являются двойственными. В качестве примера индуктивных и коиндуктивных типов данных рассмотрим этот функтор.

> data StringF rec = Nil | Cons Char rec deriving Functor

Без рекурсии, Ind StringF является конечной строкой и CoInd StringF является конечной или бесконечной строкой (если мы используем рекурсию, они обе являются конечными или бесконечными или неопределенными строками). В общем, можно конвертировать Ind f -> CoInd f для любого функтора f, Например, мы можем обернуть значение функтора в коиндуктивный тип

> wrap :: (Functor f) => f (CoInd f) -> CoInd f
> wrap fc = coinduction igo Nothing where
>   --igo :: Maybe (CoInd f) -> f (Maybe (CoInd f))
>   igo Nothing  = fmap Just fc
>   igo (Just (Coinduction step seed)) = fmap (Just . Coinduction step) $ step seed

Эта операция добавляет дополнительную операцию (сопоставление с образцом Maybe) за каждый шаг. Это означает, что это дает O(n) накладные расходы.

Мы можем использовать индукцию на Ind f а также wrap получить CoInd f,

> convert :: (Functor f) => Ind f -> CoInd f
> convert = induction wrap

Это O(n^2), (Получение первого слоя O(1), но n-й элемент O(n) из-за вложенного Maybe с, делая это O(n^2) итого.) Вдвойне мы можем определить cowrap, который принимает индуктивный тип и раскрывает свой верхний слой Functor.

> cowrap :: (Functor f) => Ind f -> f (Ind f)
> cowrap = induction igo where
>    --igo :: f (f (Ind f)) -> f (Ind f)
>    igo = fmap (\fInd -> Ind $ \fold -> fold $ fmap (`flipinduct` fold) fInd)

induction всегда O(n) так же cowrap,

Мы можем использовать coinduction производить CoInd f от cowrap а также Ind f,

> convert' :: (Functor f) => Ind f -> CoInd f
> convert' = coinduction cowrap

Это опять O(n) каждый раз, когда мы получаем элемент, в общей сложности O(n^2),

---

Мой вопрос, без использования рекурсии (прямо или косвенно), можем ли мы конвертировать Ind f в CoInd f в O(n) время?

Я знаю как это сделать с помощью рекурсии (конвертировать Ind f в Fix f а потом Fix f в CoInd f (первоначальное преобразование O(n), но тогда каждый элемент из CoInd f является O(1), делая второе преобразование O(n) всего и O(n) + O(n) = O(n))), но я хотел бы увидеть, если это возможно без.

Соблюдайте это convert а также convert' никогда не использовал рекурсию, прямо или косвенно. Отлично, не так ли?

Answer 1

Да, это формально возможно:

https://github.com/jyp/ControlledFusion/blob/master/Control/FixPoints.hs

Однако преобразование все еще требует создания промежуточного буфера, который может быть выполнен только с использованием цикла, во время выполнения.

Причина, лежащая в основе этого ограничения, заключается в том, что значение "индуктивного" типа отвечает заданному порядку оценки (*), в то время как значение "коиндуктивного" типа фиксирует порядок оценки. Единственный способ сделать возможным переход без принудительного повторного вычисления - это выделить какой-то промежуточный буфер для запоминания промежуточных результатов.

Кстати, преобразование из "коиндуктивного" в "индуктивное" не требует буфера, но требует пересчета порядка оценки с помощью явного цикла.

Кстати, я изучил основные концепции в двух статьях: 1. В Haskell для эффективных потоков: https://gist.github.com/jyp/fadd6e8a2a0aa98ae94d2. В классической линейной логике - для массивов и потоков. http://lopezjuan.com/limestone/vectorcomp.pdf

(*) Это предполагает строгий язык. Ситуация немного меняется при ленивой оценке, но концепции и окончательный ответ совпадают. Есть несколько комментариев о ленивой оценке в исходном коде.