2. Lists and user-defined types

Lists

Linked lists are an important primitive, we can define them in the following way:

• [] :: [a] - empty list
• (:) :: a -> [a] -> [a] - add element to list (“cons”)
• head :: [a] -> a - return first element of non-empty list
• tail :: [a] -> [a] - return remainder of non-empty list

Functions on lists

-- functions on lists are usually defined using pattern matching
size :: [a] -> Int
size [] = 0
size (x :: xs) = 1 + size xs
 
-- elem' x y - check whether an element exists in x at y
 
-- take' n l - return the first n elements of list l
take' n l :: Int -> [a] -> [a]
take' 0 1 = []
take' n [] = []
take n (x :: xs) = x : (take' (n - 1) xs)

User-defined types

We can define new types by declaring data and type constructors:

data Nat = Zero | Succ Nat
-- Nat is a new type
-- Zero is a data constructor
-- Succ is a data constructor
 
data Seq a = Empty | Cons a (Seq a)
-- Seq is a polymorphic and recursive type constructor
-- Cons is a data constructor
-- Empty is a data constructor
 
-- Data constructors can be used to build terms of a type:
Zero :: Nat
(Succ (Succ Zero)) :: Nat
 
-- Data constructors can be used in pattern matching:
isempty Empty = True
isempty (Cons x y) = False
 
-- Example: write definition for data type `Tree a` representing binary trees
-- (use data constructors Leaf and Branch)
data Tree a = Leaf a | Branch (Tree a) (Tree a)
 
-- We could then determine the height of the tree as such:
height :: Tree a -> Int
height (Leaf _) = 1
height (branch l r) =
	1 + max (height l) (height r)
		where max x y = if x > y then x else y

Structural Induction

To reason with recursive types, we can use the Principle of Structural Induction.

$$(P(0)\wedge \forall n.(P(n)\Rightarrow P(n+1)))\iff \forall n.P(n)$$

Example: Prove by induction that Zero is a natural element, that is, for all Nat numbers $n$: add n Zero = n

In the case of Nat, to prove a property $P$ for all elements of Nat, we have to:

1. Prove $P(\text{zero})$ - base case of induction
2. Prove that if $P(n)$ holds - induction hypothesis, then $P(\text{Succ }n)$ holds.

We can define addition on Nat by pattern matching:

add Zero x = x
add (Succ x) y = Succ (add x y)

Hence:

1. Base case: prove add Zero Zero = Zero, use definition of add
2. Induction: by definition of add:

• add (Succ n) Zero = Succ (add n Zero) which is equal to Succ n, by I.H.

Example: Prove by induction that $\text{sumNat }n=\frac{n(n+1)}{2}$ for all natural numbers $n$.

sumNat x
	| x == 0 = 0
	| x > 0 = x + sumNat (x - 1)
	| otherwise = error "negative arg."

1. Base case: $\text{sumNat }0=\frac{0\times 1}{2}=0$
2. Induction: Induction Hypothesis (IH): assume that for a given arg. $n$ that $\text{sumNat }n=\frac{n(n+1)}{2}$. todo complete proof