Curry-Howard silliness

curry_howard_silliness.cpp

#include <functional>
#include <iostream>
#include <string>
#include <tuple>
#include <type_traits>

using namespace std;

// -----------------------------------------------------------------------------
// A silly (in C++) application of the Curry-Howard isomorphism to produce the
// mechanism of a variant type using tuple and de Morgan's laws. See:
// http://milessabin.com/blog/2011/06/09/scala-union-types-curry-howard/

// -----------------------------------------------------------------------------
// negation of a type: a function from that type to nothing

struct nothing
{
  template <typename T> nothing() {}
};

template <typename T>
struct negation
{
  using type = std::function<nothing(T)>;
};

// -----------------------------------------------------------------------------
// variant: A or B = ¬(¬A and ¬B) (de Morgan)

template <typename... Ts>
using variant = negation<std::tuple<negation<Ts>...>>;

// -----------------------------------------------------------------------------
// disjunction (C++17)

template<typename...> struct disjunction : std::false_type {};
template<typename B> struct disjunction<B> : B {};
template<typename B, typename... Bs>
struct disjunction<B, Bs...> : std::conditional_t<B::value,
                                                  B,
                                                  disjunction<Bs...>>  {};

// -----------------------------------------------------------------------------
// implication rules

// T => T

template <typename T, typename U>
struct implies : public std::is_same<T, U> {};

// ¬T => ¬U <=> U => T

template <typename T, typename U>
struct implies<negation<T>, negation<U>> : public implies<U, T> {};

// T and X => T

template <typename T, typename... Ts>
struct implies<std::tuple<Ts...>, T> : public disjunction<implies<Ts, T>...> {};

// -----------------------------------------------------------------------------
// helper

template <typename T, typename U, typename... Us>
using is_one_of_t = enable_if_t<implies<negation<negation<T>>,
                                        variant<U, Us...>>::value>;

// -----------------------------------------------------------------------------
// test

void process(int i)
{
  cout << "Process int: " << i << endl;
}

void process(const string& s)
{
  cout << "Process string: " << s << endl;
}

template <typename T,
          typename = is_one_of_t<T, int, string>>
void processSomething(const T& t)
{
  process(t);
}

int main()
{
  int x{42};
  processSomething(x);

  string s{"Hello, world!"};
  processSomething(s);

  // double d{3.14};
  // processSomething(d);
}