A design pattern?
Previously we constructored:
Now there are some things. Or, this possibly encourages a way of thinking about some things.
One thing is: We can think that any natural number must necessarily be built from 0 and a series of Ses. (And if we’d like, we can think about the types of things, and argue that 0 : nat and S : nat -> nat.)
Another thing is: A number like this is a function. And that function kind of is the “eliminator function” for that number. An “eliminator function” like this is rather similar to the foldr-function for lists; we can think of it as a function for doing “constructor replacement.”
Like if we have a number built from S (S 0), and we wanna replace the Ses with foos and the 0 with bar, we can apply the number to foo and bar:
So, say we have the numbers 2 and 3...
Reduced to normal form:
And, say we want to add them together. If we want the sum, we can take the number 2 and do the “constructor replacement” thing. The number 2 is built from the 0-constructor and 2 S-contructors: S (S 0). We should be able to get sum by taking that number and, keeping all the Ses, replacing the 0 with 3: S (S 3), which should amount to like 5.
We try. Taking the number 2, we replace S with S, which should let us “keep” all the Ses, and we replace 0 with 3:
We get 5 :)
A bit of abstraction and we will have a +-function.
Or, say we want to multiply 2 by 3.
This time the idea is that we want to replace things so that we turn the number 2, or S (S 0), into + 3 (+ 3 0). We replace the Ses with a function that adds 3 to something, and we replace 0 with 0:
(So, uh. In my experience, thinking about these things in terms of constructors and constructor replacement lets me look away from the “inner workings” of the numbers a little bit, and also make the things feel slightly more like working with datatypes in e.g. an ML dialect. It sometimes makes some things clearer to me. But like, we totally did do addition and multiplication earlier, and it’s not like the functions we did here are very different from those earlier ones. Just a little different.)