type Transducer a b =
forall r . (b -> r -> r) -> (a -> r -> r)
(And I'm not claiming this is correct) then you can reasonably easily show that this is isomorphic to (a -> [b])
forall r . (b -> r -> r) -> (a -> r -> r)
forall r . (r -> b -> r) -> (r -> a -> r)
a -> (forall r . (r -> b -> r) -> r -> r) [non-obvious, but true]
a -> [b]
This is "obviously" the Kleisli category for [] so you get rich, rich structure here. If you want to include local state such as what's needed to implement `take` then you can do something like
data Fold i o where
Fold :: (i -> x -> x) -> x -> (x -> o) -> Fold i o
type Transducer a b = forall r . Fold b r -> Fold a r
If you're familiar with pure profunctor lenses then I can tell you that Fold is a Profunctor and thus these can be acted on by a lot of generalized lens combinators. This explains a lot of the richness.
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 (:) []
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.
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!)
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.
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:
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
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 :)
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.
