LA home
 FP,  λ
 Logic,  π


NB. Haskell uses the infix colon, `:' for the list constructor, also known as `cons', cf `.' in Lisp, and `::' in SML.

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
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 = []
= append [] (append l2 l3)
= append l2 l3
= append (append [] l2) l3
general case, l1 = h:t
= 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

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
   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.
base case, xs = []
LHS = slowR [] = [] = r [] [] = rev [] = RHS
general case, xs = h:t
= 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
Note:   append (r ws ps) qs = r ws (append ps qs), for every triple of lists ws, ps, qs.
base case, ws=[]
= append (r [] ps) qs
= append ps qs -- defn of r
= r [] (append ps qs) -- defn of r
general case, ws = h:t
= 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

Note that slowR xs takes O(|xs|2)-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
  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).

L.A. 8/2002
window on the wide world:

Computer Science Education Week

free op. sys.
free office suite,
ver 3.4+

~ free photoshop
web browser
like it says!

(:) cons
[x1,...] list
[ ]list
(++) append
\ λ :-)
:: has type

© L. Allison   (or as otherwise indicated),
Faculty of Information Technology (Clayton), Monash University, Australia 3800 (6/'05 was School of Computer Science and Software Engineering, Fac. Info. Tech., Monash University,
was Department of Computer Science, Fac. Comp. & Info. Tech., '89 was Department of Computer Science, Fac. Sci., '68-'71 was Department of Information Science, Fac. Sci.)
Created with "vi (Linux + Solaris)",  charset=iso-8859-1,  fetched Sunday, 28-Dec-2014 03:32:14 EST.