[C++] [Haskell] Simply Typed Lambda Calculus Church Intenger : Function Application (T -> T)

Despite simply typed lambda calculus is total(and it means that is not Turing complete why it's strongly normalizing and ever halts) can represent data(church encoding). Simply typed lambda calculus is not Turing completeness, but expressive.

We let's consider this:

n x f = f x
k f x a = f (a x) a

Where let d = k(k (k (n))) (0) (\x -> x+1), IO::print(d) will print d evalued as 4. Then...k will count until n function.

For the implementation with typed lambda calculus without Hindley Milner Inference let's go consider this type notation for that:

nn : T -> (T -> T) -> T
n : (T -> (T -> T) -> T) -> T -> (T -> T) -> T

Finnaly let's go represent this in a simply lambda typed language like c++ :) :

template <typename T>
//nn : T -> (T -> T) -> T
std::function<std::function<T(std::function<T(T)>)>(T)> nn = [=](auto x){return ([=](auto f) {return f(x);});};

template <typename T>
//n : (T -> (T -> T) -> T) -> T -> (T -> T) -> T
std::function<std::function<std::function<T(std::function<T(T)>)>(T)>(std::function<std::function<T(std::function<T(T)>)>(T)>)> n = [=](auto f){return ([=](auto x){return ([=](auto a) {return f(a(x))(a);});});};

So...

printf("%d", nn<int>(nn<int>(nn<int>(n<int>)))(0)([=](int d){return d + 1;}));

surely will prints 4.

caotic123/typedlambda.md