Marcin 'Qrczak' Kowalczyk <[EMAIL PROTECTED]> wrote: > Chris Smith <[EMAIL PROTECTED]> writes: > >> No what happens if right here you code > >> b := 16; > >> > >> Does that again change the type of "b"? Or is that an illegal > >> instruction, because "b" has the "local type" of (18..22)? > > > > It arranges that the expression "b" after that line (barring further > > changes) has type int{16..16}, which would make the later call to > > signContract illegal. > > The assignment might be performed in a function called there, so it's > not visible locally.
Indeed, I pointed that out a few messages ago. That doesn't mean it's impossible, but it does mean that it's more difficult. Eventually, the compiler will have to stop checking something, somewhere. It certainly doesn't, though, have to stop at the first functional abstraction it comes to. The ways that a function modifies the global application state certainly ought to be considered part of the visible API of that function, and if we could reasonably express that in a type system, then that's great! Granted, designing such a type system for an arbitrary imperative language seems a little scary. > Propagating constraints from conditionals is not applicable to mutable > variables, at least not easily. Certainly it worked in the code from my original response to George. Regardless of whether it might not work in more complex scenarios (and I think it could, though it would be more challenging), it still doesn't seem reasonable to assert that the technique is not applicable. If the type system fails, then it fails conservatively as always, and some programmer annotation and runtime check is needed to enforce the condition. > I think that constant bounds are not very useful at all. Most ranges > are not known statically, e.g. a variable can span the size of an > array. I think you are overestimating the difficulties here. Specialized language already exist that reliably (as in, all the time) move array bounds checking to compile time; that means that there exist at least some languages that have already solved this problem. Going back to my handy copy of Pierce's book again, he claims that range checking is a solved problem in theory, and the only remaining work is in how to integrate it into a program without prohibitive amounts of type annotation. -- Chris Smith - Lead Software Developer / Technical Trainer MindIQ Corporation -- http://mail.python.org/mailman/listinfo/python-list