Programming in Haskell の練習問題の実装例 Part 2

Programming in Haskell という書籍で Haskell の勉強をしています（日本語版はこちら）．
この本の Part II の部分の練習問題を実装してみました
答え合わせもかねているので，間違っている点や改善点があったら教えていただけるとうれしいです．

（Part I はこちら Programming in Haskell の練習問題の実装例 Part. 1 ）

8. Declaring types and classes

Exercise 1

putStr :: String -> IO ()
putStr xs = sequence_ [putChar x | x <- xs]

Exercise 2

type Board = [Int]

putRow' :: Board -> Int -> IO ()
putRow' [] _ = return ()
putRow' (b : bs) row = do
  putStr (show row)
  putStr ": "
  putStrLn (concat (replicate b "* "))
  putRow' bs (row + 1)

putBoard :: Board -> IO ()
putBoard b = putRow' b 1

Exercise 3

type Board = [Int]

putRow :: Int -> Int -> IO ()
putRow row num = do
  putStr (show row)
  putStr ": "
  putStrLn (concat (replicate num "* "))

putBoard :: Board -> IO ()
putBoard b = sequence_ [putRow r n | (r, n) <- zip [1 ..] b

Exercise 4

import System.IO

getIntegers :: Int -> Int -> IO Int
getIntegers t n = do
  if n == 0
    then return t
    else do
      xs <- getLine
      getIntegers (t + (read xs :: Int)) (n - 1)

adder :: IO ()
adder = do
  putStr "How many numbers? "
  n <- getLine
  t <- getIntegers 0 (read n :: Int)
  putStrLn ("The total is " ++ show t)

Exercise 5

import System.IO

adder' :: IO ()
adder' = do
  putStr "How many numbers? "
  n <- getLine
  res <- sequence (replicate (read n :: Int) getLine)
  putStrLn ("The total is " ++ show (sum (map (read :: String -> Int) res)))

Exercise 6

こんな感じに書いてはみたものの，delete と backspace を押しても \DEL と \b を拾ってもらえずちゃんと動作しませんでした．

import System.IO

getCh :: IO Char
getCh = do
  hSetEcho stdin False
  x <- getChar
  hSetEcho stdin True
  return x

clearLine :: IO ()
clearLine = putStr "\ESC[2K"

clearEnd :: IO ()
clearEnd = putStr "\ESC[0K"

backCursor :: IO ()
backCursor = putStr "\ESC[1D"

getChars :: Int -> String -> IO String
getChars n xs = do
  x <- getChar
  if x == '\n'
    then do
      putChar x
      return (xs ++ [x])
    else
      if x == '\b'
        then do
          backCursor
          getChars (max 0 (n - 1)) xs
        else
          if x == '\DEL'
            then do
              clearEnd
              putStr (drop n xs)
              getChars n (take (n - 1) xs ++ drop n xs)
            else do
              putChar x
              getChars (n + 1) (xs ++ [x])

readLine :: IO String
readLine = getChars 0 ""

main = do
  xs <- readLine
  print xs

11 Unbeatable tic-tac-toe

Exercise 1

...

cntNodes :: Tree a -> Int
cntNodes (Node x []) = 1
cntNodes (Node x ts) = 1 + sum [cntNodes t | t <- ts]

cntDepth :: Tree a -> Int
cntDepth (Node x []) = 0
cntDepth (Node x ts) = 1 + maximum [cntDepth t | t <- ts]

main :: IO ()
main = do
  let t = gametree empty O
  print (cntNodes t) -- 549946
  print (cntDepth t) -- 9

Exercise 2

import Data.Char
import Data.List
import System.IO
import System.Random

...

bestmove :: Grid -> Player -> IO Grid
bestmove g p = do
  putStr "number: "
  x <- (randomRIO :: (Int, Int) -> IO Int) (0, length xs - 1)
  return (xs !! x)
  where
    tree = prune depth (gametree g p)
    Node (_, best) ts = minimax tree
    xs = [g' | Node (g', p') _ <- ts, p' == best]

play' :: Grid -> Player -> IO ()
play' g p
  | wins O g = putStrLn "Player O wins!\n"
  | wins X g = putStrLn "Player X wins!\n"
  | full g = putStrLn "It's a draw!\n"
  | p == O = do
    i <- getNat (prompt p)
    case move g i p of
      [] -> do
        putStrLn "ERROR: Invalid move"
        play' g p
      [g'] -> play g' (nxt p)
  | p == X = do
    putStr "Player X is thinking... "
    g' <- bestmove g p
    play g' (nxt p)

Exercise 3

...

cntDepth :: Tree (Grid, Player) -> Int
cntDepth (Node (_, _) []) = 0
cntDepth (Node (g, p) ts) = 1 + maximum [cntDepth t | t <- ts]

minTree :: Tree (Grid, Player) -> [Tree (Grid, Player)] -> Tree (Grid, Player)
minTree t [] = t
minTree t (x : xs)
  | n < n' = minTree t xs
  | otherwise = minTree x xs
  where
    n = cntDepth t
    n' = cntDepth x

bestmove :: Grid -> Player -> Grid
bestmove g p = g''
  where
    tree = prune depth (gametree g p)
    Node (_, best) ts = minimax tree
    xs = [Node (g', p') t | Node (g', p') t <- ts, p' == best]
    Node (g'', _) ts'' = minTree (head xs) xs

Exercise 4

import Data.Char
import Data.List
import System.IO

data Player = O | B | X
  deriving (Eq, Ord, Show)

type Grid = [[Player]]

next :: Player -> Player
next O = X
next B = B
next X = O

empty :: Int -> Grid
empty size = replicate size (replicate size B)

full :: Grid -> Bool
full = all (/= B) . concat

turn :: Grid -> Player
turn g = if os <= xs then O else X
  where
    os = length (filter (== O) ps)
    xs = length (filter (== X) ps)
    ps = concat g

diag :: Int -> Grid -> [Player]
diag size g = [g !! n !! n | n <- [0 .. size - 1]]

wins :: Int -> Player -> Grid -> Bool
wins size p g = any line (rows ++ cols ++ dias)
  where
    line = all (== p)
    rows = g
    cols = transpose g
    dias = [diag size g, diag size (map reverse g)]

won :: Int -> Grid -> Bool
won size g = wins size O g || wins size X g

showPlayer :: Player -> [String]
showPlayer O = ["   ", " O ", "   "]
showPlayer B = ["   ", "   ", "   "]
showPlayer X = ["   ", " X ", "   "]

interleave :: a -> [a] -> [a]
interleave x [] = []
interleave x [y] = [y]
interleave x (y : ys) = y : x : interleave x ys

showRow :: [Player] -> [String]
showRow = beside . interleave bar . map showPlayer
  where
    beside = foldr1 (zipWith (++))
    bar = replicate 3 "|"

putGrid :: Int -> Grid -> IO ()
putGrid size = putStrLn . unlines . concat . interleave bar . map showRow
  where
    bar = [replicate ((size * 4) - 1) '-']

valid :: Int -> Grid -> Int -> Bool
valid size g i = 0 <= i && i < size ^ 2 && concat g !! i == B

chop :: Int -> [a] -> [[a]]
chop n [] = []
chop n xs = take n xs : chop n (drop n xs)

move :: Int -> Grid -> Int -> Player -> [Grid]
move size g i p = [chop size (xs ++ [p] ++ ys) | valid size g i]
  where
    (xs, B : ys) = splitAt i (concat g)

nxtTree :: Grid -> Tree Grid -> Tree Grid
nxtTree g (Node g' ts') = head [Node g'' ts'' | Node g'' ts'' <- ts', g'' == g]

cls :: IO ()
cls = putStr "\ESC[2J"

type Pos = (Int, Int)

goto :: Pos -> IO ()
goto (x, y) = putStr ("\ESC[" ++ show y ++ ";" ++ "H")

prompt :: Player -> String
prompt p = "Player" ++ show p ++ ", enter your move: "

getNat :: String -> IO Int
getNat prompt = do
  putStr prompt
  xs <- getLine
  if xs /= [] && all isDigit xs
    then return (read xs)
    else do
      putStrLn "ERROR: Invalid number"
      getNat prompt

run' :: Int -> Grid -> Player -> IO ()
run' size g p
  | wins size O g = putStrLn "Player O wins!\n"
  | wins size X g = putStrLn "Player X wins!\n"
  | full g = putStrLn "It's a draw!\n"
  | otherwise = do
    i <- getNat (prompt p)
    case move size g i p of
      [] -> do
        putStrLn "ERROR: Invalid move"
        run' size g p
      [g'] -> run size g' (next p)

run :: Int -> Grid -> Player -> IO ()
run size g p = do
  cls
  goto (1, 1)
  putGrid size g
  run' size g p

tictactoe :: IO ()
tictactoe = do
  size <- getSize
  run size (empty size) O

data Tree a = Node a [Tree a]
  deriving (Show)

moves :: Int -> Grid -> Player -> [Grid]
moves size g p
  | won size g = []
  | full g = []
  | otherwise = concat [move size g i p | i <- [0 .. ((size ^ 2) - 1)]]

gametree :: Int -> Grid -> Player -> Tree Grid
gametree size g p = Node g [gametree size g' (next p) | g' <- moves size g p]

prune :: Int -> Tree a -> Tree a
prune 0 (Node x _) = Node x []
prune n (Node x ts) = Node x [prune (n - 1) t | t <- ts]

depth :: Int
depth = 9

minimax :: Int -> Tree Grid -> Tree (Grid, Player)
minimax size (Node g [])
  | wins size O g = Node (g, O) []
  | wins size X g = Node (g, X) []
  | otherwise = Node (g, B) []
minimax size (Node g ts)
  | turn g == O = Node (g, minimum ps) ts'
  | turn g == X = Node (g, maximum ps) ts'
  where
    ts' = map (minimax size) ts
    ps = [p | Node (_, p) _ <- ts']

min' :: Int
min' = -2

max' :: Int
max' = 2

bestTree :: Player -> (Int, Grid) -> (Int, Grid) -> (Int, Grid)
bestTree p res now
  | p == O =
    if fst res < fst now
      then res
      else now
  | otherwise =
    if fst res > fst now
      then res
      else now

alphaBetaPrune' :: Int -> Player -> Int -> Int -> (Int, Grid) -> [Tree Grid] -> (Int, Grid)
alphaBetaPrune' _ _ _ _ best [] = best
alphaBetaPrune' size p a b best ts
  | a >= b = best
  | p == O = alphaBetaPrune' size p a b' best' (tail ts)
  | otherwise = alphaBetaPrune' size p a' b best' (tail ts)
  where
    Node g' ts' = head ts
    res = alphaBetaPrune size a b (Node g' ts')
    best' = bestTree p (fst res, g') best
    a' = max a (fst best')
    b' = min b (fst best')

alphaBetaPrune :: Int -> Int -> Int -> Tree Grid -> (Int, Grid)
alphaBetaPrune size a b (Node g [])
  | wins size O g = (-1, g)
  | wins size X g = (1, g)
  | otherwise = (0, g)
alphaBetaPrune size a b (Node g ts)
  | turn g == O = alphaBetaPrune' size O a b (max', g) ts
  | turn g == X = alphaBetaPrune' size X a b (min', g) ts

bestmove :: Int -> Tree Grid -> Player -> Grid
bestmove size (Node g ts) p = snd (alphaBetaPrune size min' max' (Node g ts))

play' :: Int -> Tree Grid -> Player -> IO ()
play' size (Node g ts) p
  | wins size O g = putStrLn "Player O wins!\n"
  | wins size X g = putStrLn "Player X wins!\n"
  | full g = putStrLn "It's a draw!\n"
  | p == O = do
    i <- getNat (prompt p)
    case move size g i p of
      [] -> do
        putStrLn "ERROR: Invalid move"
        play' size (Node g ts) p
      [g'] -> play size (nxtTree g' (Node g ts)) (next p)
  | p == X = do
    putStr "Player X is thinking... "
    (play size $! nxtTree (bestmove size (Node g ts) p) (Node g ts)) (next p)

play :: Int -> Tree Grid -> Player -> IO ()
play size (Node g ts) p = do
  cls
  goto (1, 1)
  putGrid size g
  play' size (Node g ts) p

fstPlayer :: IO Player
fstPlayer = do
  putStr "First Player: "
  x <- getLine
  if x == "O"
    then return O
    else
      if x == "X"
        then return X
        else do
          print "ERROR: Invalid player"
          fstPlayer

getSize :: IO Int
getSize = do
  putStr "Length of winning line: "
  xs <- getLine
  if all isDigit xs
    then return (read xs)
    else do
      print "ERROR: Invalid length"
      getSize

main :: IO ()
main = do
  hSetBuffering stdout NoBuffering
  p <- fstPlayer
  size <- getSize
  play size (gametree size (empty size) p) p

12 Monads and more

Exercise 1

data Tree a = Leaf | Node (Tree a) a (Tree a)
  deriving (Show)

instance Functor Tree where
  -- fmap :: (a -> b) -> Tree a -> Tree b
  fmap g Leaf = Leaf
  fmap g (Node l x r) = Node (fmap g l) (g x) (fmap g r)

Exercise 2

instance Functor ((->) a) where
  -- fmap :: (a -> b) -> (r -> a) -> (r -> b)
  fmap g h = g . h

Exercise 3

instance Applicative ((->) a) where
  -- pure :: a -> (r -> a)
  pure x = \_ -> x

  -- (<*>) :: (r -> (a -> b)) -> (r -> a) -> (r -> b)
  g <*> h = \x -> g x (h x)

Exercise 4

newtype ZipList a = Z [a] deriving (Show)

instance Functor ZipList where
  -- fmap :: (a -> b) -> ZipList a -> ZipList b
  fmap g (Z xs) = Z (map g xs)

instance Applicative ZipList where
  -- pure :: a -> ZipList a
  pure xs = Z xs

  -- (<*>) :: ZipList (a -> b) -> ZipList a -> ZipList b
  (Z gs) <*> (Z xs) = Z [g x | (g, x) <- zip (gs xs)]

Exercise 6

instance Monad ((->) a) where
  -- return :: a -> (r -> a)
  return = pure

  -- (>>=) :: (r -> a) -> (a -> (r -> b)) -> (r -> b)
  g >>= h = \x -> h (g x) x

Exercise 7

data Expr a = Var a | Val Int | Add (Expr a) (Expr a)
  deriving (Show)

instance Functor Expr where
  -- fmap :: (a -> b) -> Expr a -> Expr b
  fmap g (Var a) = Var (g a)
  fmap _ (Val x) = Val x
  fmap g (Add x y) = Add (fmap g x) (fmap g y)

instance Applicative Expr where
  -- pure :: a -> Expr a
  pure = Var

  -- (<*>) :: Expr (a -> b) -> Expr a -> Expr b
  _ <*> Val x = Val x
  (Val x) <*> _ = Val x
  (Var g) <*> ex = fmap g ex
  (Add eg eh) <*> ex = Add (eg <*> ex) (eh <*> ex)

instance Monad Expr where
  -- return :: a -> Expr a
  return = pure

  -- (>>=) :: Expr a -> (a -> Expr b) -> Expr b
  (Val x) >>= f = Val x
  (Var x) >>= f = f x
  (Add ex ey) >>= f = Add (ex >>= f) (ey >>= f)

ec :: Expr Char
ec = Add (Add (Var 'a') (Var 'b')) (Val 3)

vars :: Char -> Expr Int
vars 'a' = Val 1
vars 'b' = Val 2

subst :: Expr a -> (a -> Expr b) -> Expr b
subst ex vs = ex >>= vs

eval :: Expr a -> Int
eval (Val x) = x
eval (Add x y) = eval x + eval y

main = do
  print (eval (subst ec vars)) -- 

Exercise 8

type State = Int

newtype ST a = S (State -> (a, State))

app :: ST a -> State -> (a, State)
app (S st) = st

instance Functor ST where
  -- fmap :: (a -> b) -> ST a -> ST b
  fmap g st = g <$> st

instance Applicative ST where
  -- pure :: a -> ST a
  pure x = S (\s -> (x, s))

  -- (<*>) :: ST (a -> b) -> ST a -> ST b
  stf <*> stx = do
    g <- stf
    s <- stx
    return (g s)

instance Monad ST where
  -- (>>=) :: ST a -> (a -> ST b) -> ST b
  st >>= f = S (\s -> let (x, s') = app st s in app (f x) s')

13. Monadic parsing

Exercise 1

comment :: Parser ()
comment = do
  symbol "--"
  many (sat (/= '\n'))
  char '\n'
  return ()

Exercise 5

data Expr = Val Int | Add Expr Expr | Mul Expr Expr

blak (Val n) = "(Val " ++ show n ++ ")"
blak e = "(" ++ show e ++ ")"

instance Show Expr where
  show (Val n) = "Val " ++ show n
  show (Add l r) = "Add " ++ blak l ++ blak r
  show (Mul l r) = "Mul " ++ blak l ++ blak r

expr' :: Parser Expr
expr' = do
  t <- term'
  do
    symbol "+"
    e <- expr'
    return (Add t e)
    <|> return t

term' :: Parser Expr
term' = do
  f <- factor'
  do
    symbol "*"
    t <- term'
    return (Mul f t)
    <|> return f

factor' :: Parser Expr
factor' =
  do
    symbol "("
    e <- expr'
    symbol ")"
    return e
    <|> do
      n <- natural
      return (Val n)

Exercise 6

expr :: Parser Int
expr = do
  t <- term
  do
    symbol "+"
    e <- expr
    return (t + e)
    <|> do
      symbol "-"
      e <- expr
      return (t - e)
    <|> return t

term :: Parser Int
term = do
  f <- factor
  do
    symbol "*"
    t <- term
    return (f * t)
    <|> do
      symbol "/"
      t <- term
      if t == 0
        then empty
        else return (f `div` t)
    <|> return f

factor :: Parser Int
factor =
  do
    symbol "("
    e <- expr
    symbol ")"
    return e
    <|> integer

Exercise 7

expr :: Parser Int
expr = do
  t <- term
  do
    symbol "+"
    e <- expr
    return (t + e)
    <|> do
      symbol "-"
      e <- expr
      return (t - e)
    <|> return t

term :: Parser Int
term = do
  p <- pow
  do
    symbol "*"
    t <- term
    return (p * t)
    <|> do
      symbol "/"
      t <- term
      if t == 0
        then empty
        else return (p `div` t)
    <|> return p

pow :: Parser Int
pow = do
  f <- factor
  do
    symbol "^"
    p <- pow
    return (f ^ p)
    <|> return f

factor :: Parser Int
factor =
  do
    symbol "("
    e <- expr
    symbol ")"
    return e
    <|> integer

Exercise 8

expr :: Parser Int
expr = do
  n <- natural
  ns <-
    many
      ( do
          symbol "-"
          natural
      )
  return (foldl (-) n ns)

Exercise 9

これでいいのか...？

eval' :: String -> IO ()
eval' xs = case parse expr xs of
  [(n, [])] -> calc (show n)
  [(_, out)] -> calc (show "Invalid: " ++ out)
  _ -> do
    beep
    calc xs

14. Foldables and friends

Exercise 1

instance (Monoid a, Monoid b) => Monoid (a, b) where
  -- mempty :: (a, b)
  mempty = (mempty, mempty)

  -- mappend :: (a, b) -> (a, b) -> (a, b)
  (x1, y1) `mappend` (x2, y2) = (x1 `mappend` x2, y1 `mappend` y2)

Exercise 2

instance Monoid b => Monoid (a -> b) where
  -- mempty :: a -> b
  mempty = \_ -> mempty

  -- mappend :: (a -> b) -> (a -> b) -> (a -> b)
  f `mappend` g = \x -> f x `mappend` g x

Exercise 3

import Data.Foldable

instance Foldable Maybe where
  -- fold :: Monoid a => Maybe a -> a
  fold Nothing = mempty
  fold (Just x) = x

  -- foldMap :: Monoid b => (a -> b) -> Maybe a -> b
  foldMap _ Nothing = mempty
  foldMap f (Just x) = f x

  -- foldr :: (a -> b -> b) -> b -> Maybe a -> b
  foldr _ v Nothing = v
  foldr f v (Just x) = f x v

  -- foldl :: (a -> b -> a) -> a -> Myabe b -> a
  foldl _ v Nothing = v
  foldl f v (Just x) = f v x

instance Traversable Maybe where
  -- traverse :: Applicative f => (a -> f b) -> Maybe a -> f (Maybe b)
  traverse _ Nothing = pure Nothing
  traverse g (Just x) = fmap g x

Exercise 4

import Data.Foldable

data Tree a = Leaf | Node (Tree a) a (Tree a)
  deriving (Show)

instance Foldable Tree where
  -- fold :: Monoid a => Tree a -> a
  fold Leaf = mempty
  fold (Node l x r) = fold l `mappend` fold r `mappend` x

  -- foldMap :: Monoid b => (a -> b) -> Tree a -> b
  foldMap _ Leaf = mempty
  foldMap f (Node l x r) = foldMap f l `mappend` foldMap f r `mappend` f x

  -- foldr :: (a -> b -> b) -> b -> Tree a -> b
  foldr f v Leaf = v
  foldr f v (Node l x r) = f x (foldr f (foldr f v r) l)

  -- foldl :: (a -> b -> a) -> a -> Tree b -> a
  foldl f v Leaf = v
  foldl f v (Node l x r) = f (foldl f (foldl f v l) r) x

instance Traversable Tree where
  -- traverse :: Applicative f => (a -> f b) -> Tree a -> f (Tree a)
  traverse _ Leaf = pure Leaf
  traverse g (Node l x r) = pure Node <*> traverse g l <*> g x <*> traverse g r

Exercise 5

filterF :: Foldable t => (a -> Bool) -> t a -> [a]
filterF g = foldMap (\x -> [x | g x])

15. Lazy evaluation

Exercise 4

fibs :: [Integer]
fibs = 0 : 1 : [x + y | (x, y) <- zip fibs (tail fibs)]

Exercise 5

data Tree a = Leaf | Node (Tree a) a (Tree a)
  deriving (Show)

repeat' :: a -> Tree a
repeat' x = Node t x t
  where
    t = Node t x t

take' :: Int -> Tree a -> Tree a
take' 0 _ = Leaf
take' _ Leaf = Leaf
take' n (Node l x r) = Node (take' (n - 1) l) x (take' (n - 1) r)

replicate' :: Int -> a -> Tree a
replicate' n = take' n . repeat'

main = do
  print (replicate' 3 'a')

-- Node (
--   Node (
--     Node Leaf 'a' Leaf)
--     'a' (
--     Node Leaf 'a' Leaf)
--   )
--   'a' (
--   Node (
--     Node Leaf 'a' Leaf)
--     'a' (
--     Node Leaf 'a' Leaf)
--   )

Exercise 6

sqroot :: Double -> Double
sqroot n = head [y| (x, y) <- zip xs ys, abs (x - y) <= dist]
  where
    a0 = 1.0
    dist = 0.00001
    next = \x -> (x + n / x) / 2
    xs = iterate next a0
    ys = iterate next (head (tail xs))

16. Reasoning about programs

Exercise 1

data Nat = Zero | Succ Nat

add :: Nat -> Nat -> Nat
add Zero m = m
add (Succ n) m = Succ (add n m)

Induction hypothesis: add n (Succ m) = Succ (add n m)

Base case:
add Zero (Succ m)
= { applying add }
Succ m
= { unapplying add }
Succ (add Zero m)

Inductive case:
add (Succ n) (Succ m)
= { applying add }
Succ (add n (Succ m))
= { induction hypothesis }
Succ (Succ (add n m))
= { unapplying add }
Succ (add (Succ n) m)

Exercise 2

Induction hypothesis: add n m = add m n

Base case:
add Zero m
= { applying add }
m
= { using add n Zero = n }
add m Zero

Inductive case:
add (Succ n) m
= { applying add }
Succ (add n m)
= { induction hypothesis }
Succ (add m n)
= { unapplying add }
add m (Succ n)

Exercise 3

replicate :: Int -> a -> [a]
replicate 0 _ = []
replicate n x = x : replicate (n - 1) x

all p [] = True
all p (x : xs) = p x && all p xs

Induction hypothesis: all (== x) (replicate n xs) = True

Base case:
all (== x) (replicate 0 xs)
= { applying replicate }
all (== x) []
= { applying all }
= True

Inductive case:
all (== x) (replicate (n + 1) xs)
= { applying replicate }
all (== x) (x : replicate n xs)
= { applying all }
(x == x) && (all (== x) (replicate n xs))
= { induction hypothesis }
True

Exercise 4

[] ++ ys = ys
(x : xs) ++ ys = x : (xs ++ ys)

上の等式を用いて次の等式を証明する．

xs ++ [] = xs
xs ++ (ys ++ zs) = (xs ++ ys) ++ zs

Induction hypothesis: xs ++ [] = xs

Base case:
[] ++ []
= { using [] ++ ys = ys }
[]

Inductive case
(x : xs) ++ []
= { using (x : xs) ++ ys = x : (xs ++ ys) }
x : (xs ++ [])
= { induction hypothesis }
x : xs

Induction hypothesis: xs ++ (ys ++ zs) = (xs ++ ys) ++ zs

Base case:
[] ++ (ys ++ zs)
= { using [] ++ ys = ys }
ys ++ zs
= { using [] ++ ys = ys }
([] ++ ys) ++ zs

Inductive case:
(x : xs) ++ (ys ++ zs)
= { using (x : xs) ++ ys = x : (xs ++ ys) }
x : (xs ++ (ys ++ zs))
= { induction hypothesis }
x : ((xs ++ ys) ++ zs)
= { using (x : xs) ++ ys = x : (xs ++ ys) }
x : (xs ++ ys) ++ zs
= { using (x : xs) ++ ys = x : (xs ++ ys) }
(x : xs ++ ys) ++ zs

Exercise 5

Induction hypothesis: take n xs ++ drop n xs = xs

Base case on integer n:
take 0 xs ++ drop 0 xs
= { applying take and drop }
[] ++ xs
= { using [] ++ ys = ys }
xs

Base case on list xs:
take _ [] ++ drop _ []
= { applying take and drop }
[] ++ []
= { applying [] ++ ys }
[]

Inductive case:
take (n + 1) (x : xs) ++ drop (n + 1) (x : xs)
= { applying take and drop }
(x : take n xs) ++ drop n xs
= { using (x : xs) ++ ys = x : (xs ++ ys) }
x : (take n xs ++ drop n xs)
= { induction hypothesis }
x : xs

Exercise 6

data Tree = Leaf Int | Node Tree Tree

-- return (m, n)
count :: Tree -> (Int, Int)
count (Leaf _) = (0, 1)
count (Node l r) = (fst cl + fst cr + 1, snd cl + snd cr)
  where
    cl = count l
    cr = count r

Induction hypothesis: count tree = (m, m + 1)

Base case:
count (Leaf _) = (0, 1)

Inductive case:
count (Node l r)
= (fst cl + fst cr + 1, snd cl + snd cr)
= (fst (ml, ml + 1) + fst (mr, mr + 1) + 1, snd (ml, ml + 1) + snd (mr, mr + 1))
= (ml + mr + 1, (ml + 1) + (mr + 1))
= (ml + mr + 1, (ml + mr + 1) + 1)

Exercise 7

instance Functor Maybe where
  fmap _ Nothing = Nothing
  fmap g (Just x) = Just (g x)

-- functor laws
fmap id = id
fmap (g . h) = fmap g . fmap h

Proof of fmap id = id

case 1:
fmap id Nothing
= { applying fmap }
Nothing
= { unapplying id }
id Nothing

case 2:
fmap id (Just x)
= { applying fmap }
Just (id x)
= { applying id }
Just x
= { unapplying id }
id (Just x)

Proof of fmap (g . h) = fmap g . fmap h

case 1:
fmap (g . h) Nothing
= { applying fmap }
Nothing
= { unapplying fmap }
fmap h Nothing
= { unapplying fmap }
fmap g (fmap h Nothing)
= { using (g . h) x = g (h (x)) }
fmap g . fmap h Nothing

case 2:
fmap (g . h) (Just x)
= { applying fmap }
Just ((g . h) x)
= { using (g . h) x = g (h (x)) }
Just (g (h (x)))
= { unapplying fmap }
fmap g (Just (h (x)))
= { unapplying fmap }
fmap g (fmap h (Just x))
= { using (g . h) x = g (h (x)) }
fmap g . fmap h (Just x)

Exercise 8

data Tree a = Leaf a | Node (Tree a) (Tree a)

instance Functor Tree where
  -- fmap :: (a -> b) -> Tree a -> Tree b
  fmap g (Leaf x) = Leaf (g x)
  fmap g (Node l r) = Node (fmap g l) (fmap g r)

-- functor laws
fmap id = id
fmap (g . h) = fmap g . fmap h

Induction hypothesis: fmap id = id

case 1:
fmap id (Leaf x)
= { applying fmap }
Leaf (id x)
= { applying id }
Leaf x
= { unapplying id }
id (Leaf x)

case 2:
fmap id (Node l r)
= { applying fmap }
Node (fmap id l) (fmap id r)
= { inductive hypothesis }
Node l r
= { unapplying id }
id (Node l r)

Induction hypothesis: fmap (g . h) = fmap g . fmap h

case 1:
fmap (g . h) (Leaf x)
= { applying fmap }
Leaf ((g . h) x)
= { using (g . h) x = g (h (x)) }
Leaf (g (h (x)))
= { unapplying fmap }
fmap g (Leaf (h (x)))
= { unapplying fmap }
fmap g (fmap h (Leaf x))
= { using (g . h) x = g (h (x)) }
fmap g . fmap h (Leaf x)

case 2:
fmap (g . h) (Node l r)
= { applying fmap }
Node (fmap (g . h) l) (fmap (g . h) r)
= { induction hypothesis }
Node (fmap g . fmap h l) (fmap g . fmap h r)
= { unapplying fmap }
fmap g (Node (fmap h l) (fmap h r))
= { unapplying fmap }
fmap g (fmap h (Node l r))
= { using (g . h) x = g (h (x)) }
fmap g . fmap h (Node l r)

Exercise 9

instance Applicative Maybe where
    -- pure :: a -> Maybe a
  pure = Just

  -- (<*>) :: Maybe (a -> b) -> Maybe a -> Maybe b
  Nothing <*> _ = Nothing
  (Just g) <*> mx = fmap g mx

-- applicative laws

pure id <*> x = x
pure (g x) = pure g <*> pure x
x <*> pure y = pure (\g -> g y) <*> x
x <*> (y <*> z) = (pure (.) <*> x <*> y) <*> z

Proof of pure id <*> x = x

case 1:
pure id <*> Nothing
= { applying pure }
Just id <*> Nothing
= { applying <*> }
fmap id Nothing
= { applying fmap }
Nothing

case 2:
pure id <*> Just x
= { applying pure }
Just id <*> Just x
= { applying <*> }
fmap id (Just x)
= { applying fmap }
Just x

Proof of pure (g x) = pure g <*> pure x

case 1:
pure (g Nothing)
= { applying pure }
Just (g Nothing)
= { unapplying fmap }
fmap g Just (Nothing)
= { unapplying <*> }
(Just g) <*> Just (Nothing)
= { unapplying pure }
pure g <*> pure Nothing

case 2:
pure (g (Just x))
= { applying pure }
Just (g (Just x))
= { unapplying fmap }
fmap g (Just (Just x))
= { applying <*> }
(Just g) <*> (Just x)
= { unapplying pure }
pure g <*> pure x

Proof of x <*> pure y = pure (\g -> g y) <*> x

case 1:
pure (\g -> g y) <*> Nothing
= { applying pure }
Just (\g -> g y)
= { applying <*> }
fmap (\g -> g y) Nothing
= { applying fmap }
Nothing
= { applying <*> }
Nothing <*> pure y

case 2:
pure (\g -> g y) <*> Just x
= { applying pure }
Just (\g -> g y) <*> Just x
= { applying <*> }
fmap (\g -> g y) (Just x)
= { applying fmap }
Just (x y)
= { unapplying pure }
pure (x y)
= { using pure (g x) = pure g <*> pure y }
pure x <*> pure y
= { applying pure }
Just x <*> pure y

Proof of x <*> (y <*> z) = (pure (.) <*> x <*> y) <*> z

case 1 (show only a case where y = Nothing):
Just x <*> (Nothing <*> Just z)
= { applying the second <*> }
Just x <*> Nothing
= { applying <*> }
fmap x Nothing
= { applying fmap }
Nothing

case 2 (show only a case where x, y and z are Just x, Just y, and Just z respectively)
Just x <*> (Just y <*> Just z)
= { unapplying pure }
Just x <*> (pure y <*> pure z)
= { using pure (x y) <*> pure x <*> pure y }
Just x <*> pure (y z)
= { unapplying pure }
pure x <*> pure (y z)
= { using pure (x y) <*> pure x <*> pure y }
pure (x (y z))
= { using f . g x = f (g (x)) }
pure (x . y z)
= { using pure (x y) <*> pure x <*> pure y }
pure (x . y) <*> pure z
= { applying pure }
Just (x . y) <*> Just z
= { unapplying fmap }
fmap ((.) x) (Just y) <*> Just z
= { unapplying <*> }
(Just ((.) x) <*> Just y) <*> Just z
= { unapplying fmap }
(fmap (.) (Just x) <*> Just y) <*> Just z
= { unapplying <*> }
(Just (.) <*> Just x <*> Just y) <*> Just z
= { unapplying first Just }
(pure (.) <*> Just x <*> Just y) <*> Just z

Exercise 10

instance Monad [] where
  -- return :: a -> [a]
  return = pure

  -- (>>=) :: m a -> (a -> m b) -> m b
  xs >>= f = [y | x <- xs, y <- f x]

-- monad laws
return x >>= f = f x
mx >>= return = mx
(mx >>= f) >>= g = mx >= (\x -> (f x >>= g))

Proof of return x >>= f = f x

return x >>= f
= { applying return }
pure x >>= f
= { applying pure }
[x] >>= f
= { applying >>= }
[z | y <- [x], y <- f y]
= { applying the first generator }
[z | z <- f x]
= { unusing list comprehension }
f x

Proof of mx >>= return = mx

[x] >>= return
= { applying >>= }
[z | y <- [x], z <- return y]
= { applying the first generator }
[z | z <- return x]
= { applying return }
[z | z <- pure x]
= { applying pure }
[z | z <- [x]]
= { unusing list comprehension }
[x]

Proof of (mx >>= f) >>= g = mx >>= (\x -> (f x >>= g))

([x] >>= f) >>= g
= { applying the second >>= }
[z | y <- ([x] >>= f), z <- g y]
= { applying >>= }
[z | y <- [z' | y' <- [x], z' <- f y'], z <- g y]
= { applying the second generator }
[z | y <- [z' | z' <- f x], z <- g y]
= { unusing inner list comprehension }
[z | y <- f x, z <- g y]
= { unapplying >>= }
f x >>= g
= { using list comprehension }
[z | z <- (f x >>= g)]
= { unapplying generator }
[z | y <- [x], z <- (\x -> (f x >>= g)) y]
= { unapplying >>= }
[x] >>= (\x -> (f x >>= g))

Exercise 11

given: comp' e c = comp e ++ c

Base case:
comp' (Val x) c
= { specification of comp' }
comp (Val x) ++ c
= { applying comp }
[PUSH n] ++ c
= { applying comp }
PUSH n : c

Inductive case:
comp' (Add x y) c
= { specification of comp' }
comp (Add x y) ++ c
= { applying comp }
(comp x ++ comp y ++ [ADD]) ++ c
= { associativity o+ ++ }
comp x ++ (comp y ++ [ADD] ++ c)
= { induction hypothesis for x }
comp' x (comp y ++ [ADD] ++ c)
= { induction hypothesis for y }
comp' x (comp' y ([ADD] ++ c))
= { applying ++ }
comp' x (comp' y (ADD : c))

17. Calculating compilers

Exercise 1

data Expr
  = Val Int
  | Add Expr Expr
  | Throw
  | Catch Expr Expr

eval :: Expr -> Maybe Int
eval (Val n) = Just n
eval (Add x y) = case eval x of
  Just n -> case eval y of
    Just m -> Just (n + m)
    Nothing -> Nothing
  Nothing -> Nothing
eval Throw = Nothing
eval (Catch x h) = case eval x of
  Just n -> Just n
  Nothing -> eval h

type Stack = [Maybe Int]

data Code = HALT | PUSH (Maybe Int) Code | ADD Code | IF Code Code
  deriving (Show)

exec :: Code -> Stack -> Stack
exec HALT s = s
exec (PUSH n c) s = exec c (n : s)
exec (ADD c) (m : n : s) = exec c (((+) <$> n <*> m) : s)
exec (IF h c) (mx : s) = case mx of
  Nothing -> exec c (exec h s)
  Just _ -> exec c s

comp :: Expr -> Code
comp e = comp' e HALT

comp' :: Expr -> Code -> Code
comp' (Val n) c = PUSH (Just n) c
comp' (Add x y) c = comp' x (comp' y (ADD c))
comp' Throw c = PUSH Nothing c
comp' (Catch x h) c = comp' x (IF (comp' h HALT) c)