Bird's Introduction to Functional Programming: Chapter 01 Fundamental Concepts Notes and Solutions

Bird01.lhs

Richard Bird - Introduction to Functional Programming using Haskell [2ed]
Chapter 01: Fundamental Concepts

> module Bird01 where
> import Prelude hiding (pi, signum, abs)

================================================================================
1.1 Sessions and Scripts

Some definitions from the book. I've used more general type signatures.

> square :: Num a => a -> a
> square x = x * x

> smaller :: Ord a => a -> a -> a
> smaller x y
>  | x < y = x
>  | otherwise = y

"Note that definitions are written as equations between certain kinds of expression"

Definition introduces a *binding* of a *name* to the definition.
A set of bindings is called *environment*

> delta :: Floating a => a -> a -> a -> a
> delta a b c = sqrt $ square b - 4 * a * c

Exercise 1.1.1
Using square, write quad

> quad :: Num a => a -> a
> quad = square . square

Exercise 1.1.2
Write "greater"

> greater :: Ord a => a -> a -> a
> greater x y 
>  | x > y = x
>  | otherwise = y

Exercise 1.1.3
Compute area of circle, use 22/7 as approximation to pi.

> pi :: Double
> pi = 22/7

> areaCircle :: Double -> Double
> areaCircle r = pi * square r

================================================================================
1.2 Evaluation

Two different evaluation strategies for square (3 + 4)

Strategy 1: reduce arguments first
  square (3 + 4)
= square 7       [ by + ]
= 7 * 7          [ by square ]
= 49             [ by * ]

49 is in "normal" or canonical form

Strategy 2: apply functions first, evaluate arguments only when necessary
  square (3 + 4)
= (3 + 4) * (3 + 4) [ by square]
= 7 * (3 + 4)       [ by + ]
= 7 * 7             [ by + ]
= 49                [ by * ]


"Characteristic feature of functional programming is that if two reduction sequences
 both terminate, they both give the same result."

                 
> three :: Integer -> Integer
> three x = 3

> infinity :: Integer
> infinity = infinity + 1

Even though it isn't clear what integer is being defined by infinity, we can still
use it. Simplification of three infinity:

Strategy 1 : Evaluating arguments first
  three infinity
= three (infinity + 1)         [by "infinity"]
= three ((infinity + 1) + 1)   [by "infinity"]
= ...

Strategy 2: Evaluating the function first
  three infinity
= 3                            [ by "three"]

"Some ways of simplifying an expression may terminate some may not."
Chapter 7: Lazy evaluation: guarantees termination whenever termination is possible

--------------------------------------------------------------------------------
Exercise 1.2.1
Suppose that * needs to reduce both arguments to normal form before it can proceed
Does square infinity terminate?

No. Any attempt to reduce "infinity" is doomed to fail because it is a nonterminating
recursion. So square infinity will not terminate.

--------------------------------------------------------------------------------
Exercise 1.2.2
How many terminating reduction sequences are there for square (3 + 4)?

We've seen two sequences before: evaluating arguments first, applying functions first.
When we applied functions, we picked a left-to-right order of evaluation. We could
also do a right-to-left evaluation. 

If there are n arguments, we have n! permutations in which we could evaluate the exprs.
In this case, we have 2 arguments to * that need to be reduced, so 2! = 2 ways.

So total: 3

--------------------------------------------------------------------------------
Exercise 1.2.3
(I have written the language of expressions in haskell)

> data Expr = Zero | Succ Expr | Pred Expr
>        deriving (Show)

> exprEvaluate :: Expr -> Expr
> exprEvaluate (Succ (Pred e)) = exprEvaluate e
> exprEvaluate (Pred (Succ e)) = exprEvaluate e
> exprEvaluate e = e

a. Simplify the expression

> ex123a = (Succ . Pred . Succ . Pred . Pred) Zero

   Succ (Pred (Succ (Pred (Pred Zero))))
=  Succ (Pred (Pred Zero))                [ since Succ (Pred x) = x ]
=  Pred Zero                              [ same reason ]
this is the canonical form since we don't have any more rules 

Bird01> exprEvaluate ex123a
Pred Zero

b. How many ways can the reduction rules be applied to this expression?
We could also start from the innermost expression and get the same result.

Since we're nesting functions of a single arity, at each step, we have only 1! = 1
permutation to work with. So, it's either inside out or outside in.

