Re: Generalizing Types as Provable Invariants

[Pixel <address@hidden>]

Shriram Krishnamurthi <sk@cs.brown.edu> writes:

> Pixel wrote:
> 
> > > > - dependent types (cf recent thread on comp.lang.functional)
> > 
> > i meant to add that C++ has a form of dependent types
> 
> Care to elaborate?

sure :)

/*********************************************************************************/
#include <iostream>

template<class T, int size> class Array {
private:
  T v[size];
public:

  const T &operator[] (unsigned int pos) const {
    if (pos < size) return v[pos]; else throw "out of bound";
  }
  T &operator[] (unsigned int pos) {
    if (pos < size) return v[pos]; else throw "out of bound";
  }
};

// a little sugar for a few sizes:
template<class T> Array<T, 2> new_array(const T &a0, const T &a1) { 
  Array<T, 2> r; r[0] = a0; r[1] = a1; return r;
}
template<class T> Array<T, 3> new_array(const T &a0, const T &a1, const T &a2) { 
  Array<T, 3> r; r[0] = a0; r[1] = a1; r[2] = a2; return r;
}

template<class T, int size> std::ostream& operator<<(std::ostream& os, const Array<T, size> &a) {
  os << "[";
  if (size) os << a[0];
  for (int i = 1; i < size; i++) os << ", " << a[i];
  os << "]";
  return os;
}

template<class T, int size1, int size2> Array<T, size1+size2> operator+(const Array<T, size1> &a1, const Array<T, size2> &a2) {
  Array<T, size1+size2> r;
  for (int i = 0; i < size1; i++) r[i] = a1[i];
  for (int i = 0; i < size2; i++) r[i + size1] = a2[i];
  return r;
}

template<class T, int size> Array<T, size> scalar_product(const Array<T, size> &a1, const Array<T, size> &a2) {
  Array<T, size> r;
  for (int i = 0; i < size; i++) r[i] = a1[i] * a2[i];
  return r;
}


int main() {
  Array<int, 2> a = new_array<int>(0, 1);
  Array<int, 3> b = new_array<int>(2, 3, 4);

  std::cout << a << b << a + b << std::endl;

  std::cout 
    << scalar_product(a,a) 
    << scalar_product(b,b) 
    << scalar_product(a+b, b+a)
    // << scalar_product(a, b) // doesn't compile
    // << scalar_product(b, a) // doesn't compile
    << std::endl;

}
/*********************************************************************************/