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. But that made me wonder what it's doing in the definition of fix. 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)))
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?