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

Re: Generalizing Types as Provable Invariants



The 2 in your type Int_array<2> isn't really a "term", but rather what
C++ calls an "integral constant expression" (ICE); essentially, any
integral value it can compute statically.  So it's not truly a
dependent type.

Furthermore, you can't use these ICEs to statically require that all
array accesses are within bounds.  There are type systems that can do
this -- see Hongwei Xi's work which uses a restricted form of
dependent types.

Dave

> > 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
>