Chris Uppal <[EMAIL PROTECTED]> wrote: > > if (x != 0) y = 1 / x; > > else y = 999999999; > > > > is not all that much different from: > > > > try { y = 1 / x; } > > catch (ArithmeticException e) { y = 999999999; }
> My immediate thought is that the same question is equally applicable (and > equally interesting -- i.e. no simple answer ;-) for static typing. I don't see that. Perhaps I'm missing something. If I were to define a type system for such a language that is vaguely Java-based but has NotZero as a type, it would basically implement your option [D], and contain the following rules: 1. NotZero is a subtype of Number 2. Zero is a subtype of Number 3. If x : Number and k : Zero, then "if (x != k) a else b" is well-typed iff "a" is well-typed when the type-environment is augmented with the proposition "x : NotZero" and "b" is well-typed when the type- environment is augmented with the new proposition "x : Zero". Yes, I know that Java doesn't do this right now in similar places (e.g., instanceof), and I don't know why not. This kind of thing isn't even theoretically interesting at all, except that it makes the proof of type-soundness look different. As far as I can see, it ought to be second-nature in developing a type system for a language. In that case, the first example is well-typed, and also runs as expected. The second bit of code is not well-typed, and thus constitutes a type error. The way we recognize it as a type error, though, is in the fact that the compiler aborts while checking the typing relation, rather than because of the kind of problem prevented. Of course, it would be possible to build a static type system in which different things are true. For example, Java itself is a system in which both terms are well-typed. >From a dynamic type perspective, the litany of possibilities doesn't really do much for defining a dynamic type system, which I thought was our goal in this bit of the thread. I may not have been clear enough that I was look for an a priori grounds to classify these two cases by the definition. I was assuming the existing behavior of Java, which says that both accomplish the same thing and react in the same way, yet intuitively we seem to think of one as a type error being "solved", whereas the other is not. Anyway, you just wrote another message that is far closer to what I feel we ought to be thinking about than my question here... so I will get to reading that one, and perhaps we can take up this point later when and if it is appropriate. -- Chris Smith - Lead Software Developer / Technical Trainer MindIQ Corporation -- http://mail.python.org/mailman/listinfo/python-list