{"id":57,"date":"2007-12-31T17:53:17","date_gmt":"2008-01-01T00:53:17","guid":{"rendered":"http:\/\/www.elbeno.com\/haskell_soe_blog\/?p=57"},"modified":"2008-01-08T10:07:48","modified_gmt":"2008-01-08T18:07:48","slug":"exercise-103","status":"publish","type":"post","link":"https:\/\/www.elbeno.com\/haskell_soe_blog\/?p=57","title":{"rendered":"Exercise 10.3"},"content":{"rendered":"<p>Prove is, to my mind, a strong word. But by substitution we can show that these functions are equivalent. First, the originals:<\/p>\n<pre lang=\"haskell\">adjust :: [(Color, Region)] -> Coordinate\r\n          -> (Maybe (Color, Region), [(Color, Region)])\r\nadjust regs p\r\n    = case (break (\\(_,r) -> r `containsR` p) regs) of\r\n        (top, hit:rest) -> (Just hit, top++rest)\r\n        (_, []) -> (Nothing, regs)\r\n\r\nloop :: Window -> [(Color, Region)] -> IO ()\r\nloop w regs\r\n    = do clearWindow w\r\n         sequence_ [drawRegionInWindow w c r | (c,r) <- reverse regs]\r\n         (x,y) <- getLBP w\r\n         case (adjust regs (pixelToInch (x - xWin2),\r\n                            pixelToInch (yWin2 - y))) of\r\n           (Nothing, _) -> closeWindow w\r\n           (Just hit, newRegs) -> loop w (hit:newRegs)<\/pre>\n<p>We can easily alter <tt>adjust<\/tt> to:<\/p>\n<pre lang=\"haskell\">adjust regs p\r\n    = let aux (_,r) = r `containsR` p\r\n      in case (break aux regs) of\r\n           (_, []) -> (Nothing, regs)\r\n           (top, hit:bot) -> (Just hit, top++bot)<\/pre>\n<p>simply pulling the anonymous function into a <tt>let<\/tt>, renaming <tt>rest<\/tt> to <tt>bot<\/tt> and reordering the <tt>case<\/tt> clauses. Let&#8217;s further substitute the bound value of <tt>p<\/tt> into <tt>adjust<\/tt>:<\/p>\n<pre lang=\"haskell\">adjust regs\r\n    = let aux (_,r) = r `containsR` (pixelToInch (x - wWin2),\r\n                                     pixelToInch (yWin2 - y))\r\n      in case (break aux regs) of\r\n           (_, []) -> (Nothing, regs)\r\n           (top, hit:bot) -> (Just hit, top++bot)<\/pre>\n<p>Now consider what <tt>loop<\/tt> does for each return value of <tt>adjust<\/tt>, and substitute.<\/p>\n<pre lang=\"haskell\">(_, []) -> (Nothing, regs)     {- from adjust -}\r\n(Nothing, _) -> closeWindow w  {- from loop -}<\/pre>\n<p><tt>(Nothing, regs)<\/tt> is bound to <tt>(Nothing, _)<\/tt><br \/>\ntherefore we can substitute:<br \/>\n<tt>(_, []) -> closeWindow w<\/tt><\/p>\n<pre lang=\"haskell\">(top, hit:bot) -> (Just hit, top++bot)        {- from adjust -}\r\n(Just hit, newRegs) -> loop w (hit : newRegs) {- from loop -}<\/pre>\n<p><tt>(Just hit, top++bot)<\/tt> is bound to <tt>(Just hit, newRegs)<\/tt><br \/>\ntherefore we can substitute:<br \/>\n<tt>(top, hit:bot) -> loop w (hit : (top++bot))<\/tt><\/p>\n<p>Our new <tt>adjust<\/tt> variant is now:<\/p>\n<pre lang=\"haskell\">adjust regs\r\n    = let aux (_,r) = r `containsR` (pixelToInch (x - wWin2),\r\n                                     pixelToInch (yWin2 - y))\r\n      in case (break aux regs) of\r\n           (_, []) -> closeWindow w\r\n           (top, hit:bot) -> loop w (hit : (top++bot))<\/pre>\n<p>Obviously at this point there are various unbound variables in this variant of <tt>adjust<\/tt>, so it cannot stand alone. But it can now itself be substituted into the body of <tt>loop<\/tt>:<\/p>\n<pre lang=\"haskell\">loop w regs\r\n    = do clearWindow w\r\n         sequence_ [drawRegionInWindow w c r | (c,r) <- reverse regs]\r\n         (x,y) <- getLBP w\r\n         let aux (_,r) = r `containsR` (pixelToInch (x - xWin2),\r\n                                        pixelToInch (yWin2 - y))\r\n         case (break aux regs) of\r\n           (_, []) -> closeWindow w\r\n           (top, hit:bot) -> loop w (hit : (top++bot))<\/pre>\n<p>We lose the <tt>in<\/tt> because we are inside the <tt>do<\/tt> form. The only thing that remains is to show that<br \/>\n<tt>sequence_ [drawRegionInWindow w c r | (c,r) <- reverse regs]<\/tt><br \/>\nis equivalent to<br \/>\n<tt>sequence_ (map (uncurry (drawRegionInWindow w)) (reverse regs))<\/tt><\/p>\n<p>The prelude defines <tt>uncurry<\/tt>:<\/p>\n<pre lang=\"haskell\">uncurry :: (a -> b -> c) -> ((a,b) -> c)\r\nuncurry f p = f (fst p) (snd p)<\/pre>\n<p><tt>(drawRegionInWindow w)<\/tt> is a function of type <tt>Color -> Region -> IO ()<\/tt>.<br \/>\n<tt>(uncurry (drawRegionInWindow w))<\/tt> is a function of type <tt>(Color, Region) -> IO ()<\/tt>.<br \/>\n<tt>(reverse regs)<\/tt> is of type <tt>[(Color, Region)]<\/tt>.<\/p>\n<p>So by inspection we can see that the two forms are equivalent. <tt>map<\/tt> and <tt>uncurry<\/tt> do explicitly what the list comprehension does implicitly. Equivalency of the final form of <tt>loop<\/tt> follows.<\/p>\n<pre lang=\"haskell\">loop w regs\r\n    = do clearWindow w\r\n         sequence_ (map (uncurry (drawRegionInWindow w)) (reverse regs))\r\n         (x,y) <- getLBP w\r\n         let aux (_,r) = r `containsR` (pixelToInch (x - xWin2),\r\n                                        pixelToInch (yWin2 - y))\r\n         case (break aux regs) of\r\n           (_, []) -> closeWindow w\r\n           (top, hit:bot) -> loop w (hit : (top++bot))<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>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) (_, []) [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":[],"categories":[1],"tags":[],"_links":{"self":[{"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=\/wp\/v2\/posts\/57"}],"collection":[{"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=57"}],"version-history":[{"count":0,"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=\/wp\/v2\/posts\/57\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=57"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=57"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=57"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}