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? _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe