Chris F Clark <[EMAIL PROTECTED]> wrote: > These informal systems, which may not prove what they claim to prove > are my concept of a "type system".
Okay, that works. I'm not sure where it gets us, though, except for gaining you the right to use "type system" in a completely uninteresting sense to describe your mental processes. You still need to be careful, since most statements from type theory about type systems tend to implicitly assume the property of being sound. I'm not exactly convinced that it's possible to separate that set of reasoning people do about programs into types and not-types, though. If you want to stretch the definition like this, then I'm afraid that you end up with the entire realm of human thought counting as a type system. I seem to recall that there are epistemologists who would be happy with that conclusion (I don't recall who, and I'm not actually interested enough to seek them out), but it doesn't lead to a very helpful sort of characterization. > It is to the people who are reasoning informally about > the program we wish to communicate that there is a type error. That > is, we want someone who is dealing with the program informally to > realize that there is an error, and that this error is somehow related > to some input not being kept within proper bounds (inside the domain > set) and that as a result the program will compute an unexpected and > incorrect result. I've lost the context for this part of the thread. We want this for what purpose and in what situation? I don't think we necessarily want this as the goal of a dynamic type system, if that's what you mean. There is always a large (infinite? I think so...) list of potential type systems under which the error would not have been a type error. How does the dynamic type system know which informally defined, potentially unsound, mental type system to check against? If it doesn't know, then it can't possibly know that something is a type error. If it does know, then the mental type system must be formally defined (if nothing else, operationally by the type checker.) > I also stress the informality, because beyond a certain nearly trivial > level of complexity, people are not capable of dealing with truly > formal systems. I think (hope, anyway) that you overstate the case here. We can deal with formal systems. We simply make errors. When those errors are found, they are corrected. Nevertheless, I don't suspect that a large part of the established base of theorems of modern mathematics are false, simply because they are sometimes rather involved reasoning in a complex system. Specifications are another thing, because they are often developed under time pressure and then extremely difficult to change. I agree that we should write better specs, but I think the main challenges are political and pragmatic, rather than fundamental to human understanding. > Therefore, I do not want to exlcude from type systems, things wich are > informal and unsound. They are simply artifacts of human creation. Certainly, though, when it is realized that a type system is unsound, it should be fixed as soon as possible. Otherwise, the type system doesn't do much good. It's also true, I suppose, that as soon as a person realizes that their mental thought process of types is unsound, they would want to fix it. The difference, though, is that there is then no formal definition to fix. -- Chris Smith - Lead Software Developer / Technical Trainer MindIQ Corporation -- http://mail.python.org/mailman/listinfo/python-list
