Darren New wrote: > Chris Smith wrote: >> Specialized >> language already exist that reliably (as in, all the time) move array >> bounds checking to compile time; > > It sounds like this means the programmer has to code up what it means to > index off an array, yes? Otherwise, I can't imagine how it would work. > > x := read_integer_from_stdin(); > write_to_stdout(myarray[x]); > > What does the programmer have to do to implement this semantic in the > sort of language you're talking about? Surely something somewhere along > the line has to "fail" (for some meaning of failure) at run-time, yes?
You should really take a look at Epigram. One of its main features is that it makes it possible not only to statically /check/ invariants, but also to /establish/ them. In your example, of course the program has to check the integer at runtime. However, in a dependent type system, the type of the value returned from the check-function can very well indicate whether it passed the test (i.e. being a valid index for myarray) or not. Ben -- http://mail.python.org/mailman/listinfo/python-list
