Monadic semantics C++17

Bind.v

Set Implicit Arguments.

Inductive proc: Type -> Type :=
| ret: forall T, T -> proc T
| bind: forall T T', proc T -> (T -> proc T') -> proc T'
| print: nat -> proc unit.



Fixpoint f(a: nat) :=
  match a with
    | 0 => ret tt
    | S n => bind (print a) (fun _ => f n)
  end.

Compute f 10.

highorder.cpp

#include <iostream>
#include "type_deduction.hpp"
#include <functional>

using namespace std;

// Attempt at inductive monad definition
template<typename T>
struct Proc   { virtual ~Proc<T>() {} };

template<typename T>
struct Ret   : Proc<T> {
    Ret(T t) : n(t){}
    T n;
};

template<typename T1, typename T2>
struct Bind  : Proc<T2> {
    Bind(Proc<T1> a, std::function<Proc<T2>(T1)> &cb): in(a), f(cb) {}
    Proc<T1> &in;
    std::function<Proc<T2>(T1)> &f;
};

struct Print : Proc<int> {
    Print(int m): n(m){}
    int n;
    // Here's how I do the linking with stdc++, super easy!
    const void operator()() {
        std::cout << this->n << std::endl;
    }
};

// Pin types to <int, char>
// Inductive step f<a>
template<int a>
struct f {
    static const Bind<int, char> value;
};
template<int a>
inline std::function<Proc<char>(int)> lambda = [](auto _) {
    return f<a-1>::value;
};
template<int a>
const Bind<int, char> f<a>::value = Bind(Print(a), lambda<a>);

// Base case f<0>
template <>
struct f<0> {
    static const Ret<char> value;
};
const auto f<0>::value = Ret<char>('a');

int main() {
  auto foo = f<10>();
  std::cout << type_name<decltype(foo)>() << '\n';
  return 0;
}

type_deduction.hpp

#include <type_traits>
#include <typeinfo>
#ifndef _MSC_VER
#   include <cxxabi.h>
#endif
#include <memory>
#include <string>
#include <cstdlib>

template <class T>
std::string
type_name()
{
    typedef typename std::remove_reference<T>::type TR;
    std::unique_ptr<char, void(*)(void*)> own
           (
#ifndef _MSC_VER
                abi::__cxa_demangle(typeid(TR).name(), nullptr,
                                           nullptr, nullptr),
#else
                nullptr,
#endif
                std::free
           );
    std::string r = own != nullptr ? own.get() : typeid(TR).name();
    if (std::is_const<TR>::value)
        r += " const";
    if (std::is_volatile<TR>::value)
        r += " volatile";
    if (std::is_lvalue_reference<T>::value)
        r += "&";
    else if (std::is_rvalue_reference<T>::value)
        r += "&&";
    return r;
}

Use clang++ -std=c++17 -o highorder highorder.cpp to compile.
Use clang++ -std=c++17 -Xclang -ast-dump -fsyntax-only highorder.cpp to dump the AST and verify template unrolling.