Natural Number
We can use the datatype keyword to define new datatypes.
We take natural number as the first datatype example.
After the definition, Nat is a Type.
And we can use Nat's constructors to construct Nat.
We define some common natural numbers, and use them to write tests in the following code.
We can use the recursion keyword to define functions that operates over Nat.
add is one of the most basic function, it adds two Nats togather.
We did not recursively call add(prev), but use almost.prev to get the result of the recursive call,
i.e. almost.prev is the same as add(prev).
i.e. recursive is like pattern matching, but an extra argument called almost is given to the caller, in which we can get the results of recursive calls.
We often add a _ prefix for a name taken from pattern matching, but not used in the following code.
_prev is a example of this situation.
Applying a function that takes two arguments to only one argument, will return another function that takes one argument.
We often use same_as_chart to write test.
By using recursion, we are defining function using recursive combinator.
If we view recursion over Nat as a function, it roughly has the following definition.
The induction keyword is like recursion, but the return type can depend on the target, we use a function to specify the return type, and we call this function motive.
If we view induction over Nat as a function, it roughly has the following definition.
After understood the definition of add, we naturally want to define mul.
Let write some tests, we use { ...; return ... } to make the name twelve only visible inside the following { ... }.
Next we define power function.
power_of(x, y) means y raised to the power of x.
We swap the argument to get a more natural reading of the function.
power(base, n) means base raised to the power of n.
We define power_of first, because its definition is similar to that of add and mul.
In primary school after the young Gauss misbehaved, his teacher gave him a task: adding the numbers from 1 to 100.
gauss(x) calculates 0 + 1 + 2 + ... + x,
Thanks, Carl Friedrich Gauss (1777 - 1855), you are the prince of mathematics!
factorial(n) calculates n!.
For example, 5! = 5 * 4 * 3 * 2 * 1 = 120.
Let's end this chapter with this famous function.
Actually, before we end this chapter, let's define another very famous function -- the Fibonacci function.
F(0) = 0
F(1) = 1
F(n) = F(n-1) + F(n-2)
| 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 |
|---|
| 0 | 1 | 1 | 2 | 3 | 5 | 8 | 13 | 21 | 34 | 55 |
We use an iterative process for computing the Fibonacci numbers. The idea is to use a pair of integers current and next, initialized F(0) = 1 and F(0) = 0, and to repeatedly apply the simultaneous transformations:
current <- next
next <- current + next
First, we define a helper function -- fibonacci_iter, for the iterative process.
Then we can define the fibonacci using fibonacci_iter.