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?