I wrote: > These informal systems, which may not prove what they claim to prove > are my concept of a "type system".
Chris Smith <[EMAIL PROTECTED]> replied: > Okay, that works. I'm not sure where it gets us, though.... Ok, we'll get there. First, we need to step back in time, to when there was roughly algol, cobol, fortran, and lisp. Back then, at least as I understood things, there were only a few types that generally people understood integer, real, and (perhaps) pointer. Now, with algol or fortran things were generally only of the first two types and variables were statically declared to be one or the other. With lisp any cell could hold any one of the 3, and some clever implementor added "tag bits" to distinguish which the cell held. As I understood it, the tag bits weren't originally for type correctness, so much as they facilitated garbage collection. The garbage collector didn't know what type of data you put in a cell and had to determine which cells contained pointers, so that the mark-and-sweep algorithms could sweep by following the pointers (and not following the integers that looked like pointers). Still, these tag bits did preserve the "dynamic" type, in the sense that we knew types from the other languages. As I remember it, sophistication with type really didn't occur as a phenomena for the general programmer until the introduction of Pascal (and to a lesser extent PL/I). Moreover, as I recall it, perhaps because I didn't learn the appropriate dialect was that lisp dialects kept with the more general notion of type (lists and tuples) and eschewed low-level bit-fiddling where we might want to talk about a 4 bit integer representing 0 .. 15 or -8 .. 7. The important thing is the dynamicism of lisp allowed one to write polymorphic programs, before most of us knew the term. However, we still had a notion of type: integers and floating point numbers were still different and one could not portably use integer operations on floating pointer values or vice versa. However, one could check the tag and "do the right thing" and many lisp primitives did just that, making them polymorphic. The way most of us conceived (or were taught to conceive) of the situation was that there still were types, they were just associated with values and the type laws we all knew and loved still worked, they just worked dynamically upon the types of the operand values that were presented at the time. Can this be made rigorous? Perhaps. Instead of viewing the text of the program staticly, let us view it dynamicly, that is by introducing a time (or execution) dimension. This is easier if you take an imperative view of the dynamic program and imagine things having an operational semantics, which is why we stepped back in time in the first place, so that we are in a world where imperative programming is the default model for most programmers. Thus, as we traverse a list, the first element might be an integer, the second a floating point value, the third a sub-list, the fourth and fifth, two more integers, and so on. If you look statically at the head of the list, we have a very wide union of types going by. However, perhaps there is a mapping going on that can be discerned. For example, perhaps the list has 3 distinct types of elements (integers, floating points, and sub-lists) and it circles through the types in the order, first having one of each type, then two of each type, then four of each type, then eight, and so on. The world is now patterned. However, I don't know how to write a static type annotation that describes exactly that type. That may just be my lack of experience in writing annotations. However, it's well within my grasp to imagine the appropriate type structure, even though **I** can't describe it formally. More importantly, I can easily write something which checks the tags and sees whether the data corresponds to my model. And, this brings us to the point, if the data that my program encounters doesn't match the model I have formulated, then something is of the wrong "type". Equally importantly, the dynamic tags, have helped me discover that type error. Now, the example may have seemed arbitrary to you, and it was in some sense arbitrary. However, if one imagines a complete binary tree with three kinds elements stored in memory as rows per depth, one can get exactly the structure I described. And, if one were rewriting that unusual representation to a more normal one, one might want exactly the "type check" I proposed to validate that the input binary tree was actually well formed. Does this help explain dynamic typing as a form of typing? -Chris -- http://mail.python.org/mailman/listinfo/python-list
