[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Generalizing Types as Provable Invariants
- To: Pixel <address@hidden>
- Subject: Re: Generalizing Types as Provable Invariants
- From: "David B. Tucker" <address@hidden>
- Date: Sat, 8 Jun 2002 21:36:24 -0400
- Cc: address@hidden
- In-reply-to: <200206081526.LAA11945@bosch.cs.brown.edu>; from sk@cs.brown.edu on Sat, Jun 08, 2002 at 11:26:57AM -0400
- References: <200206081526.LAA11945@bosch.cs.brown.edu>
- Sender: address@hidden
- User-agent: Mutt/1.2.5i
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
>