The length of the empty list, [], also known as nil, is zero, and the length of a non-empty list, (_:xs), is 1 plus the length of xs. The result of appending the empty list, [], and a list, xs, is just xs. The result of appending a non-empty list, (h:t), and xs is a list whose head is h and whose tail is append t xs.

module List
 (module List, module Unique, module Reverse)-- export all
where
import Unique
import Reverse

len []     = 0
len (_:xs) = 1 + len xs

append []    xs = xs          -- same as (++) in H98
append (h:t) xs = h:(append t xs)

A small theorem

append l1 (append l2 l3) = append (append l1 l2) l3, for all lists l1, l2 and l3, i.e. list append is associative.

base case, l1 = []

LHS

= append [] (append l2 l3)

= append l2 l3

= append (append [] l2) l3

= RHS

general case, l1 = h:t

LHS

= append (h:t) (append l2 l3)

= h:(append t (append l2 l3))

= h:(append (append t l2) l3) -- by induction on |l1|

= append (h:(append t l2)) l3

= append (append (h:t) l2) l3

= RHS

Try that on C++ code!

Accumulating speed

The fast, i.e. O(|L|)-time, way to reverse a list L uses an auxiliary function, r, which has two parameters, an input parameter and an accumulating parameter, ans. The accumulating parameter grows as the input list shrinks:

module Reverse (module Reverse) where

rev xs =                      -- O(|xs|)-time
 let
   r []    ans = ans          -- done
   r (h:t) ans = r t (h:ans)  -- accumulate
 in r xs []

We can prove that the fast reverse function above is equivalent to the obvious but slow version:

Definition of the obvious but slow list reversal function:

slowR [] = []

slowR (h:t) = append (slowR t) [h]

 

Claim:   slowR xs = rev xs, for every list xs.

Proof:

base case, xs = []

LHS = slowR [] = [] = r [] [] = rev [] = RHS

general case, xs = h:t

LHS

= slowR (h:t)

= append (slowR t) [h] -- defn of slowR

= append (rev t) [h] -- by induction on |t|

= append (r t []) [h] -- defn of rev

= r t (append [] [h]) -- see note below

= r t [h] -- defn of append

= r (h:t) [] -- defn of r

= rev (h:t) -- defn of rev

= RHS

Note:   append (r ws ps) qs = r ws (append ps qs), for every triple of lists ws, ps, qs.

base case, ws=[]

LHS

= append (r [] ps) qs

= append ps qs -- defn of r

= r [] (append ps qs) -- defn of r

= RHS

general case, ws = h:t

LHS

= append (r (h:t) ps) qs

= append (r t (h:ps)) qs -- defn of r

= r t (append (h:ps) qs) -- by induction on |t|

= r t (h:(append ps qs)) -- defn of append

= r (h:t) (append ps qs) -- defn of r

= RHS

Note that slowR xs takes O(|xs|²)-time because of those calls on append.

Duplicates removed

Function unique removes duplicate values from a list. The result is a list, r, which is built by a function u. This function depends on r, so u and r are mutually recursive, making this an example of a circular program [more].

module Unique ( module Unique ) where

unique xs =                     -- remove duplicates
 let
  r = u xs 0                         -- result list
  u []     _ = []                    -- build result
  u (x:xs) n = if member x r n then u xs n
               else x:(u xs (n+1))
  member e xs     0 = False
  member y (x:xs) n = x==y || member y xs (n-1)
 in r

Note that unique operates correctly, i.e. lazily, on infinite lists.

The simple driver `Main.hs' exercises the above operations on lists.

module Main where
import List

main =
  print ( append [1,2,3] [4,5,6] ) >>
  print ( rev [1,2,3,4] ) >>
  print ( unique [1,2,1,3,2,4] )

Note that Haskell 98 provides a large number of useful operations on lists in Prelude PreludeList (H98 A1 p105).