[Haskell-cafe] Fixed-point operator (was: seq does not preclude
parametricity)
Matthew Brecknell
haskell at brecknell.org
Sun Jan 28 23:19:36 EST 2007
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?
More information about the Haskell-Cafe
mailing list