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.
