How do I convert an inductive type into a coinductive type efficiently (without recursion)?

Question

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

Any inductive type is defined like so

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

induction has type (f a -> a) -> Ind f -> a. There is a dual concept to this called coinduction.

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

coinduction has type (a -> f a) -> a -> CoInd f. Notice how induction and coinduction are dual. As an example of inductive and coinductive datatypes, look at this functor.

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

Without recursion, Ind StringF is a finite string and CoInd StringF is a finite or infinite string (if we use recursion, they are both finite or infinite or undefined strings). In general, it is possible to convert Ind f -> CoInd f for any Functor f. For example, we can wrap a functor value around a coinductive type

> 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

This operation adds an extra operation (pattern matching Maybe) for each step. This means it gives O(n) overhead.

We can use induction on Ind f and wrap to get CoInd f.

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

This is O(n^2). (Getting the first layer is O(1), but the nth element is O(n) due to the nested Maybes, making this O(n^2) total.) Dually, we can define cowrap, which takes an inductive type, and reveals its top Functor layer.

> 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 is always O(n), so so is cowrap.

We can use coinduction to produce CoInd f from cowrap and Ind f.

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

This is again O(n) everytime we get an element, for a total of O(n^2).

---

My question is, without using recursion (directly or indirectly), can we convert Ind f to CoInd f in O(n) time?

I know how to do it with recursion (convert Ind f to Fix f and then Fix f to CoInd f (the initial conversion is O(n), but then each element from CoInd f is O(1), making the second conversion O(n) total, and O(n) + O(n) = O(n))), but I would like to see if its possible without.

Observe that convert and convert' never used recursion, directly or indirectly. Nifty, ain't it!

Doctrinaire

typo: "induction has type (f a -> a) -> Ind a -> a." Should be Ind f. – Torey

duals and curry confuse me, but isn't induction :: (f a -> a) -> (Ind a -> a) ≈ (f a -> a, Ind a) -> a, so shouldn't it's dual be either (Ind a -> a) -> (f a -> a) or a -> (f a -> a, Ind a)? – Torey

@Torey the outer -> is in the meta theory. Given any f-algebra f :: f a -> a, cata f :: Mu f -> a is the unique f-algebra homomorphism from the initial f-algebra (Mu f) to a. This is how you get (f a -> a) -> Mu f -> a. flip that and you can literally take that as the definition of Mu f! As for ana/coinduction, Given an f-coalgebra (f :: a -> f a), we have ana f :: a -> Nu f. So (a -> f a) -> a -> Nu f. The arrows that get turned around were 'f' and the cata f/ana f arrows, not the meta-theoretic ones. When you dualize the def. of monad to make comonad, same thing happens. – Firewarden

Edward KMETT: Thanks! – Torey

I have the funny feeling that if it's possible, it will use something relating to the "double reverse" technique, hiding some sort of seed in a functor. And it may only be possible for some functors, if at all. – Agleam

@Agleam Do you have a link to the "double reverse" technique? – Doctrinaire

@PyRulez, I'm being extremely vague. Please don't take it literally. I'm talking about a tail-recursive implementation of map as map = reverse . map' [] where {map' seed [] = seed; map' seed (x : xs) = map' (x : seed) xs}. – Agleam

Answer 1

Yes, this is formally possible:

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

However, the conversion still requires the construction of an intermediate buffer, which can only be done using a loop, at runtime.

The reason underlying this limitation is that a value of the 'inductive' type responds to a given order of evaluation (*), while the a value of the 'co-inductive' type fixes an order of evaluation. The only way to make the transition possible without forcing many re-computations is to allocate some kind of intermediate buffer, to memoize intermediate results.

By the way, the conversion from 'co-inductive' to 'inductive' requires no buffer, but requires reifing the evaluation order by using an explicit loop.

BTW, I have studied the underlying concepts in two papers: 1. In Haskell, for effectful streams: https://gist.github.com/jyp/fadd6e8a2a0aa98ae94d 2. In classical linear logic, for arrays and streams. http://lopezjuan.com/limestone/vectorcomp.pdf

(*) That's assuming a strict language. Things change a bit in presence of lazy evaluation, but the concepts and the final answer are the same. There are some comments about lazy evaluation in the source code.

Thaddeusthaddus

Can you explain why general recursion (in the form of Fix here) is required to construct and deconstruct that buffer? – Agleam

@dfeuer: this is simply because haskell concrete recursive structures can only be declared using general recursion. – Thaddeusthaddus

Is there a dual form of loop? (I like it because even though it uses general recursion, it does not use recursive types (ironically, this function could not be defined at all in a non-recursive environment, because I know a way to use it to produce Void.)) – Doctrinaire

@PyRulez: as far as I can tell the dual of loop is 'alloc'. – Thaddeusthaddus