fmap fix return

July 7, 2013 - Tagged as: en, haskell.

While floating across the internets, I came across a blog with title fmap fix return. I immediately run ghci and queried it’s type:

ghci> :t fmap fix return
fmap fix return :: a -> a

We know that only value with type forall a. a -> a (other than bottom) is identity function(id in Haskell). I found it very interesting, fmap fix return gives us identity function!

I got a pen and paper and started evaluating expressions to understand how does that give us the identity function.

First, let’s note our actors:

fmap :: Functor f => (a -> b) -> f a -> f b
-- instance specific implementation

fix  :: (a -> a) -> a
fix f = let x = f x in x

return :: Monad m => a -> m a
-- instance specific implementation

A very important thing to realize at this point is which monad and functor instances are used for return and fmap. To realize this, observe that we get a function as return value of fmap. Which means Functor f => f b is a -> a, or written in a different style to see it’s functor property: ((->) a) a, so our functor here is (->) a.

After that, we need to look up functor and monad instances for (->) a. Since it’s 2:30 AM here, I wanted to derive that too.

instance Functor ((->) a) where
     fmap = (.)

It’s very easy to derive just by looking specialized version of fmaps type for ((->) a): fmap :: (a1 -> b) -> (a -> a1) -> (a -> b).

We can easily prove that it satisfies functor laws:

fmap id f
= id . f
= f

fmap (p . q) <-> (fmap p) . (fmap q)
(fmap p) . (fmap q) f
= fmap p . (q . f)
= p . q . f
= fmap (p . q) f

Monad instance can also be derived from types of return and >>=:

instance Monad ((->) a) where
    return   = const
    f >>= fn = \r -> fn (f r) r

(I found Monad instance of ((->) a) very interesting, especially the >>= part. I couldn’t come up with a problem that makes use of this instance, I’ll investigate that after some sleep)

It satisfies monad laws:

-- left identity
return a >>= f
= const a >>= f
= \r -> f ((const a) r) r
= \r -> f a r
= f a

-- right identity
m >>= return
= \r -> return (m r) r
= \r -> (const (m r) r)
= \r -> m r
= m

-- associativity
(m >>= f) >>= g <-> m >>= (\x -> f x >>= g)

let's first write `p` for `m >>= f`

= p >>= g
= \r1 -> g (p r1) r1

let's also evaluaute p

p = m >>= f
= \r2 -> f (m r2) r2

substitute new p

= \r1 -> g ((\r2 -> f (m r2) r2) r1) r1
= \r1 -> g (f (m r1) r1) r1
= \r -> g (f (m r) r) r

now let's also evaluate right hand side of equation

m >>= (\x -> f x >>= g)
= m >>= (\x -> (    f x >>= g    )) -- just added a paren for clarity
= m >>= (\x -> (\r -> g (f x r) r))

let write `p` for `\x -> (\r -> g (f x r) r)`

= m >>= p
= \r1 -> p (m r1) r1

put p back

= \r1 -> (\x -> (\r -> g (f x r) r)) (m r1) r1
= \r1 -> (\r -> g (f (m r1) r)) r1
= \r1 -> g (f (m r1) r1)

For those who have no idea what’s above, I’m basically proving some equalities by substituting expressions with their equivalents. This is a benefit for working on a purely functional language, which means referential transparency.

OK, now with these return and fmap implementations in mind, let’s evaluate fmap fix return:

fmap fix return
= fix . return
= \r -> fix (return r)
= \r -> fix (const r)
= \r -> (\f = let x = f x in x) (const r)
= \r -> let x = (const r) x in x

since `const a _ = a`, we have x = r here

= \r -> r

.. which is the identity function.

Thus fmap fix return demystified.