[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Generalizing Types as Provable Invariants

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"

> 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