Implementing the Natural Numbers in the Type System using C Templates-CodePudding

I have this struct template

template<typename N>
struct Succ{};

and this function template

template<typename N> N dec(Succ<N> s_n){
    N n;
    return n;
}

and this does exactly what I want, if I decrement once too often, I get a compiler error.

Now, I would like to use this style of code in my projects for catching errors, however it is very tedious to create initial "values", I mean, 2 is already Succ<Succ<SomeType>>.

How can I accomplish this with C templates? Something like

Nat<2,SomeType> two;

which is the same as

Succ<Succ<SomeType>> two;

And can some people give me links or other resources to this kind of template programming please? Like, how to implement Peano Arithmetic with C templates and how to create Type Numbers more easily.

CodePudding user response：

Something like this

template<typename N>
struct Succ{};

template<int N, typename T>
struct NatImpl
{
    using type = Succ<typename NatImpl<N-1, T>::type>;
};

template<typename T>
struct NatImpl<0, T>
{
    using type = T;
};

template<int N, typename T>
using Nat = typename NatImpl<N, T>::type;

Templated using is a thing, but you can't specialise them, so that is done in the NatImpl class.

And the proof

int main()
{
    Nat<3,int> x = Succ<Succ<int>>();
}

error C2440: 'initializing': cannot convert from 'Succ<Succ<int>>' to 'Succ<Succ<Succ<int>>>'

CodePudding user response：

You can create a alias template taking the number, a template and the type as template parameters and implement it via a helper template:

template<size_t N, template<class> class T, class U>
struct NatHelper
{
    using Type = T<typename NatHelper<N - 1, T, U>::Type>;
};

template<template<class> class T, class U>
struct NatHelper<0, T, U>
{
    using Type = U;
};

template<size_t N, template<class> class T, class U>
using Nat = typename NatHelper<N, T, U>::Type;

struct SomeType
{};

template<typename N>
struct Succ {};

using N0 = Nat<0, Succ, SomeType>;
static_assert(std::is_same_v<N0, SomeType>);

using N2 = Nat<2, Succ, SomeType>;
static_assert(std::is_same_v<N2, Succ<Succ<SomeType>>>);

using N10 = Nat<10, Succ, SomeType>;
static_assert(std::is_same_v<N10, Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<SomeType>>>>>>>>>>>);

CodePudding user response：

A C 17 version using constexpr if could look like this:

template <size_t N, class SomeType>
auto NatHelper() {
    if constexpr (N > 1) return Succ<decltype(NatHelper<N - 1, SomeType>())>{};
    else return Succ<SomeType>{};
}

template<size_t N, class SomeType>
using Nat = decltype(NatHelper<N, SomeType>());

Demo