**1**

### Fundamentals

#### Function on Types

We all know that C++ templates can receive types as “parameters”. In the same spirit we could can “return values”s, so that we can form a function. The basic paradigm is the following:

template<class T> struct Computed { using type = T; }

In this way we constructed a type level function named `Computed`

, with one parameter and result the parameter itself. We use the function as `Computed<float>::type`

, the result being `float`

itself.

Why an extra `struct`

wrapper instead of directly defining the “function”? That’s because partialization on `using`

is not allowed. Such codes are invalid:

template <class T> using computed<T> = T; template<> using computed<int> = double;

#### Partialization

template<class T> struct Computed { using type = T; } template<> struct Computed<int> { using type = double; }

`Computed<bool>::type`

would become `bool`

, while `Computed<int>::type`

would (specially) be `double`

. Certainly, there are a set of rules for the matching process. E.g. the most “specific” case gets matched first. This is somewhat from Haskell, where the first-defined case comes first. The equivalent code in Haskell is:data Type = Bool | Double | Int computed :: Type -> Type computed Int = Double computed t = t

### Peano numbers

`Zero`

for `0`

, and a `Succ`

for the successive. Thus `1`

would be `Succ<Zero>`

, `2`

would be `Succ<Succ<Zero>>`

, and so on. This is but the heuristic demonstration of “induction”.struct Peano {}; struct Zero: Peano {}; template<class T> struct Succ: Peano {};

template<class T1, class T2> struct Add { using type = ???; }

`2+1=3`

, or `Add<Succ<Succ<Zero>>, Succ<Zero>>::type = Succ<Succ<Succ<Zero>>>`

. Certainly the latter expression is not valid C++, since there is no equality operator for types. Instead, we should use the `std::is_same<T1, T2>`

function, which is predefined in `<type_traits>`

. Or you can implement it yourself, again using partialization. This is a possible implementation:template<class T, class U> struct is_same { static constexpr bool value = false; }; template<class T> struct is_same<T, T> { static constexpr bool value = true; };

template<> struct Add<Succ<Succ<Zero>>, Succ<Zero>> { using type = Succ<Succ<Succ<Zero>>>; }

`0 + b = b, (Succ a) + b = Succ (a + b)`

. In C++ they are:template<class T1, class T2> struct Add; template<class T> struct Add<Zero, T> { using type = T; }; template<class T1, class T2> struct Add<Succ<T1>, T2> { using type = Succ<typename Add<T1, T2>::type> };

`typename`

— the compiler doesn’t know whether the `::type`

is a member type or a member variable, so we need this keyword as a hint.`std::is_same<Add<Succ<Succ<Zero>>, Succ<Zero>>::type, Succ<Succ<Succ<Zero>>>>::value == true`

or so. Such nesting of `Succ`

is somewhat hard to read, so you can simply write a template to generate Peano types from integers:template<int v> struct peano { using type = Succ<typename peano<v - 1>::type>; }; template<> struct peano<0> { using type = Zero; };

Then you can simplify it to `Add<peano<2>::type, peano<1>::type>::type`

and `peano<3>::type`

. The other opeartions like subtraction, multiplication and division can be similarly implemented, which are left as exercises.

### Exercises:

### Afterwords

We can further “prove” the assertions in our intuition, such addition is commutative, multiplication is distributive over addition, and so on. We may talk about this later.

**1**

huge 數學歸納需要專門去學習麼

我觉得最好去学一学实分析开头定义自然数的部分，自然就懂了。

这个配色看着很费眼睛诶，背景和字体的颜色反差太大了。