c. Prove that the process of reduction must terminate for all expressions.
[Hint: Define an appropriate notion of expression size, show that each reduction step
       does indeed reduce size.]
           
I'm going to use "depth" of an expression as my metric for expression size.

That is: 

> depth :: Expr -> Integer
> depth Zero = 0
> depth (Succ x) = 1 + depth x
> depth (Pred x) = 1 + depth x

*Bird01> depth ex123a
5

*Bird01> depth $ exprEvaluate ex123a
1

To prove that reduction terminates, we will show that depth e >= depth $ exprEvaluate e

Proof is by cases:

Case: when expression is not of the form Succ (Pred x) or Pred (Succ x)
 In that case, we just return the expression itself.
 So depth x = depth $ exprEvaluate x

Case Succ (Pred x): Proof is by induction on x
  Note: depth (Succ (Pred x)) = 2 + depth x               
        exprEvaluate (Succ (Pred x)) = exprEvaluate x

  Base Case: Suppose that x is of the form in case 1 so it can't be reduced further
        then we get x.
        Since 2 + depth x > depth x, the reduction terminates.
  
  Inductive Case
    Inductive hypothesis is that depth (exprEvaluate x) <= depth x

    So, 2 + depth x >= depth (ExprEvaluate x)
    
Case Pred (Succ x): Proof is the same as in the previous case.

So, in each of the three cases, the size of the expression is non-increasing. Hence, reduction terminates.

--------------------------------------------------------------------------------
Exercise 1.2.4

"add" is also a data type. Reduction rules:

add (zero, e2) = e2
add (succ (e1), e2) = succ(add (e1, e2))
add (pred (e1), e2) = pred (add (e1, e2))

Simplify: add (succ (pred (zero)), zero)

Strategy 1: evaluate arguments first
  add (succ (pred (zero)), zero)
= add (zero, zero)                 [ since succ (pred zero) = zero ]
= zero                             [ since add(zero, zero) = zero ]

Strategy 2: evaluate function first
  add (succ (pred (zero)), zero)
= succ (add(pred(zero)) zero))     [ since add (succ (e), f) = succ (add (e,f)) ]
  don't have a rule for succ(add ...), so we must evaluate add
= succ (pred (add(zero, zero)))      [ since add (pred (e), f) = pred (add (e,f))]
= succ (pred (zero))                 [ add zero]
= zero                               [ succ pred]

--------------------------------------------------------------------------------
Exercise 1.2.5

Define size of expression as:

size(zero) = 1
size(succ (e)) = 1 + size e
size(pred (e)) = 1 + size e
size(add (e1, e2)) = 1 + 2 * (size (e1) + size (e2))

Show that application of any reduction rule reduces expression size.

I've shown this to be the case for zero, succ and pred. So I need to show that
it is true for add as well.

1. add(zero, e2) = e2
LHS = size(add(zero, e2))
    = 1 + 2 * (size zero + size e2)
    = 1 + 2 * (1 + size e2)
    = 3 + size e2
RHS = size e2

2. add(succ(e1), e2) = succ(add(e1, e2))
LHS = size(add(succ(e1), e2))
    = 1 + 2 * (size (succ e1) + size e2)
    = 1 + 2 * (1 + size e1 + size e2)
    = 3 + 2 * (size e1 + size e2)

RHS = size(succ(add(e1, e2)))
    = 1 + size(add (e1, e2))
    = 1 + 1 + 2 * (size e1 + size e2)
    = 2 + 2 * (size e1 + size e2)

3. add(pred(e1), e2) = pred(add(e1, e2))
   exactly the same as 2 since size (pred (e1)) == size (pred (e2))

Since every reduction rule except the one where we pass the argument unchanged
leads to a decrease in the expression size, the evaluation process must terminate.

================================================================================
1.3 Values

Values vs Representations
2 is a representation of the abstract concept of "two things"
1 + 1 represents the same abstract concept
II (roman) represents the same concept

evaluator: prints the canonical form of a value

