Lists

home1 home2
 Bib
 Algorithms
 Bioinfo
 FP
 Logic
 MML
 Prog.Lang
and the
 Book

FP
 Haskell
  Haskell98
   Lists

Alg's:Lists
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
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|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
 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).


L.A. 8/2002
Coding Ockham's Razor, L. Allison, Springer

A Practical Introduction to Denotational Semantics, L. Allison, CUP

Linux
 Ubuntu
free op. sys.
OpenOffice
free office suite
The GIMP
~ free photoshop
Firefox
web browser

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

© L. Allison   http://www.allisons.org/ll/   (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 Friday, 29-Mar-2024 11:44:47 AEDT.