[Haskell-cafe] Re: Fixed-point operator (was: seq does not preclude parametricity)

[Robert Dockins]

On Sunday 28 January 2007 23:19, Matthew Brecknell wrote:
> On Wed, 24 Jan 2007 10:41:09 -0500, "Robert Dockins" wrote:
> > newtype Mu a = Roll { unroll :: Mu a -> a }
> >
> > omega :: a
> > omega = (\x -> (unroll x) x) (Roll (\x -> (unroll x) x))
> >
> > fix :: (a -> a) -> a
> > fix f = (\x -> f . (unroll x) x) (Roll (\x -> f . (unroll x) x)) omega
> >
> > ones :: [Int]
> > ones = fix (1:)
> >
> > fibs :: [Int]
> > fibs = fix (\f a b -> a : f b (a+b)) 0 1
>
> That's an interesting definition of fix that I haven't seen before,
> though I am a little puzzled by omega. Since I have an irrational fear
> of recursion, and I like to take every opportunity I get to cure it, I
> decided to take a closer look...
>
> I figure omgea is just a way to write _|_ as an anonymous lambda
> expression.

Yup.  If you type-erase it, you get the very familiar term:

(\x -> x x) (\x -> x x)

Which is the canonical non-terminating untyped lambda term.

> But that made me wonder what it's doing in the definition of 
> fix.

I like to think of fix as implementing the semantics of recursion via the 
ascending Kleene chain.  Kleene's fixpoint theorem says that:

least_fixpoint( f ) = least_upper_bound (f^i  _|_   |   i in N )

where f^i means f composed together i times.

If you run it out, you'll see that my definition of fix calculates something 
like:

(f . f . f . f  ... ) _|_

===

f (f (f (f ( ... _|_))))


> I can see that without it, fix would have the wrong type, since 
>
> type inference gives the x parameters the type (Mu(b->a)):
> > -- A bit like fix, except it's, erm...
> > broke :: (a -> a) -> b -> a
> > broke f = (\x -> f . unroll x x) (Roll (\x -> f . unroll x x))
>
> So omega consumes an argument that has unconstrained type, and which
> appears to be unused. It's perhaps easier to see the unused argument
>
> with fix rewritten in a more point-full style:
> > fix' f = (\x y -> f (unroll x x y)) (Roll (\x y -> f (unroll x x y)))
> > omega
>
> Performing the application, (fix' f) becomes (f(fix' f)), and so on.
>
> So, I think I follow how this fixed-point operator works, and it seems
> reasonable to use _|_ to consume an unused non-strict argument. But I
> find it mildly disturbing that this unused argument seems to appear out
> of nowhere.
>
> Then I noticed that rewriting fix without (.) seems to work just as well
> (modulo non-termination of the GHC inliner), and without the unused
>
> argument:
> > fix :: (a -> a) -> a
> > fix f = (\x -> f (unroll x x)) (Roll (\x -> f (unroll x x)))

This is another fine way to write it.

> Of course, the corollary is that I can introduce as many unused
>
> arguments as I want:
> > fix'' f = (\x -> (f.).(unroll x x)) (Roll (\x -> (f.).(unroll x x)))
> > omega omega fix''' f = (\x -> ((f.).).(unroll x x)) (Roll (\x ->
> > ((f.).).(unroll x x))) omega omega omega -- etc...
>
> This gave me a new way to approach the question of where the unused
> argument came from. Given a function (f) of appropriate type, I can
>
> write:
> > f :: a -> a
> > (f.) :: (b -> a) -> (b -> a)
> > ((f.).) :: (c -> b -> a) -> (c -> b -> a)
>
> And so on. Nothing strange here. But all of these functions can inhabit
>
> the argument type of fix, so:
> > fix :: (a -> a) -> a
> > fix f :: a
> > fix (f.) :: b -> a
> > fix ((f.).) :: c -> b -> a
>
> Those are some strange types, and I have found those unused arguments
> without reference to any particular implementation of fix. Thinking
> about it, (forall a b . b -> a) is no stranger than (forall a . a).
> Indeed, I think the only thing that can have type (forall a . a) is _|_.
> Likewise, I can't imagine anything other than the identity function
> having the type (forall a . a -> a), and it's not too hard to see where
> (fix id) would lead.
>
> So perhaps it's not the appearance of the unused argument in the above
> definition of the fixed-point operator, but the type of the fixed-point
> operator in general that is a bit strange. Certainly, I have always
> found fix to be mysterious, even though I am getting quite comfortable
> with using it.
>
> I'm wondering: Is any of this related to the preceding discussion about
> how fix affects parametricity? Can anyone recommend some
> (preferably entry-level) readings?