BONUS! But not as easy as λa, λb, λc ...

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
{-# LANGUAGE Rank2Types #-}

module Control.Church where

import Prelude hiding (succ, and, or)

{--

Semantics of nx in the language HA! ... it can be something other than Peano.

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, and plus m n is m f applications FOLLOWED BY n f applications
to x. So extending HA! with the type Church, Use the Church numerals of --}

zero :: Church t1
zero = undefined

one :: Church t1
one = undefined

{-- (well, define those numerals, anyway). With the above numerals, define
plus, from plus, define succ, then mult and pow.

... The function pow, if you're familiar with exponentiation-as-
function-application, is really, really simple using Church numerals. --}

plus :: Church t1 -> Church t1 -> Church t1
plus n1 n2 = undefined

succ :: Church t1 -> Church t1
succ n1 = undefined

-- 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

-- ... etc.

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

mult :: Church t1 -> Church t1 -> Church t1
mult n1 n2 = undefined

-- 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 = undefined

{--

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

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

Now, booleans are also really simple using Church representations:

True is that when given two values, the first is returned
False is that when given two values, the second is returned

So, we extend HA!-language once more with the type ChurchBool
defined in the meta-langauge and the predicate values px and qx 
for [x = 0, 1, 2, ...]

 --}

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

true :: ChurchBool t1
true = undefined

false :: ChurchBool t1
false = undefined

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

and :: ChurchBool t1 -> ChurchBool t1 -> ChurchBool t1
and p0 q0 = undefined

or :: ChurchBool t1 -> ChurchBool t1 -> ChurchBool t1
or p0 q0 = undefined

-- for both the Church numerals and Church booleans you can use the 
-- meta-language to help you with verifying your definitions.