Как эффективно преобразовать индуктивный тип в коиндуктивный тип (без рекурсии)?
> {-# 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. Существует двойное понятие, называемое coinduction.
> 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 - конечная или бесконечная строка (если мы используем рекурсию, они являются как конечными, так и бесконечными или undefined). В общем случае можно преобразовать Ind f -> CoInd f для любого Functor 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 s, что делает это O(n^2) total.)
Двойственно мы можем определить 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) total и O(n) + O(n) = O(n))), но я хотел бы видеть, возможно ли его без.
Обратите внимание, что convert и convert' никогда не использовали рекурсию, прямо или косвенно. Нифти, не так ли?
Ответы
Ответ 1
Да, это формально возможно:
https://github.com/jyp/ControlledFusion/blob/master/Control/FixPoints.hs
Однако преобразование по-прежнему требует создания промежуточного буфера, который может выполняться только с помощью цикла во время выполнения.
Причина, лежащая в основе этого ограничения, заключается в том, что значение "индуктивного" типа отвечает на заданный порядок оценки (*), а значение "коиндуктивного" типа фиксирует порядок оценки. Единственный способ сделать переход возможным без принуждения многих повторных вычислений состоит в том, чтобы выделить некоторый промежуточный буфер для memoize промежуточных результатов.
Кстати, переход от "коиндуктивного" к "индуктивному" не требует никакого буфера, но требует повторения порядка оценки с использованием явного цикла.
Кстати, я изучил основные понятия в двух статьях:
1. В Haskell для эффективных потоков: https://gist.github.com/jyp/fadd6e8a2a0aa98ae94d
2. В классической линейной логике для массивов и потоков. http://lopezjuan.com/limestone/vectorcomp.pdf
(*) Это предполагает строгий язык. Вещи немного меняются в присутствии ленивой оценки, но концепции и окончательный ответ одинаковы. В исходном коде есть несколько комментариев относительно ленивой оценки.
