# Lists

 home  Bib Algorithms Bioinfo FP Logic MML Prog.Lang and the mmlist

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
window on the wide world:
 The Darwin Awards V: Next Evolution

 Linux  Ubuntu free op. sys. OpenOffice free office suite, ver 3.4+ The GIMP ~ free photoshop Firefox web browser FlashBlock like it says!

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 Tuesday, 20-Aug-2019 10:55:58 AEST.