We want to be able to say that every syntactically well-formed expression produces a value
but: what is sqrt -1? (when you don't have complex numbers)
     what is 1/0 ? 
                   
So, _|_ (bottom) means undefined value of a given type.       
in our definition, infinity was bottom of type integer.

Strict and Non-strict functions:
     three infinity = 3
but  square infinity = doesn't terminate aka bottom

 If f bottom = bottom, then f is a strict function
 So, square is strict, but three is nonstrict
                   
Lazy evaluation allows nonstrict definitions.

--------------------------------------------------------------------------------
Exercise 1.3.1

> multiply :: Num a => a -> a -> a
> multiply x y = if x == 0 then 0 else x * y

Assume that x == y proceeds by reducing e1 and e2 to normal form and testing
whether the two are identical. 

a. What is the result of multiply 0 infinity?
   We reduce x to its normal form i.e. 0 and test if it is 0
   Since it is, we return 0. 

b. What is the value of multiply infinity 0?
   Attempt to reduce infinity to normal form doesn't terminate.
   So, we return bottom.
                                       
So, multiply is strict in its left argument.

--------------------------------------------------------------------------------
Exercise 1.3.2

Suppose we define h by the equation: h x = f (g x). Show that if f and g are
both strict then so is h.

Direct Proof
h bottom = f (g bottom)
         = f bottom       [ since g is strict ]
         = bottom         [ since f is strict ]

Note, this means that as long as the outermost function is nonstrict, we can still
have h be nonstrict.

================================================================================
1.4 Functions

f :: A -> B means
f maps each element of the _source type_ A to a unique element in the _target type_ B

three associates every number (including bottom) to a single number, 3.
square associates every well-defined number with its square, and bottom with bottom.

========================================
1.4.1 Extensionality

Two functions f and g are equal if f x = g x for all x.

(Recall: intensional and extensional equality of functions from the functions chapter
         in discrete mathematics using a computer)

> double', double'' :: Num a => a -> a
> double' x = x + x
> double'' = (2 *)

double' and double'' are extensionally equal (since they always produce same results)
  - actually maybe not for floats. 
but they're not intensionally equal because they have different definitions

========================================
1.4.2 Currying

Compare the smaller from earlier with this one:

> uncurriedSmaller :: Ord a => (a, a) -> a
> uncurriedSmaller (x, y) = if x < y then x else y

This is a function of a single argument that is a pair of items that are ordered.
It returns the smaller

The smaller from earlier was a function of one argument x, that returned a new function
of a single argument y which would return x if y was larger than it.

For currying to work properly, want function application to associate to the left:
smaller 3 4 means (smaller 3) 4 

But this means that: square square 3 doesn't make any sense because we try to do:
 (square square) 3. can't apply square to a function!

Advantage of currying:
1. reduce parens
2. returns another function that might me useful in its own right.

e.g.

> twice :: (a -> a) -> a -> a
> twice f x = f (f x)

Now we can say:

> quad' :: Num a => a -> a
> quad' = twice square 

If we had twice be uncurried:

> twiceU :: (a -> a, a) -> a
> twiceU (f, x) = f (f x)

Then, we can't write quad without mentioning the argument as well:

> quad'' :: Num a => a -> a
> quad'' x = twiceU (square, x)


Converting an uncurried function into a curried one:

> curry' :: ((a, b) -> c) -> a -> b -> c
> curry' f x y = f (x,y)

{Exercise to reader} write uncurry

> uncurry' :: (a -> b -> c) -> (a, b) -> c
> uncurry' f (x,y) = f x y

========================================
1.4.3 Operators

A function written in an infix notation is an operator.

in haskell: write name of function inside backquotes to make it into an operator.

> eg143 = 1 `elem` [1..10]

========================================
1.4.4 Sections

Suppose @ is an arbitrary binary operator.

Then, (@ x) and (x @) are also functions with the definitions:

(x @) y = x @ y
(@ y) x = x @ y

These are called sections.

========================================
1.4.5 Precedence

We'll use the standard arithmetic precedence rules.

Function application has highest precedence.

Exponentiation has higher than any arithmetic op.

========================================
1.4.6 Association

Operators associate either to the left or the right.

function application associates to the left.

operators on same level of precedence associate to the left as well:
 5 - 4 - 2 is (5 - 4) - 2 not 5 - (4 - 2)

Associativity: different concept
 If (x @ y) @ z = x @ (y @ z), then @ is said to be associative.
 e.g. +, *

========================================
1.4.7 Functional Composition

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

Written as "." in Haskell

Composition is associative so (f . g) . h = f . (g . h) so can omit brackets altogether.

--------------------------------------------------------------------------------
Exercise 1.4.1

f :: Integer -> Integer
g :: Integer -> (Integer -> Integer)

h x y = f (g x y)

a. What is the type of h?
   x and y have to be Integers since they are input to g
                  
   type of g x y is Integer
   type of f (g x y) is Integer as well 

   So type of h is: Integer -> Integer -> Integer

b. Which of the following are true?
   h = f . g ?
   No. since "." assumes that the functions take in a single variable, (f . g) x y
       is actually ((f . g) x) y
       but f is Integer -> Integer whereas g x is (Integer -> Integer)
       so can't pass g x to f. This whole expression is an error.

   h = f . (g x)?
   Yes. g x has type Integer -> Integer, f has type Integer -> Integer
        combining them with . gives a function of type Integer -> Integer
        when we pass an argument y to h, we get (f . (g x)) y = f ((g x) y) = f (g x y)

   h x y = (f . g) x y
   No because g x is not Integer; it is Integer -> Integer
                  
--------------------------------------------------------------------------------
Exercise 1.4.2

What is the type of the curried delta?
it is Num a => a -> a -> a -> a
(my delta has always been curried :D)

--------------------------------------------------------------------------------
Exercise 1.4.3

the type of log which takes in a base and a number would be:

log :: Num a => a -> a -> a
log base number = {log of number in the given base}

Actually that is incorrect. If we pass in an integer as a base and a number,
the log can be floating. So it should actually be:

log :: (Num a, b, c) => a -> b -> c

Some number as the base, some number as the thing you want to get the log of
and get some number out.

--------------------------------------------------------------------------------
Exercise 1.4.4 One appropriate type for definite integral function

integral:: (Num a, b) => (a -> b) -> a -> a -> b
                       f          l    u    ans

f is the function of one argument you're integrating over
l is the lower limit
u is the upper limit
ans is the answer

--------------------------------------------------------------------------------
Exercise 1.4.5 Give examples of functions with the following types:

(Integer -> Integer) -> Integer
e.g. +, * 

Integer -> Integer -> Integer -> Integer

e.g. max3

--------------------------------------------------------------------------------
Exercise 1.4.6 Which are true?

a. (*) x = (* x)?
     ((*) x) y 
   = x * y         [ prefix notation to infix ]
   = y * x         [ commutativity of * ]
   = (* x)         [ convert to section form ]
                  
b. (+) x = (x +) ?
   ((+) x) y
  = x + y          [ prefix to infix ]
  = (x +)          [ section form ]

c. (-) x = (- x)?
   LHS is a function Num a => a -> a
   RHS is a Function Num a => a
   So not equal.                  
                  
--------------------------------------------------------------------------------
Exercise 1.4.7

Write uncurry: done earlier.

================================================================================
1.5 Definitions

========================================
Using Guards:

> signum :: (Ord a, Num a) => a -> a
> signum x
>  | x < 0 = -1
>  | x == 0 = 0
>  | otherwise = 1

========================================
Recursive Definitions

> fact :: Integer -> Integer
> fact 0 = 1
> fact n = n * fact (n - 1)

e.g. fact 1 reduction:
  fact 1 
= 1 * fact (1 - 1)
= 1 * fact 0
= 1 * 1
= 1

Problem: If -ve integer passed, the function never terminates
Solution: catch it with a guard

> fact' :: Integer -> Integer
> fact' n
>  | n == 0 = 1
>  | n > 0 = n * fact (n - 1)
>  | n < 0 = error "Negative number passed to factorial"

"There are other ways to define fact, and we'll discuss them later in the book"

========================================
Local Definitions

example: quadratic solver

> quadSoln :: (Ord a, Floating a) => a -> a -> a -> (a,a)
> quadSoln a b c
>  | disc < 0 = error "The quadratic equation has imaginary roots"
>  | otherwise = ((- b + sqdisc) / (2* a), (- b - sqdisc) / (2 * a))
>  where disc = b ** 2 - 4 * a  * c
>        sqdisc = sqrt disc

--------------------------------------------------------------------------------
Exercise 1.5.1

> fib :: Integer -> Integer
> fib 0 = 1
> fib 1 = 1
> fib n
>  | n > 0 = fib (n - 2) + fib (n - 1)
>  | otherwise = error "Negative number passed to fib"

This is exponential time!

better fib:

> fib' :: Int -> Integer
> fib' = (fiblist !!)
>  where fiblist = 0 : 1 : zipWith (+) fiblist (tail fiblist)

This is linear time
         
--------------------------------------------------------------------------------
Exercise 1.5.2
         
> abs :: Integer -> Integer         
> abs n
>  | n > 0 = n
>  | otherwise = - n

================================================================================
1.6 Types

Strong Typing: type of an expression depends only on the type of its component expressions

Polymorphic types: via type variables.

e.g. with (.), we wrote:

(.) :: (b -> c) -> (a -> b) -> (a -> c)

a,b,c are type variables

Note: error should be usable in every function. Its input is a string. So, 

error :: String -> a

--------------------------------------------------------------------------------
Exercise 1.6.1: Give polymorphic types for the following functions

const x y = x
const :: a -> b -> a

subst f g x = f x (g x)
subst :: (a -> b -> c) -> (a -> b) -> a -> c
 How?
 - fix x :: a
 - then, g :: a -> b 
 - then, f :: a -> b -> c
 - then, f x (g x) :: c

apply f x = f x
apply :: (a -> b) -> a -> b

flip f x y = f y x
flip :: (b -> a -> c) -> a -> b -> c

--------------------------------------------------------------------------------
Ex 1.6.2 Define a function swap so that: flip (curry f) = curry (f . swap)

Since curry :: ((a, b) -> c) -> a -> b -> c, f :: (a, b) -> c
      flip (curry f) :: b -> a -> c
                 
Want: curry (f . swap) :: b -> a -> c

> swap :: (a, b) -> (b, a)
> swap (x,y) = (y,x)

--------------------------------------------------------------------------------
Ex 1.6.3 Find polymorphic type assignments for

strange f g = g (f g)

Suppose: f :: a -> b
         g :: c -> d

  Since g takes the output of f, we must have b = c.
  Since f is consuming g as an argument, we must have a = c -> d
  Strange produces the output of g, so the overall output is also d                

  So, we have strange :: ((c -> d) -> c) -> (c -> d) -> d

stranger f = f f

Suppose: f :: a -> b

  Since we have f f, f should be able to consume its own output
  So, a :: a -> b.
               
  Infinite type?
   Yup. haskell complains saying: Occurs check: cannot construct the infinite type: t1 = t1 -> t              
               
--------------------------------------------------------------------------------
Ex 1.6.4 Find polymorphic type assignment for square x = x * x

We have (*) :: Num a => a -> a -> a

So, square :: Num a => a -> a

================================================================================
1.7 Specifications

Specification: description of the task
Implementation: program that satisfies spec

Example of a spec:
  increase :: Integer -> Integer
  increase x > square x, whenever x >= 0

Example of an implementation (mine is different from the book's)
  increase = (1+) . square

Proof that this meets spec:
  increase x 
= ((1+) . square) x
= 1 + (square x)       
  which is greater than square x for all x 
               
This was an example where we wrote an implementation and verified that it met the spec.
We can also start with a very simple (and inefficient) definition and derive a faster program:

Start with quad x = x * x * x * x
Needs 4 multiplications, expensive with arbitrary precision arithmetic.

  quad x 
= x * x * x * x
= (x * x) * (x * x)     [ by associativity of * ]
= square x * square x   [ by definition of square ]
= square (square x)     [ definition of square ]

We have gone from four multiplications to two. 
We'll see more sophisticated examples of this later on.

--------------------------------------------------------------------------------
Exercise 1.7.1 

Give another definition of increase that meets its specification:

increase x = (square . square) x

Proof that this meets spec:
  (square (square x))
= (square x) * (square x)
  Since (square x) > 0 for all x, square x * square x > square x for all x.
               
================================================================================
1.8 Chapter Notes (Further Reading)

For further information on the denotational aspects of functional languages:
 Stoy (1977) : Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory
 Gordon (1979): The Denotational Description of Programming Languages, an Introduction

For implementation of lazy functional language:
 Peyton Jones (1987): The Implementation of Functional Programming Languages
 Peyton Jones and Lester (1991): Implementing Functional Programming Languages

For formal derivation of programs from their specifications (target is imperative language)
 Morgan (1996): Programming from Specifications [2nd edition]
 Kaldewaij (1990): Programming: The Derivation of Algorithms

For functional and relational treatment of program derivation in categorical setting:
 Bird and de Moor (1997): The Algebra of Programming
 (advanced text, read after this one)