## Exercise 11.1

January 1st, 2008

1) Prove that (∀cs | cs is finite) putCharList cs = map putChar cs

where

```putCharList [] = [] putCharList (c:cs) = putChar c : putCharList cs   map f [] = [] map f (x:xs) = f x : map f xs```

Base case:

```putCharList [] => [] => map putChar []```

Inductive Step:

assume that purCharList cs = map putChar cs

then

```putCharList (c:cs) => putChar c : putCharList cs => putChar c : map putChar cs => map putChar (c:cs)```

QED.

2) Prove that (∀xs | xs is finite) listProd xs = fold (*) 1 xs

where

```listProd [] = 1 listProd (x:xs) = x * listProd xs   fold op init [] = init fold op init (x:xs) = x `op` fold op init xs```

Base case:

```listProd [] => 1 => fold (*) 1 []```

Inductive Step:

assume that listProd xs = fold (*) 1 xs

then

```listProd (x:xs) => x * listProd xs => x * fold (*) 1 xs => fold (*) 1 (x:xs)```

QED.

## Exercise 10.4

January 1st, 2008

A quick look at Graphics.SOE reveals that getWindowEvent is the right function to trap mouse down, up, and move events separately.

```{- maybeClear is useful for avoiding flicker when not dragging objects. A real flicker-free solution should use double-buffering of course - this code still flickers terribly while dragging. -}   maybeClear :: Bool -> Window -> IO () maybeClear b w = if b then do clearWindow w else return ()   {- The program is in two halves: either we're waiting for a click (not dragging), or we're waiting for a release (dragging). Waiting for a click is almost identical to the previous definition of loop, except for the event function. -}   waitForClick :: Window -> [(Color, Region)] -> Bool -> IO () waitForClick w regs b = do maybeClear b w sequence_ [drawRegionInWindow w c r | (c,r) <- reverse regs] event <- getWindowEvent w case event of (Button (x,y) True True) -> let aux (_,r) = r `containsR` (pixelToInch (x - xWin2), pixelToInch (yWin2 - y)) in case (break aux regs) of (_, []) -> closeWindow w (top, hit:bot) -> waitForRelease (x,y) (x,y) w (hit : (top++bot)) True _ -> waitForClick w regs False   {- While dragging, we keep track of the initial click coordinates and translate the Region at the head of the list by the offset of the current mouse coordinates. When the mouse button is released, we go back to waiting for a click, leaving the head Region where it is. -}   waitForRelease :: Point -> Point -> Window -> [(Color, Region)] -> Bool -> IO () waitForRelease (origx, origy) (x,y) w regs b = do maybeClear b w sequence_ [drawRegionInWindow w c r | (c,r) <- reverse \$ tail regs] let (c,r) = head regs newHeadReg = (Translate (pixelToInch (x - origx), pixelToInch(origy - y)) r) drawRegionInWindow w c newHeadReg event <- getWindowEvent w case event of (Button (x,y) True False) -> waitForClick w ((c,newHeadReg) : (tail regs)) True (MouseMove pt) -> waitForRelease (origx,origy) pt w regs True _ -> waitForRelease (origx,origy) (x,y) w regs False   {- All that remains is to drive the drag and drop functionality with some boilerplate draw and main functions. -}   draw3 :: String -> Picture -> IO () draw3 s p = runGraphics \$ do w <- openWindow s (xWin, yWin) waitForClick w (pictToList p) True   main = draw3 "Drag and Drop" pic```

## Exercise 10.3

December 31st, 2007

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))```

## Exercise 10.2

December 31st, 2007

Simply run the code given in the book. The Graphics.SOE package seems to be buggy with respect to updating the window properly. I had redraw bugs using both GHCI and Hugs (using Ubuntu 7.10 on x86_84).

## Exercise 10.1

December 28th, 2007

This exercise is simply to execute the code given in the book.

To draw the “five circles” example:

```draw "five circles" \$ Region Blue \$ Translate (-2,0) \$ Scale (0.5, 0.5) fiveCircles```

Note: Technical errors 17, 18 and 19 apply to the code (in particular shapeToGRegion) in Chapter 10.

## Exercise 9.12

August 9th, 2007

Instances where we can curry and convert anonymous functions to sections are easy to find, for example from Exercise 5.5:

```doubleEach'' :: [Int] -> [Int] doubleEach'' = map (*2)```

## Exercise 9.11

August 9th, 2007
```map f (map g xs) = map (f.g) xs   map (\x -> (x+1)/2) xs = map (/2) (map (+1) xs)```

## Exercise 9.10

August 9th, 2007
`map ((/2).(+1)) xs`

## Exercise 9.9

August 8th, 2007
`fix f = f (fix f)`

First, f takes the result of fix f, and second, the return type of f must be the same as the return type of fix.

`fix :: (a -> a) -> a`

Research shows that fix is the Fixed point combinator (or Y-combinator). Apparently this allows the definition of anonymous recursive functions. So let’s try to make remainder into an anonymous function. A good way to start is to simply remove one of the arguments and see if we can return an anonymous function. Something tells me that a is the argument to remove, since b is used in the base case.

```remanon b = (\f x -> if x < b then x else f (x-b))```

That’s a good start. Note here that if we try to do something like:

`(remanon 3) remanon`

Haskell says “unification would give infinite type” – which is a good sign. This is what we would like to do with the help of fix. So now if we apply fix to this, we get:

```fix (remanon b) = (remanon b) (fix (remanon b)) = (\x -> if x < b then x else (fix (remanon b)) (x-b))```

Which looks good. So we need to fix remanon and apply it to a.

`remainder' a b = fix (remanon b) a`

And that works.

## Exercise 9.8

August 8th, 2007
```power :: (a -> a) -> Int -> a -> a power f 0 = (\x -> x) power f n = (\x -> f (power f (n-1) x))```

Since the function is called power, there is one obvious application that springs to mind, i.e. raising to a power:

```raise :: Int -> Int -> Int raise x y = power (*x) y 1```