Chris Smith wrote: > Pascal Costanza <[EMAIL PROTECTED]> wrote: >>> Clearly, in this example, the program >>> is invoking an operation (division) on values that are not appropriate >>> (zero for the second argument). Hence, if your definition really is a >>> definition, then this must qualify. >> Here, you are asking more from dynamic type systems than any existing >> type system provides. The definition of what is considered to be a type >> error and what not is always part of the specification of a type system. > > No, I'm not. Were we to follow this path of definition, it would not > require that dynamic type systems catch ALL type errors; only that they > catch some. Not that it matters, though. I am analyzing the logical > consequences of your own definition. If those logical consequences were > impossible to fulfill, that would be an even more convincing reason to > find a new definition. Concepts of fairness don't enter into the > equation.
Yes it does. All static type systems define only a strict subset of all possible errors to be covered, and leave others as runtime errors. The same holds for dynamic type systems. >>> If you want to make a statement instead of the sort you've implied >>> above... namely that a type error is *any* error that's raised by a type >>> system, then that's fine. It certainly brings us closer to static >>> types. Now, though, the task is to define a type system without making >>> a circular reference to types. You've already rejected the statement >>> that all runtime errors are type errors, because you specifically reject >>> the division by zero case as a type error for most languages. What is >>> that distinction? >> I don't need such a distinction. I can just define what is covered by a >> type system and what is not. All type systems work that way. > > You've got to define something... or, I suppose, just go on using words > without definitions. You claimed to give a definition, though. > > I have been led by others to believe that the right way to go in the > dynamic type sense is to first define type errors, and then just call > anything that finds type errors a type system. That would work, but it > would require a type error. You seem to want to push that work off of > the word "type error" and back onto "type system", but that requires > that you define what a type system is. I didn't know I was supposed to give a definition. > Incidentally, in the case of static type systems, we define the system > (for example, using the definition given from Pierce many times this > thread), and then infer the definition of types and type errors from > there. Because a solid definition has been given first for a type > system without invoking the concepts of types or type errors, this > avoids being circular. Do you mean this one? "A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute." This isn't really such a strong definition because it shifts the problem of what exactly a type system is to finding a definition for the word "kind". But if this makes you happy, here is an attempt: "A dynamic type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying values according to their kinds." Basically, this correlates with the typical approach of using tags to indicate the type/kind/class of values. And indeed, this is what dynamic type systems typically do: they check tags associated with values. Other kinds of runtime errors are not raised because of such checks, but because of other reasons. Therefore, there is naturally a distinction between runtime errors that are type errors and those that are not. I am not convinced that this definition of mine is a lot clearer than what I have said before, but I am also not convinced that Pierce's definition is any clearer either. It is merely a characterization of what static type systems do. The preciseness comes into play when actually defining a type system: then you have to give definitions what the errors at runtime are that you want to prove absent by way of the static type system, give the typing rules for the type system, and then prove soundness by showing that the typing rules correlate precisely to the runtime errors in the first stage. Since you have to map two different views of the same thing to each other you have to be precise in giving definitions that you can then successfully use in your proofs. In dynamic type system, this level of precision is not necessary because proving that dynamic type errors is what the dynamic type system catches is trivially true, and most programmers don't care that there is a distinction between runtime type errors and runtime "other" errors. But this doesn't mean that this distinction doesn't exist. Pascal -- 3rd European Lisp Workshop July 3 - Nantes, France - co-located with ECOOP 2006 http://lisp-ecoop06.bknr.net/ -- http://mail.python.org/mailman/listinfo/python-list
