Chris F Clark wrote: > A static > type system eliminates some set of tags on values by syntactic > analysis of annotations (types) written with or as part of the program > and detects some of the disallowed compuatations (staticly) at compile > time.
Adreas relied: > Explicit annotations are not a necessary ingredient of a type system, > nor is "eliminating tags" very relevant to its function. While this is true, I disagree at some level with the second part. By eliminating tags, I mean allowing one to perform "type safe" computations without requiring the values to be tagged. One could argue that the tags were never there. However, many of the interesting polymorphic computations reaquire either that the values be tagged or that some other process assures that at each point one can determine apriori what the correct variant of computation is which applies. To me a static type system is one which does this apriori determination. A dynamic type system does not do a apriori and instead includes explicit information in the values being computed to select the corret variant computations. In that sense, a static type system is eliminating tags, because the information is pre-computed and not explicitly stored as a part of the computation. Now, you may not view the tag as being there, but in my mind if there exists a way of perfoming the computation that requires tags, the tag was there and that tag has been eliminated. To put it another way, I consider the tags to be axiomatic. Most computations involve some decision logic that is driven by distinct values that have previously been computed. The separation of the values which drive the compuation one-way versus another is a tag. That tag can potentially be eliminated by some apriori computation. In what I do, it is very valuable to move information from being explicitly represented in the computed result into the tag, so that I often have distinct "types" (i.e. tags) for an empty list, a list with one element, a list with two elements, and a longer list. In that sense, I agree with Chris Smith's assertion that "static typing" is about asserting general properties of the algorithm/data. These assertions are important to the way I am manipulating the data. They are part of my type model, but they may not be part of anyone else's, and to me toe pass a empty list to a function requiring a list with two elements is a "type error", because it is something I expect the type system to detect as incorrect. The fact that no one else may have that expectation does not seem relevant to me. Now, to carry this farther, since I expect the type system to validate that certain values are of certain types and only be used in certain contexts, I am happy when it does not require certain "tags" to be actualy present in the data. However, because other bits of code are polymorphic, I do expect certain values to require tags. In the end, this is still a win for me. I had certain data elements that in the abstract had to be represented explicitly. I have encoded that information into the type system and in some cases the type system is not using any bits in the computed representation to hold that information. Whenever that happens, I win and that solves one of the problems that I need solved. Thus, a type system is a way for me to express certain axioms about my algorithm. A dynamic type system encodes those facts as part of the computation. A static type system pre-calculates certain "theorems" from my axioms and uses those theorems to allow my algorithm to be computed without all the facts being stored as part of the computation. Hopefully, this makes my point of view clear. -Chris ***************************************************************************** Chris Clark Internet : [EMAIL PROTECTED] Compiler Resources, Inc. Web Site : http://world.std.com/~compres 23 Bailey Rd voice : (508) 435-5016 Berlin, MA 01503 USA fax : (978) 838-0263 (24 hours) ------------------------------------------------------------------------------ -- http://mail.python.org/mailman/listinfo/python-list
