6

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.

JimHawkins
  • 4,843
  • 8
  • 35
  • 55
user3391947
  • 63
  • 3
  • A good way to _test_ this is to make a function increments (like `++`) and then create a test harness that passes an initial value (`0`) and the increment function in place of `f`. – Davin Tryon Mar 07 '14 at 09:58
  • As for your `plus` function, you should be thinking about creating a function that _adds_ function applications. (So, think wrap one in the other). – Davin Tryon Mar 07 '14 at 09:59
  • I still don't understand. Do I need to convert sixty (for example) to 60? Is there a built in function for that? – user3391947 Mar 07 '14 at 10:09
  • 1
    No, you don't want to convert. You want to build up church numerals. But, you can test the structure that you have created afterword. – Davin Tryon Mar 07 '14 at 10:33

3 Answers3

9

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

Will Ness
  • 70,110
  • 9
  • 98
  • 181
  • thank you. could you help me with the type definition for the function, I am still struggling to implement it so perhaps that would help me get my head around it – user3391947 Mar 07 '14 at 10:56
  • it's very simple you just ask GHCi about it: `:t let one f x = f x in one` produces `:: (t -> t1) -> t -> t1`. And for `plus` it is `:: (t -> t1 -> t2) -> (t -> t3 -> t1) -> t -> t3 -> t2` We can freely replace the `t_i` with `a,b,c,d,...` for readability. – Will Ness Mar 07 '14 at 11:07
  • what is it that you're struggling to implement? The above definitions just go, as they are, right into your source code file. – Will Ness Mar 07 '14 at 11:11
5

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
chi
  • 111,837
  • 3
  • 133
  • 218
1

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.

hammar
  • 138,522
  • 17
  • 304
  • 385