Run Time C++ Dependent Type Experiment

proved_non_zero_optional.cpp

#include <string>
#include <iostream>
#include "optional.hpp"

using nonstd::optional; // this is like Maybe. For more complex examples could use variant (discriminated union)

class proved_non_zero_maybe
{
public:
   static optional<proved_non_zero_maybe> prove(int v)
   {
      if (0 == v)
         return {};
      return proved_non_zero_maybe(v);
   }

   const int val;

private:
   explicit proved_non_zero_maybe(int v) : val(v) {}
};

int safer_div(int x, proved_non_zero_maybe y)
{
   return x / y.val; // look ma, no checks for div by zero
}


int main()
{
   int runtime_y;
   std::cin >> runtime_y;

   auto y = proved_non_zero_maybe::prove(runtime_y); // this is the proof

   if (y) // checking the proof
      std::cout << safer_div(10, y.value()) << std::endl;
   else
      std::cout << "Input was zero!" << std::endl;
}