Excuse me, miss, where we put this Grande Peano? (heh)

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
118
119
120
121
import Prelude hiding (max, min, subtract, or, not)

{--

A solution to the Peano HA! exercise at http://lpaste.net/108099

Logic.

The HA!-instruction set.

Given the symbols:

S Z ( ) = :: -> fx nx (for x = 0, 1, 2 ...)

Remember no 'where' is to show nowhere in the code. 

Geddit? 'no-where' 'nowhere'?

GEDDIT?

 --}

data Peano = Z | S Peano

max :: Peano -> Peano -> Peano
max n1 n2 = max' n1 n2 Z

max' :: Peano -> Peano -> Peano -> Peano
max' Z n2 n3 = add n2 n3
max' n1 Z n3 = add n1 n3
max' (S n1) (S n2) n3 = max' n1 n2 (S n3)

min :: Peano -> Peano -> Peano
min n1 n2 = minFrom n1 n2 Z

minFrom :: Peano -> Peano -> Peano -> Peano
minFrom Z n2 n3 = n3
minFrom n1 Z n3 = n3
minFrom (S n1) (S n2) n3 = minFrom n1 n2 (S n3)

add :: Peano -> Peano -> Peano
add Z n2 = n2
add n1 Z = n1
add (S n1) n2 = add n1 (S n2)

subtract :: Peano -> Peano -> Peano
subtract Z n2 = Z  -- lower-bound
subtract n1 Z = n1
subtract (S n1) (S n2) = subtract n1 n2

-- ... for subtract, please note the Peano-semantics of the lower-bound
-- of the series: pred Z = Z (also please note that 'pred' is not a predefined
-- function in HA!)

mult :: Peano -> Peano -> Peano
mult Z n2 = Z
mult n1 Z = Z
mult n1 n2 = mult' n1 n2 Z

mult' :: Peano -> Peano -> Peano -> Peano
mult' Z n2 n3 = n3
mult' (S n1) n2 n3 = mult' n1 n2 (add n3 n2)

pow :: Peano -> Peano -> Peano
pow Z n2 = Z
pow n1 Z = S Z
pow n1 n2 = pow' n1 n2 (S Z)

pow' :: Peano -> Peano -> Peano -> Peano
pow' n1 Z n3 = n3
pow' n1 (S n2) n3 = pow' n1 n2 (mult n1 n3)

fact :: Peano -> Peano
fact Z = S Z
fact (S n) = mult (S n) (fact n)

-- the compact visual representation of Peano-numbers:

instance Show Peano where
   show p = "P" ++ show (intOf p)

intOf Z = 0
intOf (S n) = 1 + intOf n

data Boolean {- as in George -} = Sure | Whatevs -- 'Whatevs' always means 'No'
  deriving (Eq, Show, Read)                      -- have you noticed that?
                                                 -- a passive-aggressive 'No'

eq :: Peano -> Peano -> Boolean
eq Z Z = Sure
eq Z (S n2) = Whatevs
eq (S n1) Z = Whatevs
eq (S n1) (S n2) = eq n1 n2

lt :: Peano -> Peano -> Boolean
lt n1 Z = Whatevs
lt Z (S n) = Sure
lt (S n1) (S n2) = lt n1 n2

-- Now, define the rest wrt lt and eq

or :: Boolean -> Boolean -> Boolean
or Sure _ = Sure
or _ Sure = Sure
or _ _    = Whatevs

le :: Peano -> Peano -> Boolean
le n1 n2 = or (lt n1 n2) (eq n1 n2)

not :: Boolean -> Boolean
not Sure = Whatevs
not Whatevs = Sure

gt :: Peano -> Peano -> Boolean
gt n1 n2 = not (le n1 n2)

ge :: Peano -> Peano -> Boolean
ge n1 n2 = not (lt n1 n2)

-- I ran a bunch of tests against these functions but ... you get it, right?
-- have a great weekend!
80:13: Warning: Use :
Found:
"P" ++ show (intOf p)
Why not:
'P' : show (intOf p)