Exercise 10.3

Prove is, to my mind, a strong word. But by substitution we can show that these functions are equivalent. First, the originals:

adjust :: [(Color, Region)] -> Coordinate
          -> (Maybe (Color, Region), [(Color, Region)])
adjust regs p
    = case (break (\(_,r) -> r `containsR` p) regs) of
        (top, hit:rest) -> (Just hit, top++rest)
        (_, []) -> (Nothing, regs)

loop :: Window -> [(Color, Region)] -> IO ()
loop w regs
    = do clearWindow w
         sequence_ [drawRegionInWindow w c r | (c,r) <- reverse regs]
         (x,y) <- getLBP w
         case (adjust regs (pixelToInch (x - xWin2),
                            pixelToInch (yWin2 - y))) of
           (Nothing, _) -> closeWindow w
           (Just hit, newRegs) -> loop w (hit:newRegs)

We can easily alter adjust to:

adjust regs p
    = let aux (_,r) = r `containsR` p
      in case (break aux regs) of
           (_, []) -> (Nothing, regs)
           (top, hit:bot) -> (Just hit, top++bot)

simply pulling the anonymous function into a let, renaming rest to bot and reordering the case clauses. Let’s further substitute the bound value of p into adjust:

adjust regs
    = let aux (_,r) = r `containsR` (pixelToInch (x - wWin2),
                                     pixelToInch (yWin2 - y))
      in case (break aux regs) of
           (_, []) -> (Nothing, regs)
           (top, hit:bot) -> (Just hit, top++bot)

Now consider what loop does for each return value of adjust, and substitute.

(_, []) -> (Nothing, regs)     {- from adjust -}
(Nothing, _) -> closeWindow w  {- from loop -}

(Nothing, regs) is bound to (Nothing, _)
therefore we can substitute:
(_, []) -> closeWindow w

(top, hit:bot) -> (Just hit, top++bot)        {- from adjust -}
(Just hit, newRegs) -> loop w (hit : newRegs) {- from loop -}

(Just hit, top++bot) is bound to (Just hit, newRegs)
therefore we can substitute:
(top, hit:bot) -> loop w (hit : (top++bot))

Our new adjust variant is now:

adjust regs
    = let aux (_,r) = r `containsR` (pixelToInch (x - wWin2),
                                     pixelToInch (yWin2 - y))
      in case (break aux regs) of
           (_, []) -> closeWindow w
           (top, hit:bot) -> loop w (hit : (top++bot))

Obviously at this point there are various unbound variables in this variant of adjust, so it cannot stand alone. But it can now itself be substituted into the body of loop:

loop w regs
    = do clearWindow w
         sequence_ [drawRegionInWindow w c r | (c,r) <- reverse regs]
         (x,y) <- getLBP w
         let aux (_,r) = r `containsR` (pixelToInch (x - xWin2),
                                        pixelToInch (yWin2 - y))
         case (break aux regs) of
           (_, []) -> closeWindow w
           (top, hit:bot) -> loop w (hit : (top++bot))

We lose the in because we are inside the do form. The only thing that remains is to show that
sequence_ [drawRegionInWindow w c r | (c,r) <- reverse regs]
is equivalent to
sequence_ (map (uncurry (drawRegionInWindow w)) (reverse regs))

The prelude defines uncurry:

uncurry :: (a -> b -> c) -> ((a,b) -> c)
uncurry f p = f (fst p) (snd p)

(drawRegionInWindow w) is a function of type Color -> Region -> IO ().
(uncurry (drawRegionInWindow w)) is a function of type (Color, Region) -> IO ().
(reverse regs) is of type [(Color, Region)].

So by inspection we can see that the two forms are equivalent. map and uncurry do explicitly what the list comprehension does implicitly. Equivalency of the final form of loop follows.

loop w regs
    = do clearWindow w
         sequence_ (map (uncurry (drawRegionInWindow w)) (reverse regs))
         (x,y) <- getLBP w
         let aux (_,r) = r `containsR` (pixelToInch (x - xWin2),
                                        pixelToInch (yWin2 - y))
         case (break aux regs) of
           (_, []) -> closeWindow w
           (top, hit:bot) -> loop w (hit : (top++bot))

Leave a Reply