Representing Integers as Functions (Church Numerals?)

Question

Given the following function definition and assuming similar definitions for all positive integers give the type definition and code for a function called plus that will take as arguments two such functions representing integers and return a function that represents the sum of the two input integers. E.g. (plus one two) should evaluate to a function that takes two arguments f x and returns (f(f(f x))).

one f x = f x
two f x = f (f x)
three f x = f (f (f x)))

etc.

I am new to functional programming and I can't get my head around this. I firstly don't know how I can define the functions for all the positive integers without writing them out (which is obviously impossible). As in, if I have plus(sixty, forty), how can my function recognize that sixty is f applied 60 times to x?

I am meant to be writing this in Miranda, but I am more familiar with Haskell, so help for either is welcome.

Answer 1

Apply equational reasoning¹, 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.

¹i.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).

Answer 2

You don't need to recognize how many times the function is calling f. For example, to implement succ, which adds 1 to a Church numeral, you can do something like this:

succ n f x = f (n f x)

Then you first use n to apply f however many times it needs to, and then you do the final f yourself. You could also do it the other way round, and first apply f once yourself and then let n do the rest.

succ n f x = n f (f x)

You can use a similar technique to implement plus.

Answer 3

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