Bird's Introduction to Functional Programming: Chapter 02 Simple Datatypes Notes and Solutions

Bird02.lhs

Richard Bird - Introduction to Functional Programming using Haskell [2ed]
Chapter 02: Simple Datatypes

> module Bird02 where
> import Data.Char (chr, ord)

================================================================================
2.1 Booleans

> data Bool' = False' | True'
>        deriving (Show)

Define functions using pattern matching

> not' :: Bool' -> Bool'
> not' True' = False'
> not' False' = True'

How is not e simplified?
 1. reduce e to normal form
 2. if reduction terminates and results in True', then first equation is used.
    otherwise second equation is used.
 3. If e cannot be reduced, value of not e is undefined.

So, not bottom = bottom, "not" is a strict function.

So, there are THREE boolean values: True', False', Bottom
every datatype introduces an extra anonymous value: bottom

> and', or' :: Bool' -> Bool' -> Bool'
> False' `and'` _x = False'
> True' `and'` x = x

> True' `or'` _x = True'
> False' `or'` x = x

How is e1 || e2 simplified?
 1. reduce e1 to normal form. If it fails, then value is undefined 
 2. if reduction succeeds and e1 is True, then True is returned
                              e1 is False, then x is evaluated and returned.

So, bottom || _ = bottom
    True   || bottom = True
    False  || bottom = bottom

So, || is strict in its left argument but not in its right.

If we had instead pattern matched against both arguments:
  True || True = True
  False || True = True
  True || False = True
  False || False = False
Then, the resulting function would have been strict in both arguments

========================================
2.1.1 Equality and comparison operators

