-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathChapter8.lhs
More file actions
117 lines (71 loc) · 2.29 KB
/
Copy pathChapter8.lhs
File metadata and controls
117 lines (71 loc) · 2.29 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
Haskell: The Craft of Functional Programming
Simon Thompson
(c) Addison-Wesley, 1999.
Chapter 8
Reasoning about programs
^^^^^^^^^^^^^^^^^^^^^^^^
> module Chapter8 where
> import Prelude hiding (sum,length,(++),reverse,unzip)
Testing and verification
^^^^^^^^^^^^^^^^^^^^^^^^
A function supposed to give the maximum of three (integer) values.
> mysteryMax :: Int -> Int -> Int -> Int
> mysteryMax x y z
> | x > y && x > z = x
> | y > x && y > z = y
> | otherwise = z
Definedness and termination
^^^^^^^^^^^^^^^^^^^^^^^^^^^
A factorial function, giving an undefined result on negative integers.
> fact :: Int -> Int
> fact n
> | n==0 = 1
> | otherwise = n * fact (n-1)
An infinite list
> posInts :: [Int]
> posInts = [1, 2 .. ]
Induction
^^^^^^^^^
The sum function, defined recursively.
> sum :: [Int] -> Int
> sum [] = 0 -- (sum.1)
> sum (x:xs) = x + sum xs -- (sum.2)
Double every element of an integer list.
> doubleAll :: [Int] -> [Int]
> doubleAll [] = [] -- (doubleAll.1)
> doubleAll (z:zs) = 2*z : doubleAll zs -- (doubleAll.2)
The property linking the two:
sum (doubleAll xs) = 2 * sum xs -- (sum+dblAll)
Other functions used in the examples
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
The definitions given here use explicit recursion, rather than applying
higher-order functions as may happen in the Prelude definitions.
> length :: [a] -> Int
> length [] = 0 -- (length.1)
> length (z:zs) = 1 + length zs -- (length.2)
> (++) :: [a] -> [a] -> [a]
> [] ++ zs = zs -- (++.1)
> (w:ws) ++ zs = w:(ws++zs) -- (++.2)
> reverse :: [a] -> [a]
> reverse [] = [] -- (reverse.1)
> reverse (z:zs) = reverse zs ++ [z] -- (reverse.2)
> unzip :: [(a,b)] -> ([a],[b])
> unzip [] = ([],[])
> unzip ((x,y):ps)
> = (x:xs,y:ys)
> where
> (xs,ys) = unzip ps
Generalizing the proof goal
^^^^^^^^^^^^^^^^^^^^^^^^^^^
The shunting function
> shunt :: [a] -> [a] -> [a]
> shunt [] ys = ys -- (shunt.1)
> shunt (x:xs) ys = shunt xs (x:ys) -- (shunt.2)
> rev :: [a] -> [a]
> rev xs = shunt xs [] -- (rev.1)
An alternative definition of the factorial function.
> fac2 :: Int -> Int
> fac2 n = facAux n 1
> facAux :: Int -> Int -> Int
> facAux 0 p = p
> facAux n p = facAux (n-1) (n*p)