**Paste:**#108114**Authors:**1HaskellADay and geophf**Language:**Haskell**Channel:**-**Created:**2014-07-25 14:05:18 UTC**Revisions:**- 2014-07-25 19:39:34 UTC #108151 (diff): No title (1HaskellADay)
- 2014-07-25 17:11:33 UTC #108139 (diff): No title (1HaskellADay)
- 2014-07-25 16:33:45 UTC #108134 (diff): No title (geophf)
- 2014-07-25 14:05:18 UTC #108114: Get me to the Church on thyme (1HaskellADay)

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