[DanWaterworth]

Here's proof that the last two parts are isomorphic:

    to :: (a -> [b]) -> (a -> (forall r . (b -> r -> r) -> r -> r))
    to f a =
      h (f a)
     where
      h :: [b] -> (forall r . (b -> r -> r) -> r -> r)
      h b cons nil =
        case b of
          (x:xs) -> cons x (h xs cons nil)
          [] -> nil

    from :: (a -> (forall r . (b -> r -> r) -> r -> r)) -> (a -> [b])
    from f a = f a (:) []

[moomin]

Is this quite right? Sorry this is a bit vague/unclear, but what happens if you, say, call the reduction function, throw the result away and then call it again?

I ran this example through Clojure in let's write a transducer, and it plain doesn't work; I think the mapping given above works for all transducers that are actually valid, but I think the type definition allows for broken ones.

Again, I'm not sure & still learning, so please explain if I've gone wrong here.

[tel]

If you throw the result away in pure code then you may as well have never computed it: the second result holds only.

In an impure setting none of the math above holds.

Edit: note that this doesn't mean you have to throw away local or global state. You can recapture that by using state machine transformers or even Kleisli state machine transformers (although that gets pretty heavy!)

[moomin]

Aaah. Makes sense. I couldn't figure out why the reasoning seemed sound, but I had something that didn't match. It's because in Clojure, r has state itself.

[tel]

The fast way is to say that [b] is the initial algebra of the functor (Maybe . (b,)) and then note that initial algebras are representable as

    newtype Mu f = Mu (forall r . (f r -> r) -> r)

[DanWaterworth]

Interesting. I'm not well versed in these things yet, but I've seen:

    forall r . (f r -> r) -> r

before. Am I right in saying it's the type of a catamorphism? In which case, yes, it makes total sense that your `Mu` type is equivalent to the (possibly) more usual:

    newtype Mu f = Mu (f (Mu f))

[tel]

Yep! You can think of it as a "frozen catamorphism" or the "right half" of foldr when you specialize `f`.

The really fascinating part is that my Mu is equivalent to your Mu in Haskell... because it's Turing complete. In a world where least and greatest fixed points differ, in a world where data and codata differ, then Mu has a cousin Nu

    data Mu f = Mu (forall r . (f r -> r) -> r)
    data Nu f = forall r . Nu (r -> f r) r

where Mu generates the data and Nu generates the codata. You'll recognize Nu as a frozen anamorpism, of course.

If you want a total language, replace generalized fixed points with these two pairs of fixed points. Mu only lets you construct things finitely and tear them down with catamorphisms and Nu only lets you destruct things finitely which you've built with anamorphisms.

Even in Haskell you can treat certain uses of types as being data-like or codata-like by viewing them more preferentially through Mu or Nu---though you can always convert both to Fix

    newtype Fix f = Fix (f (Fix f))

[rebcabin]

I'd be grateful for a pointer to some fundamental background reading; I can only follow enough of your reasoning to be intrigued and committed to learning more :)

[tel]

I'm trying to write up a blog post about this now. A really good presentation focused on types and programming languages is available in the middle chapters of Practical Foundations for Programming Languages. I originally learned about it from studying Aczel's Antifoundation Axiom from Barwise and Moss' Vicious Circles[0]---in there you can get a much more mathematical foundationalist POV---but Harper's book is more direct.

[0]http://www.amazon.com/Vicious-Circles-Center-Language-Inform...

[NotAtWork]

Thank you.

That step had me really confused.