Chris Smith <[EMAIL PROTECTED]> writes: > 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. Do you reject that there could be something more general than what a type theorist discusses? Or do you reject calling such things a type? Let you write: > 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. I'm particularly interested if something unsound (and perhaps ambiguous) could be called a type system. I definitely consider such things type systems. However, I like my definitions very general and vague. Your writing suggests the opposite preference. To me if something works in an analogous way to how a known type system, I tend to consider it a "type system". That probably isn't going to be at all satisfactory to someone wanting a more rigorous definition. Of course, to my mind, the rigorous definitions are just an attempt to capture something that is already known informally and put it on a more rational foundation. > So what is the domain of a function? (Heck, what is a function? ... > (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.) Yes, I meant the typical HS algebra definition of domain, which is a set, same thing for function. More rigorous definitions can be sustituted as necessary and appropriate. > 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.) Actually, I like 2 quite well. There is some set in my mind when I'm writing a particular expression. It is likely an ill-defined set, but I don't notice that. That set is exactly the "type". I approximate that set and it's relationships to other sets in my program with the typing machinery of the language I am using. That is the static (and well-founded) type. It is however, only an approximation to the ideal "real" type. If I could make that imaginary mental set concrete (and well-defined), that would be exactly my concept of type. Now, that overplays the conceptual power in my mind. My mental image is influenced by my knowledge of the semantics of the language and also any implementations I may have used. Thus, I will weaken 2 to be closer to 3, because I don't expect a perfectly ideal type system, just an approximation. To the extent that I am aware of gotchas in the language or a relavent implementation, I amy write extra code to try and limit things to model 1. Note that in my fallible mind, 1 and 2 are identical. In my hubris, I expect that the extra checks I have made have restricted my inputs to where model 3 and 1 coincide.
Expanding that a little. I expect the language to catch type errors where I violate model 3. To the extent model 3 differs from model 1 and my code hasn't added extra checks to catch it, I have bugs resulting from undetected type errors or perhaps modelling errors. To me they are type errors, because I expect that there is a typing system that captures 1 for the program I am writing, even though I know that that is not generally true. As I reflect on this more, I really do like 2 in the sense that I believe there is some abstract Platonic set that is an ideal type (like 1) and that is what the type system is approximating. to the sense that languages approximate either 1 or 2, those facilites are type facilities of a language. That puts me very close to your (rejected) definition of type as the well-defined semantics of the language. Except I think of types as the sets of values that the language provides, so it isn't the entire semantics of the language, just that part which divides values into discrete sets which are approriate to different operations (and detect inaapropriate values). -Chris -- http://mail.python.org/mailman/listinfo/python-list