Re: Generalizing Types as Provable Invariants

[Pixel <address@hidden>]

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

> Pixel wrote:
> 
> > [lots of template C++ code]
> 
> I don't see the dependent types in your code.  I see lots of macro
> (template) expansion and macro-time constants and arithmetic, but
> those aren't dependent types.

what is Array<int, 2> ? it is a type indexed by term [*]. which is the
definition of dependent type in "Types and Programming Languages"
(B.Pierce)

> If you care to make this point, perhaps you also care to do it less
> opaquely (and more concisely)?

As for me, i always prefer somewhat useful examples.
Here is the most concise version i can think of:

template<int size> class Int_array {
  // ...
};
main() {
    Int_array<2> a;
}


[*] well, in fact here it's indexed on both type and term