[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"
(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