Representing Integers as Functions (Church Numerals?)
Apply equational reasoning1, and abstraction. You have
one f x = f x -- :: (a -> b) -> a -> b
two f x = f (f x) -- = f (one f x) -- :: (a -> a) -> a -> a
three f x = f (f (f x)) -- = f (two f x) -- :: (a -> a) -> a -> a
-- ~~~~~~~~~~~
Thus, a successor function next
is naturally defined, so that three = next two
. Yes, it is as simple as writing next two
instead of three
in the equation above:
next :: ((b -> c) -> a -> b) -> (b -> c) -> a -> c
-- three f x = next two f x = f (two f x) -- `two` is a formal parameter
-- ~~~~~~~~~~~
next num f x = f (num f x) -- generic name `num`
zero :: t -> a -> a
zero f x = x
This captures the pattern of succession. f
will be used as a successor function, and x
as zero value. The rest follows. For instance,
plus :: (t -> b -> c) -> (t -> a -> b) -> t -> a -> c
plus two one f x = two f (one f x) -- formal parameters two, one
-- = f (f (one f x)) -- an example substitution
-- = f (f (f x) -- uses the global definitions
-- = three f x -- for one, two, three
i.e. one f x
will be used as a zero value by two
(instead of the "usual" x
), thus representing three
. A "number" n
represents a succession of n +1
operations.
The above, again, actually defines the general plus
operation because two
and one
are just two formal function parameters:
Prelude> plus three two succ 0 -- built-in `succ :: Enum a => a -> a`
5
Prelude> :t plus three two
plus three two :: (a -> a) -> a -> a
Prelude> plus three two (1:) [0]
[1,1,1,1,1,0]
The key thing to gasp here is that a function is an object that will produce a value, when called. In itself it's an opaque object. The "observer" arguments that we apply to it, supply the "meaning" for what it means to be zero, or to find a successor, and thus define what result is produced when we make an observation of a number's value.
1i.e. replace freely in any expression the LHS with the RHS of a definition, or the RHS with the LHS, as you see fit (up to the variables renaming of course, to not capture/shadow the existing free variables).
To convert a number to a numeral you can use something like:
type Numeral = forall a . (a -> a) -> (a -> a)
toChurch :: Int -> Numeral
toChurch 0 _ x = x
toChurch n f x = f $ toChurch (pred n) f x
fromChurch :: Numeral -> Int
fromChurch numeral = numeral succ 0