Get me to the Church on thyme

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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
{-# LANGUAGE Rank2Types #-}

module Control.Church where

import Prelude hiding (succ, and, or)

{--

A solution to the bonus problem posted at http://lpaste.net/108108

http://lpaste.net/108114

Semantics of nx.

Hm.

Let's think about this. If the Peano-numeral have a Church-numeral semantics
then multiplication and exponentiation is a SNAP! (But addition, without
pattern-matching and destructuring are a BEAR!)

And subtraction ...? Don't even get me started on that.

Just ... don't.

So! BONUS!

We extend our language HA! with the symbol (\) and the semantics of (->) in
definitions, and the type-variable names tx [x = 0, 1, 2, ..] in declarations.

So, given the declaration of the Church numeral in the meta-language: --}

type Church t1 = forall t1. (t1 -> t1) -> t1 -> t1

{--

A Church numeral, n, is applying a function, f, to some value, x, n times.

So, zero is f applied zero times to x, giving just x, one is applied once to
x, giving f x --}

zero :: Church t1
zero = \f0 n0 -> n0 -- const id

one :: Church t1
one = \f0 n0 -> f0 n0 -- id

-- plus m n is m f applications FOLLOWED BY n f applications to x.

plus :: Church t1 -> Church t1 -> Church t1
plus n1 n2 = \f0 n0 -> n1 f0 (n2 f0 n0)

succ :: Church t1 -> Church t1
succ = plus one                 -- that was easy!

-- so, actually, one is superfluous in light of zero and succ, so let's
-- define some other numerals

two, three, four, five, six :: Church t1
two = succ one
three = succ two
four = succ three
five = succ four
six = succ five

-- although, I'm wondering, as Church numerals are unary, should I have
-- used i, ii, iii, iv, v, vi, vii, viii, ix, x? But how to represent
-- zero, then? o?

{-- to express multiplication and exponentiation: --}

-- mult is n1 applications of n2 applications of the function over some value:

mult :: Church t1 -> Church t1 -> Church t1
mult n1 n2 = \f0 n0 -> n1 (n2 f0) n0

-- pow is really, really easy to define with regard to n1 and n2, but the
-- typing in Haskell can trip things up :/ ... edit: solved this with forall.

pow :: Church t1 -> Church t1 -> Church t1
pow n1 n2 = n2 n1 -- oh, yeah!

{--

Demonstrate that mult and pow do (ITRW) what they promise (ITCU)

ITRW: 'in the real world'
ITCU: 'in the church universe'

*Control.Church> one (+ 1) 0
1
*Control.Church> zero (+ 1) 0
0
*Control.Church> succ one (+ 1) 0
2
*Control.Church> succ zero (+ 1) 0
1
*Control.Church> plus one one (+ 1) 0
2
*Control.Church> plus one two (+ 1) 0
3

... we have just proved that 1 + 2 = 3. I'm feeling good!

BUT: 

*Control.Church> plus (succ succ succ one) (succ succ succ succ one) (+ 1) 0
6

WRONG!

BUT:

*Control.Church> plus (succ (succ (succ one))) 
                      (succ (succ (succ (succ one)))) (+ 1) 0
9

RIGHT! (whew!)

So, let's just use our defined Church numerals

*Control.Church> plus two three (+ 1) 0
5

That makes sense.

*Control.Church> mult four five (+ 1) 0
20
*Control.Church> pow three four (+ 1) 0
81

Groovitude!

Now for booleans:

 --}

type ChurchBool t1 = forall t1. t1 -> t1 -> t1

-- True is that when given two values, the first is returned

true :: ChurchBool t1
true = \p1 -> \p2 -> p1 -- const

-- False is that when given two values, the second is returned

false :: ChurchBool t1
false = \p1 -> \p2 -> p2 -- const id

-- with the above, define the 'and' and 'or' functions. Verify their veracity:

and :: ChurchBool t1 -> ChurchBool t1 -> ChurchBool t1
and p q = p q p

or :: ChurchBool t1 -> ChurchBool t1 -> ChurchBool t1
or p q = p p q

{--

So:

*Control.Church> :t and
and :: ChurchBool t1 -> ChurchBool t1 -> t2 -> t2 -> t2
*Control.Church> and true true True False
True
*Control.Church> and false true True False
False
*Control.Church> or true false True False
True
*Control.Church> or false true True False
True
*Control.Church> or false false True False
False

YAY!

 --}
42:1: Error: Redundant lambda
Found:
zero = \ f0 n0 -> n0
Why not:
zero f0 n0 = n0
45:1: Error: Redundant lambda
Found:
one = \ f0 n0 -> f0 n0
Why not:
one f0 n0 = f0 n0
50:1: Error: Redundant lambda
Found:
plus n1 n2 = \ f0 n0 -> n1 f0 (n2 f0 n0)
Why not:
plus n1 n2 f0 n0 = n1 f0 (n2 f0 n0)
74:1: Error: Redundant lambda
Found:
mult n1 n2 = \ f0 n0 -> n1 (n2 f0) n0
Why not:
mult n1 n2 f0 n0 = n1 (n2 f0) n0
142:1: Error: Redundant lambda
Found:
true = \ p1 -> \ p2 -> p1
Why not:
true p1 p2 = p1
142:8: Warning: Collapse lambdas
Found:
\ p1 -> \ p2 -> p1
Why not:
\ p1 p2 -> p1
142:15: Warning: Use const
Found:
\ p2 -> p1
Why not:
(const p1)
147:1: Error: Redundant lambda
Found:
false = \ p1 -> \ p2 -> p2
Why not:
false p1 p2 = p2
147:9: Warning: Collapse lambdas
Found:
\ p1 -> \ p2 -> p2
Why not:
\ p1 p2 -> p2
147:16: Error: Use id
Found:
\ p2 -> p2
Why not:
id
155:1: Error: Eta reduce
Found:
or p q = p p q
Why not:
or p = p p