What is the difference between Fix, Mu and Nu in Ed Kmett's recursion scheme package

Question

In Ed Kmett's recursion-scheme package, there are three declarations:

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

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

data Nu f where 
  Nu :: (a -> f a) -> a -> Nu f

What is the difference between those three data types?

Eleanoreleanora

I don't know too much theory, but I gather that for more proofy languages, Mu is the least fixed point and Nu is the greatest fixed point. In Haskell, these three are all supposed to be equivalent (I believe). Note that it's super-easy to implement cata for Mu and ana for Nu. – Lorenzoloresz

Try to solve this kata codewars.com/kata/folding-through-a-fixed-point/haskell – Dodi

Answer 1

Mu represents a recursive type as its fold, and Nu represents it as its unfold. In Haskell, these are isomorphic, and are different ways to represent the same type. If you pretend that Haskell doesn't have arbitrary recursion, the distinction between these types becomes more interesting: Mu f is the least (initial) fixed point of f, and Nu f is its greatest (terminal) fixed point.

A fixed point of f is a type T an isomorphism between T and f T, i.e. a pair of inverse functions in :: f T -> T, out :: T -> f T. The type Fix just uses Haskell's built-in type recursion to declare the isomorphism directly. But you can implement in/out for both Mu and Nu.

For a concrete example, pretend for a moment that you can't write recursive values. The inhabitants of Mu Maybe , i.e. values :: forall r. (Maybe r -> r) -> r, are the naturals, {0, 1, 2, ...}; the inhabitants of Nu Maybe, i.e. values :: exists x. (x, x -> Maybe x), are the conaturals {0, 1, 2, ..., ∞}. Think about the possible values of these types to see why Nu Maybe has an extra inhabitant.

If you want to get some intuition for these types, it can be a fun exercise to implement the following without recursion (roughly in increasing order of difficulty):

• zeroMu :: Mu Maybe, succMu :: Mu Maybe -> Mu Maybe
• zeroNu :: Nu Maybe, succNu :: Nu Maybe -> Nu Maybe, inftyNu :: Nu Maybe
• muTofix :: Mu f -> Fix f, fixToNu :: Fix f -> Nu f
• inMu :: f (Mu f) -> Mu f, outMu :: Mu f -> f (Mu f)
• inNu :: f (Nu f) -> Nu f, outNu :: Nu f -> f (Nu f)

You can also try to implement these, but they require recursion:

• nuToFix :: Nu f -> Fix f, fixToMu :: Fix f -> Mu f

Mu f is the least fixed point, and Nu f is the greatest, so writing a function :: Mu f -> Nu f is very easy, but writing a function :: Nu f -> Mu f is hard; it's like swimming against the current.

(At one point I was meaning to write a more detailed explanation of these types, but it might be a little too long for this format.)

Osteal

Great explanation, thank you! Is there a sources (articles/papers/books) that explain it even more detailed? For example, analogues for term-level fix points and why Nu (as representation a recursive type as its fold) is least fixed point at type level. There is also important links between LFP and initial algebras and also between GFP and terminal coalgebra. – Magocsi

I'm sure I'm missing something, but Nu Maybe seems to have many more inhabitants - at least many that Haskell happily type-checks. For instance, Nu Just [], Nu Just "abcd", Nu (const Nothing) 42 all seem appropriately typed. What am I getting wrong? – Stoical

Wait. Conatural numbers? Is that a thing? – Indicant

Sergey Cherepanov: I don't know of one off-hand, though here's a proof of initiality using parametricity. The connection between initial algebras and initial fixed points is sometimes called Lambek's lemma. B. Mehta: In the same way that id :: forall a. a -> a can't distinguish between different inputs, the outside world can't distinguish between Nu Just [] and Nu Just 0. paulotorrens: It's at least an idiomatic name for this type, the one-point compactification of the naturals, for this reason. – Osteal

Updated link for the proof of initiality. – Osteal

Thanks for fun exercise! I uploaded my answer here if anyone is interested: gist.github.com/inamiy/7488380da6001cb0f778b59d9f7230cd – Denton