> equal', nequal' :: Bool' -> Bool' -> Bool'
> equal' x y = (x `and'` y) `or'` (not' x `and'` (not' y))

> nequal' x y = not' (x `equal'` y)

"==" or equal' is a computable test for equality
"=" is used for definitions, and is mathematical equality.

So, bottom = bottom is true (everything equals itself), but bottom == bottom is bottom 
since we can't compute it.

----------------------------------------
Equality tests (==), (/=) are defined in a type class:

class Eq a where
 (==), (/=) :: a -> a -> Bool

To declare that something is in a type class we write:

instance Eq Bool where
  x == y = (x && y) || (not x && not y)
                
----------------------------------------
Ord is a subclass of Eq:

class (Eq a) => Ord a where
  (<), (<=), (>=), (>) :: a -> a -> Bool
                
only < is required because <= is just < or = , the others are negations.

----------------------------------------
Examples

> leapyear :: Int -> Bool
> leapyear y = y `mod` 4 == 0 && y `mod` 100 /= 0 || y `mod` 400 == 0

Function that determines the type of triangle

> data Triangle = Failure | Isosceles | Equilateral | Scalene
>        deriving (Show)

Assumption: x <= y <= z

> analyse :: Int -> Int -> Int -> Triangle
> analyse x y z
>  | x + y <= z  = Failure
>  | x == z      = Equilateral
>  | (x == y) || (y == z) = Isosceles
>  | otherwise = Scalene

--------------------------------------------------------------------------------
Exercise 2.1.1: define "and" and "or" using conditional expressions

> andCond, orCond :: Bool -> Bool -> Bool
> andCond x y = if x then y else False
> orCond x y = if x then True else y

--------------------------------------------------------------------------------
Exercise 2.1.2: we want False < True (because we declared it in that order)
                and False < False to be False, True < True to be False
                                   
why is this definition: (x < y) = (not x) or y incorrect?

answer: False < False would be true

--------------------------------------------------------------------------------
Exercise 2.1.3: Implication

> (==>) :: Bool -> Bool -> Bool
> True ==> False = False
> _ ==> _ = True

--------------------------------------------------------------------------------
Exercise 2.1.4: Rewrite the declaration of type class Eq by giving default definition of /=

> class Eq' a where
>  (===), (/===) :: a -> a -> Bool
>  x /=== y = not (x === y)

--------------------------------------------------------------------------------
Exercise 2.1.5 Rewrite analyse so that it doesn't assume x <= y <= z
Exercise 2.1.6 Write a function sort3 that sorts three integers into nondecreasing order.

> sort3 :: (Ord a) => a -> a -> a -> (a,a,a)
> sort3 x y z
>  | x <= y = if y <= z then (x,y,z) else (x,z,y)
>  | otherwise = if x <= z then (y, x, z) else (y, z, x)

> analyse' :: Int -> Int -> Int -> Triangle
> analyse' x y z = analyse a b c
>   where (a,b,c) = sort3 x y z
          
--------------------------------------------------------------------------------
Exercise 2.1.7: How many equations do you have to write to make Triangle an instance of Ord?
          
In general, we need to have answers for each possible pairs. There are n choose 2 = 4C2 = 6 equations
          
--------------------------------------------------------------------------------
Exercise 2.1.8: Are there numbers that can be compared by (==) but cannot be sensibly compared with <?
          
Complex numbers do not form an ordered field (http://en.wikipedia.org/wiki/Inequality_(mathematics)#Complex_numbers_and_inequalities)
          
--------------------------------------------------------------------------------
Exercise 2.1.9: == Should have the following properties:
  1. Reflexive: x == x for all x
  2. Transitive: x == y and y == z means x == z
  3. Symmetric: x == y means y == x
 Show that these hold for == on bool          
          
Recall: our definition of x equal y was (x `and` y) `or` (not x `and` (not y))         
          
1. Reflexivity
  x == x
= (x and x) or (not x and not x)
= x or (not x)       [ a and a == a]
= true since this is a tautology

  So reflexivity holds
          
2. Transitivity
  x == y and y == z 
= ((x and y) or (not x and not y)) and ((y and z) or (not y and not z))
  Case: y is True
= ((x and True) or (not x and not True)) and ((True and z) or (not True and not z))
= (x or (not x and False)) and (z or (not z and False))
= (x or (not x)) and (z or (not z))
  Since a or not a is a tautology:          
= True and True = True
   So transitivity holds in this case.
 
  Case: y is False
= ((x and False) or (not x and not False)) and ((False and z) or (not False and not z))
= (x or (not x and True)) and (z or (not z and True))
= (x or (not x)) and (z or (not z))
= True and True (since a or not a is a tautology)
  So transitivity holds here too.
          
 Thus, transitivity holds in all cases.
          
3. Symmetry:
  x == y
= (x and y) or (not x and not y)
= (y and x) or (not y and not x)   by the transitivity of and
= y == x by definition
 So, symmetry holds as well.

--------------------------------------------------------------------------------
Exercise 2.1.10 What properties of < would you like to hold?

Standard mathematical rules:

1. Transitivity: x < y and y < z means x < z
2. Irreflexivity: x < x is False for all x
3. Asymmetric: x < y means y !< x
          
================================================================================
2.2 Characters
          
Two primitives for working with chars:
          
ord :: Char -> Int
chr :: Int -> Char
          
Now we can define equality of chars (assuming we have equality of ints) by:
  x == y = ord x == ord y

Same with Ord Char
          
We can also write:
          
> isDigit, isLower, isUpper :: Char -> Bool
> isDigit c = ('0' <= c) && (c <= '9')
> isLower c = ('a' <= c) && (c <= 'z')
> isUpper c = ('A' <= c) && (c <= 'Z')


> capitalize :: Char -> Char
> capitalize c
>  | isLower c = chr $ ord c + shift
>  | otherwise = c
>  where shift = ord 'A' - ord 'a'

--------------------------------------------------------------------------------
Exercise 2.2.1 Write nextlet that returns the letter coming immediately after it

> nextlet :: Char -> Char
> nextlet 'z' = 'a'
> nextlet 'Z' = 'A'
> nextlet c = chr $ ord c + 1

Or we could use modulo arithmetic

--------------------------------------------------------------------------------
Exercise 2.2.2: digitval converts a digit to its numeric value

> digitVal :: Char -> Int
> digitVal d 
>  | isDigit d = ord d - ord '0'
>  | otherwise = error "Not a digit!"

================================================================================
2.3 Enumerations

> data Day = Sun | Mon | Tue | Wed | Thu | Fri | Sat
>        deriving (Show)

(recall that it also contains bottom as a value)

Writing Eq or Ord manually would require 7C2 = 21 equations each!
Instead, we encode it as integers and use integers for equality and ord instead.
This is basically the typeclass enum

> instance Enum Day where
>   fromEnum Sun = 0
>   fromEnum Mon = 1
>   fromEnum Tue = 2
>   fromEnum Wed = 3
>   fromEnum Thu = 4
>   fromEnum Fri = 5
>   fromEnum Sat = 6
>   toEnum 0 = Sun
>   toEnum 1 = Mon
>   toEnum 2 = Tue
>   toEnum 3 = Wed
>   toEnum 4 = Thu
>   toEnum 5 = Fri
>   toEnum 6 = Sat

Note: we must have fromEnum (toEnum x) = x, but this constraint cannot be expressed
  in Haskell

With the nums we can now write:

> instance Eq Day where
>   x == y = (fromEnum x) == (fromEnum y)

> instance Ord Day where
>   x < y = (fromEnum x) < (fromEnum y)

> workday :: Day -> Bool
> workday x = Mon <= x && x <= Fri

> restday :: Day -> Bool
> restday = not . workday 

> dayAfter :: Day -> Day
> dayAfter d = toEnum $ (fromEnum d + 1) `mod` 7

========================================
2.3.1 Automatic Instance Declarations

use the deriving clause:

data Day = Sun | Mon | Tue | Wed | Thu | Fri | Sat
        deriving (Eq, Ord, Enum, Show)
               

--------------------------------------------------------------------------------
Exercise 2.3.1 : dayBefore

> dayBefore :: Day -> Day
> dayBefore d = toEnum $ (fromEnum d - 1) `mod` 7

--------------------------------------------------------------------------------
Exercise 2.3.2 : Direction which has north south east west and write reverse

> data Direction = North | South | East | West
>              deriving (Enum, Show)

> reverseDirection :: Direction -> Direction
> reverseDirection North = South
> reverseDirection South = North
> reverseDirection East = West
> reverseDirection West = East

-OR-

> reverseDir :: Direction -> Direction
> reverseDir x
>  | even a = toEnum $ a + 1
>  | odd a = toEnum $ a - 1
>  where a = fromEnum x

--------------------------------------------------------------------------------
Exercise 2.3.3: Declare bool as a member of type class enum

> instance Enum Bool' where
>   fromEnum False' = 0
>   fromEnum True' = 1
>   toEnum 0 = False'
>   toEnum 1 = True'

================================================================================
2.4 Tuples

(a,b) is like we had written data Pair = MakePair a b. except that it has syntactic support.

Note: bottom is of type (a,b).
Note also that (bottom, bottom) is distinct from just bottom

example:

> testPair :: (a, b) -> Bool
> testPair (x,y) = True

Here:

> test1 = testPair undefined
> test2 = testPair (undefined, undefined)

*Bird02> test1
*** Exception: Prelude.undefined
*Bird02> test2
True

"More generally, if alpha is an enum with m declared constructors,
                    beta is an enum with n declared constructors
  then, (alpha, beta) has 1 + (m + 1) * (n + 1) values in total."

m + 1 because we have the m values and bottom
n + 1 because we have the n values and bottom
add 1 to the product because bottom is itself a of type (alpha, beta)


> pair :: (a -> b, a -> c) -> a -> (b, c)
> pair (f, g) x = (f x, g x)

> cross :: (a -> b, c -> d) -> (a, c) -> (b, d)
> cross (f, g) = pair (f . fst, g . snd)

Cross is from category theory.

Theorem: cross (f, g) bottom = (f bottom, g bottom)
Proof:  cross (f, g) bottom
      = pair (f . fst, g . snd) bottom     [ defn of cross ]
      = ((f . fst) bottom, (g . snd) bottom) 
      = (f (fst bottom), g (snd bottom))
      = (f bottom, g bottom)               [ fst and snd are both strict]
                 
Compare with:

> cross' (f, g) (x, y) = (f x, g y)

bottom fails to pattern match with (x, y) so cross' (f, g) bottom = bottom
So, cross is lazier than cross' and can deliver additional results
  
Some more theorems
1. fst . pair (f, g) = f
2. snd . pair (f, g) = g
3. pair (f, g) . h = pair (f . h, g . h)
4. cross (f, g) . pair (h, k) = pair (f . h, g . k)

Proof of 1
  (fst . pair (f, g)) x
= fst (pair (f, g) x)
= fst (f x, g x)
= f x
  So, fst . pair (f, g)  = f
                         
Proof of 2
  (snd . pair (f, g)) x
= snd (pair (f, g) x)
= snd (f x, g x)
= g x
  So snd . pair (f, g) = g
                         
Proof of 3                         
  (pair (f, g) . h) x
= pair (f, g) (h x)
= (f (h x), g (h x))
= ((f . h) x, (g . h) x)
= pair (f . h, g . h) x

  So, #3 holds

Proof of 4
  cross (f, g) . pair (h, k)
= pair (f . fst, g . snd) . pair (h, k)      [ defn of . ]
= pair (f . fst . pair (h, k), g . snd . pair (h, k))  [ by #3]
= pair (f . h, g . k)  [ by #1 and #2 ]
Note: This proof was conducted entirely in functions. More of this in Chapter 12

========================================
Nullary Tuple: ()
The type () has two members: bottom and ()

Use it to convert constants into functions

> pifun :: () -> Float
> pifun () = 3.14159

now we can write square . square . pifun
instead of (square . square) pi

--------------------------------------------------------------------------------
Exercise 2.4.1 Prove that cross (f, g) . cross (h, k) = cross (f. h, g . k)

  cross (f, g) . cross (h, k)
= cross (f, g) . pair (h . fst, k . snd)   [ by defn of cross ]
= pair (f . h . fst, g . k . snd)          [ since cross (f, g) . pair (h, k) = pair (f . h, g . k)]
= pair ((f . h) . fst, (g . k) . snd)      [ associativity of . ]
= cross (f . h, g . k)                     [ by defn of cross ]

--------------------------------------------------------------------------------
Exercise 2.4.2 datatype declaration for triple

> data Triple a b c = MakeTriple a b c
>             deriving (Show)

--------------------------------------------------------------------------------
Exercise 2.4.3 

First triple has d,m,y of current date
Second has d,m,y of birthdate
Return age as a whole number of years

> birthday :: (Integer, Integer, Integer) -> (Integer, Integer, Integer) -> Integer
> birthday (d,m,y) (dd, mm, yy) = y - yy + shift
>    where shift = if m > mm || m == mm && d >= dd then 0 else -1 

Shift is just calculating if we're on or past the birthdate
           
--------------------------------------------------------------------------------
Exercise 2.4.4 Can we have (a,b) as a member of Enum if both a and b are Enum?
           
Yes. Since a and b are enum, both a and b are countably infinite.
So, we can have (a,b) be an enum by performing the mapping in the same way we 
map rationals to the naturals.
           
================================================================================
2.5 Either
          
Example of a type whose value depends on other types:

Either a b = Left a | Right b

Either gives us a new type that has "combined" a and b

> case' :: (a -> c, b -> c) -> Either a b -> c
> case' (f, _g) (Left  x) = f x
> case' (_f, g) (Right y) = g y

Using case', we can define plus (category theory term)

> plus :: (a -> c, b -> d) -> Either a b -> Either c d
> plus (f, g) = case' (Left . f, Right . g)

algebraic properties of case and plus:
1. case (f, g) . Left = f
2. case (f, g) . Right = g
3. h . case (f, g) = case (h . f, h . g)
4. case (f, g) . plus (h, k) = case (f . h, g . k)

Proof of 1
  case (f, g) . Left 
= case (f, g) (Left x)                
= f x                  [ by definition of case]

Proof of 2
  case (f, g) . Right
= case (f, g) (Right y)
= g y                  [ by definition of case ]

Proof of 3: by cases
  Case 1: input is Left x
LHS = h (case (f, g) Left x)
    = h (f x)
RHS = case (h . f, h . g) Left x
    = (h . f) x
  Case 2: input is Right x
LHS = h (case (f, g) Right x)
    = h (g x)
RHS = case (h . f, h . g) Right x
    = (h . g) x

Proof of 4
  case (f, g) . plus (h, k) 
= case (f, g) . case (Left . h, Right . k)     [by definition of case]
= case ( case (f, g) . Left . h, case (f, g) . Right . k)      [by #3]
= case ( (case (f, g) . Left) . h, (case (f, g) . Right) . k)  [ by associativity of compose ]
= case ( f . h, g . k)     [ Since case (f, g) (Left x) = f x and case (f, g) (Right x) = g x ]

--------------------------------------------------------------------------------
Exercise 2.5.1: Define a function of source Either Bool Char that behaves differently on
the three arguments: Left bottom, Right bottom, and bottom

> ex251 :: Either Bool Char -> Char
> ex251 (Right x) = 'a'
> ex251 (Left x) = undefined

ex251 bottom = bottom because we try to evaluate it
ex251 (Right bottom) = 'a' 
ex251 (Left bottom) = undefined

--------------------------------------------------------------------------------
Ex 2.5.2: Prove that case (f, g). plus (h, k) = case (f . h, g . k)
 Proved earlier.

================================================================================
2.6 Type Synonyms

use type to give alternative names:

> type Roots = (Float, Float)
> type Angle = Float

--------------------------------------------------------------------------------
2.6.1 New Types

when you use type, you're just giving it a new name.
so, == is defined for roots because we have it defined for floats.

This is a problem because maybe we want equality of Angle to be mod 2 pi

we could say data Angle = MakeAngle Float

but there are two problems:
1. We need to keep wrapping and unwrapping things to work with them
2. Since MakeAngle bottom is also of type angle, we have an extra element

So, Angle is not isomorphic to Float

Solution: use newtype
  newtype Angle = MakeAngle Float
               
1. newtype is strict so MakeAngle Bottom is not actually of type Angle
2. there is no boxing unboxing overhead at runtime 

--------------------------------------------------------------------------------
Exercise 2.6.1
Want to treat two distances as equal if they are less than 10 miles apart.

> distanceEqual :: (Ord a, Num a) => a -> a -> Bool
> distanceEqual x y = x == y || abs (x - y) < 10

can we call this == if Distance is a type synonym? No because then it just
uses the == of the type it is a synonym for.

--------------------------------------------------------------------------------
Exercise 2.6.2: Show that Jane and Dick are different:

> data Jane = MkJane Int
> newtype Dick = MkDick Int

> nonstrict :: Either Jane Dick -> String 
> nonstrict (Left (MkJane _)) = "Jane"
> nonstrict (Right (MkDick _)) = "Dick"

*Bird02> nonstrict (Right undefined)
"Dick"
*Bird02> nonstrict (Left undefined)
"*** Exception: Prelude.undefined

I'm showing the constructor pattern match case from
http://www.haskell.org/haskellwiki/Newtype

================================================================================
2.7 Strings

type String = [Char]

there's a Show class to display objects:

class Show a where
  showsPrec :: Int -> a -> String -> String

(see 5.3 and 7.3 for more details on the arguments)

--------------------------------------------------------------------------------
2.7.1 Put in ascending order: McMillan, Macmillan, MacMillan

MacMillan, Macmillan, McMillan

why? Lexicographic order and
*Bird02> 'm' > 'M'
True

*Bird02> "MacMillan" > "McMillan"
False
*Bird02> "MacMillan" < "McMillan"
True
*Bird02> "Macmillan" < "McMillan"
True

--------------------------------------------------------------------------------
2.7.2 What are the values of:

show (show 42) 
= show "42"
= "\"42\""

show 42 ++ show 42
= "42" ++ "42"
= "4242"

--------------------------------------------------------------------------------
2.7.3 showDate

e.g. showDate (10, 12, 1997) = "10 December, 1997"

> months = ["January", "February", "March", "April", "May", "June", "July", "August",
>           "September", "October", "November", "December"]            

> showDate (d, m, y) = showDay d ++ " " ++ showMonth m ++ " " ++ showYear y

> showDay :: Integer -> String
> showDay d = show d ++ suffix (d `rem` 10)
>  where suffix 1 = "st"
>        suffix 2 = "nd"         
>        suffix 3 = "rd"
>        suffix _ = "th"

> showMonth m = months !! (m - 1)
> showYear y = show y

*Bird02> showDate (10, 12, 1997)
"10th December 1997"

================================================================================
2.8 Further Notes 

Modern accounts of boolean algebra and logic:
  Ben-Ari (1993): Mathematical Logic for Computer Science
  Burke and Foxley (1996): Logic and its Applications
  Gries and Schneider (1995): A logical approach to discrete Math
               
Theoretical Foundations of Type classes:
  Wadler and Blott (1989): How to make ad-hoc polymorphism less ad-hoc
  Jones (1992): Qualified Types: Theory and Practice
  Jones (1995): A system of constructor classes: overloading and implicit higher-order polymorphism

Category Theory:               
  Barr and Wells (1995): Category Theory for Computer Science
  Pierce (1991): Basic Category Theory for Computer Scientists
  Bird and de Moor (1997): The Algebra of Programming