Chris F Clark <[EMAIL PROTECTED]> wrote: > Chris Smith <[EMAIL PROTECTED]> writes: > > I thought about this in the context of reading Anton's latest post to > > me, but I'm just throwing out an idea. > > I wrote: > > I think there is some sense of convergence here. > > Apologies for following-up to my own post, but I forgot to describe > the convergence. > > The convergence is there is something more general that what type > theorists talk about when discussing types. Type theory is an > abstraction and systemization of reasoning about types. This more > general reasoning doesn't need to be sound, it just needs to be based > aound "types" and computations.
Unfortunately, I have to again reject this idea. There is no such restriction on type theory. Rather, the word type is defined by type theorists to mean the things that they talk about. Something becomes a type the instant someone conceives of a type system that uses it. We could try to define a dynamic type system, as you seem to say, as a system that checks against only what can be known about some ideal type system that would be able to prove the program valid... but I immediately begin to wonder if it would ever be possible to prove that something is a dynamic type system for a general-purpose (Turing- complete) language. If you could define types for a dynamic type system in some stand-alone way, then this difficulty could be largely pushed out of the way, because we could say that anything that checks types is a type system, and then worry about verifying that it's a sound type system without worrying about whether it's a subset of the perfect type system. So back to that problem again. You also wrote: > I consider any case where a program gives a function outside of its > domain a "type error", because an ideal (but unacheivable) type system > would have prevented it. That does not make all errors, type errors, > because if I give a program an input within its domain and it > mis-computes the result, that is not a type error. So what is the domain of a function? (Heck, what is a function? I'll neglect that by assuming that a function is just an expression; otherwise, this will get more complicated.) I see three possible ways to look at a domain. (I need a word here that implies something like a set, but I don't care to verify the axioms of set theory. I'm just going to use set. Hope that's okay.) 1. The domain is the set of inputs to that expression which are going to produce a correct result. 2. The domain is the set of inputs that I expected this expression to work with when I wrote it. 3. The domain is the set of inputs for which the expression has a defined result within the language semantics. So the problem, then, more clearly stated, is that we need something stronger than #3 and weaker than #1, but #2 includes some psychological nature that is problematic to me (though, admittedly, FAR less problematic than the broader uses of psychology to date.) Is that a fair description of where we are in defining types, then? -- Chris Smith - Lead Software Developer / Technical Trainer MindIQ Corporation -- http://mail.python.org/mailman/listinfo/python-list
