A demonstration of why the decidable equality operator is useful.

existential_type.cpp

/*
 * Idea: sometimes, you want a pair (a : A, B a), where the first element determines the type of the second element.
 * By the product-exponent adjunction, a map (a : A, B a) -> C is equivalent to a map (a : A) -> B a -> C.
 * Furthermore, if we perform a full double negation translation of our program, we can replace terms of type
 * (a : A, B a) with terms of type forall R. ((a : A, B a) -> R) -> R and thus with terms of type
 * forall R. ((a : A) -> B a -> R) -> R.  These are considerably easier to model in C++ than what we started with.
 *
 * We model a term x of type (a : A) -> B a -> R using a C++-term of a C++-type of the form
 *  struct x_dfun {
 *      template<A a>
 *      R invoke(B<a> b);
 *  };
 *
 * We will be primarily interested in the case A = size_t and B a = std::array<int, a>.
 *
 * We model a term x of type forall R. ((a : A) -> B a -> R) -> R using a C++-term of the form
 *
 *  template<typename R, typename Cont>
 *  R x_with_cont(Cont cont);
 *
 * We now consider the problem of taking two arrays and calculating their dot product if their length is equal, or
 * informing the user that the input is incorrect if they are not.
 */

#include <array>
#include <iostream>

using std::size_t;

template<size_t N>
using IntArray = std::array<int, N>;

template<typename R, typename Cont>
R get_input_with_cont(Cont cont) {
    // Get a vector of the user's choice and invoke the continuation with that.
    std::string response;
    std::cout << "Choose vector A or B: ";
    std::cin >> response;
    if (response == "A") {
        IntArray<2> arr = {1, 1};
        return cont.invoke(arr);
    } else {
#ifdef DEMONSTRATE_ERROR
        IntArray<3> arr = {1, 1, 1};
#else
        IntArray<2> arr = {0, 1};
#endif
        return cont.invoke(arr);
    }
}

template<size_t N>
int dot_product(IntArray<N> const& a, IntArray<N> const& b) {
    int sum = 0;
    for (size_t i = 0; i < N; ++i)
        sum += a[i] * b[i];
    return sum;
}

// (N : size_t) -> IntArray N -> Int
// The outer template parameter stores the context.
// Gets input as parameter and computes dot product.
template<size_t M>
struct step2_dfun {
    IntArray<M> ctx_array;
    template<size_t N>
    int invoke(IntArray<N> array) {
        // The compiler will fail here.  You can try adding an if statement, but it won't resolve the issue.
        // (You can specialise, though, which will work; it's a slightly different solution, though.)
        return dot_product(ctx_array, array);
    }
};

// (N : size_t) -> IntArray N -> Int
// Saves its input in a continuation and then gets a second input.
struct step1_dfun {
    template<size_t N>
    int invoke(IntArray<N> array) {
        step2_dfun<N> cont{array};
        return get_input_with_cont<int>(cont);
    }
};

int main() {
    std::cout << "Result: " << get_input_with_cont<int>(step1_dfun{}) << '\n';
}