Created
August 16, 2018 01:43
-
-
Save vladris/2dc4f5a47d003da002a70f0c0184b0a3 to your computer and use it in GitHub Desktop.
Peano arithmetic in C++ type system
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include <type_traits> | |
// Natural numbers | |
struct nat { }; | |
// Typed only if T is derived from nat | |
template <typename T> | |
using nat_only = std::enable_if_t<std::is_base_of<nat, T>::value>; | |
// Zero is a natural number | |
struct zero : nat { }; | |
// So is the successor of a natural number | |
template <typename T, typename = nat_only<T>> | |
struct succ : nat { }; | |
// A few numbers... | |
using one = succ<zero>; | |
using two = succ<one>; | |
using three = succ<two>; | |
using four = succ<three>; | |
using five = succ<four>; | |
// Conversion to int | |
template <typename T> | |
struct to_int { }; | |
template <> | |
struct to_int<zero> { static constexpr int value = 0; }; | |
template <typename Pred> | |
struct to_int<succ<Pred>> { static constexpr int value = 1 + to_int<Pred>::value; }; | |
// Addition | |
template <typename X, typename Y, typename = nat_only<Y>> | |
struct add { }; | |
template <typename Y> | |
struct add<zero, Y> { using type = Y; }; | |
template <typename Pred, typename Y> | |
struct add<succ<Pred>, Y> { using type = typename add<Pred, succ<Y>>::type; }; | |
// Assertions | |
static_assert(0 == to_int<zero>::value, "0 == zero"); | |
static_assert(3 == to_int<three>::value, "3 == three"); | |
static_assert(std::is_same_v<add<two, three>::type, five>, "2 + 3 == 5"); | |
static_assert(std::is_same_v<add<one, four>::type, add<three, two>::type>, "1 + 4 == 3 + 2"); |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment