This post is part of a list: Some lambda-notes
Next thing: A design pattern?
Previous thing: Pairs

We have made some numbers and some functions for working with numbers. Also some other datatypes.

We haven’t really done so here, but sometimes when we define numbers we fuss more about how they are constructed, about what the constructors are. We say things like: “A natural number is zero or it is the successor of a natural number.” (In a Standard ML we might say: datatype nat = Zero | Succ of nat.)

So let’s try to? With the lambdas and such...

We already know what zero looks like:

0 ≜ λf.λx.x

We do not know that successor looks like:

S ≜ λn.λf.λx.f (n f x)

It takes a number, n, as its argument. S applied to n should return a number that is one larger than n.

(Remember: The number n is a function that, if given two arguments, applies the first argument n times to the second.)

So, S takes a number, n, as its argument, and returns one of those λf.λx.-functions. Within, we do (n f x); we apply n to f and x. This should amount to applying fn times” to x. And then we apply f to the result of (n f x), so that we should, in total, get f applied, well, “n+1 times” to x.

We can test it some and see if it looks right:

S 0 S (S 0) S (S (S 0)) S (S (S (S (S 0))))

And like, that’s it, that’s our successor. It seems maybe less impressive than the addition and multiplication functions we did earlier. But like it’s pretty cool:

Will take a look at that last ting. But like, in later post...