In the recursion-schemes
package the following types are defined:
newtype Fix f = Fix (f (Fix f))
newtype Mu f = Mu (forall a. (f a -> a) -> a)
Are they isomorphic? If so, how do you prove it?
In the recursion-schemes
package the following types are defined:
newtype Fix f = Fix (f (Fix f))
newtype Mu f = Mu (forall a. (f a -> a) -> a)
Are they isomorphic? If so, how do you prove it?
Copyright © 2021 Jogjafile Inc.
Yes, they are isomorphic in Haskell. See What is the difference between Fix, Mu and Nu in Ed Kmett's recursion scheme package for some additional remarks.
Let's begin by defining functions to perform the conversions:
To show those functions witness an isomorphism, we must show that:
From
Fix
and backOne of the directions of the isomorphism comes off somewhat more straightforwardly than the other:
The final passage above,
cata Fix t = t
, can be verified through the definition ofcata
:cata Fix t
, then, isFix (fmap (cata Fix) (unfix t))
. We can use induction to show it must bet
, at least for a finitet
(it gets more subtle with infinite structures -- see the addendum at the end of this answer). There are two possibilities to consider:unfix t :: f (Fix f)
is empty, having no recursive positions to dig into. In that case, it must be equal tofmap absurd z
for somez :: f Void
, and thus:unfix t
is not empty. In that case, we at least know thatfmap (cata Fix)
can't do anything beyond applyingcata Fix
on the recursive positions. The induction hypothesis here is that doing so will leave those positions unchanged. We then have:(Ultimately,
cata Fix = id
is a corollary ofFix :: f (Fix f) -> Fix x
being an initial F-algebra. Resorting directly to that fact in the context of this proof would probably be too much of a shortcut.)From
Mu
and backGiven
muToFix . fixToMu = id
, to prove thatfixToMu . muToFix = id
it suffices to prove either:that
muToFix
is injective, orthat
fixToMu
is surjective.Let's take the second option, and review the relevant definitions:
fixToMu
being surjective, then, means that, given any specificFunctor
f
, all functions of typeforall a. (f a -> a) -> a
can be defined as\alg -> cata alg t
, for some specifict :: Fix f
. The task, then, becomes cataloguing theforall a. (f a -> a) -> a
functions and seeing whether all of them can be expressed in that form.How might we define a
forall a. (f a -> a) -> a
function without leaning onfixToMu
? No matter what, it must involve using thef a -> a
algebra supplied as an argument to get ana
result. The direct route would be applying it to somef a
value. A major caveat is that, sincea
is polymorphic, we must be able to conjure saidf a
value for any choice ofa
. That is a feasible strategy as long asf
-values happen to exist. In that case, we can do:To make the notation clearer, let's define a type for things we can use to define
forall a. (f a -> a) -> a
functions:Besides the direct route, there is just one other possibility. Given that
f
is aFunctor
, if we somehow have anf (Moo f)
value we can apply the algebra twice, the first application being under the outerf
layer, viafmap
andfromMoo
:Considering that we can also make
forall a. (f a -> a) -> a
out off (Moo f)
values, it makes sense to add them as a case ofMoo
:Accordingly,
fromLayered
can be incorporated tofromMoo
:Note that, by doing so, we have sneakily moved from applying
alg
under onef
layer to recursively applyingalg
under an arbitrary number off
layers.Next, we can note an
f Void
value can be injected into theLayered
constructor:That means we don't actually need the
Empty
constructor:What about the
Empty
case infromMoo
? The only difference between the two cases is that, in theEmpty
case, we haveabsurd
instead of\moo -> fromMoo moo alg
. Since allVoid -> a
functions areabsurd
, we don't need a separateEmpty
case there either:A possible cosmetic tweak is flipping the
fromMoo
arguments, so that we don't need to write the argument tofmap
as a lambda:Or, more pointfree:
At this point, a second look at our definitions suggests some renaming is in order:
And there it is: all
forall a. (f a -> a) -> a
functions have the form\alg -> cata alg t
for somet :: Fix f
. Therefore,fixToMu
is surjective, and we have the desired isomorphism.Addendum
In the comments, a germane question was raised about the applicability of the induction argument in the
cata Fix t = t
derivation. At a minimum, the functor laws and parametricity ensure thatfmap (cata Fix)
won't create extra work (for instance, it won't enlarge the structure, or introduce additional recursive positions to dig into), which justifies why stepping into the recursive positions is all that matters in the inductive step of the derivation. That being so, ift
is a finite structure, the base case of an emptyf (Fix t)
will eventually be reached, and all is clear. If we allowt
to be infinite, however, we can keep descending endlessly,fmap
afterfmap
afterfmap
, without ever reaching the base case.The situation with infinite structures, though, is not as awful as it might seem at first. Laziness, which is what makes infinite structures viable in the first place, allows us to consume infinite structures lazily:
While the succession of recursive positions extends infinitely, we can stop at any point and get useful results out of the surrounding
ListF
functorial contexts. Such contexts, it bears repeating, are unaffected byfmap
, and so any finite segment of the structure we might consume will be unaffected bycata Fix
.This laziness reprieve reflects how, as mentioned elsewhere in this discussion, laziness collapses the distinction between the fixed points
Mu
,Fix
andNu
. Without laziness,Fix
is not enough to encode productive corecursion, and so we have to switch toNu
, the greatest fixed point. Here is a tiny demonstration of the difference: