Chris Uppal <[EMAIL PROTECTED]> wrote: > I think we're agreed (you and I anyway, if not everyone in this thread) that > we > don't want to talk of "the" type system for a given language. We want to > allow > a variety of verification logics. So a static type system is a logic which > can > be implemented based purely on the program text without making assumptions > about runtime events (or making maximally pessimistic assumptions -- which > comes > to the same thing really). I suggest that a "dynamic type system" is a > verification logic which (in principle) has available as input not only the > program text, but also the entire history of the program execution up to the > moment when the to-be-checked operation is invoked.
I am trying to understand how the above statement about dynamic types actually says anything at all. So a dynamic type system is a system of logic by which, given a program and a path of program execution up to this point, verifies something. We still haven't defined "something", though. We also haven't defined what happens if that verification fails. One or the other or (more likely) some combination of the two must be critical to the definition in order to exclude silly applications of it. Presumably you want to exclude from your definition of a dynamic "type system" which verifies that a value is non-negative, and if so executes the block of code following "then"; and otherwise, executes the block of code following "else". Yet I imagine you don't want to exclude ALL systems that allow the programmer to execute different code when the verification fails (think exception handlers) versus succeeds, nor exclude ALL systems where the condition is that a value is non-negative. In other words, I think that everything so far is essentially just defining a dynamic type system as equivalent to a formal semantics for a programming language, in different words that connote some bias toward certain ways of looking at possibilities that are likely to lead to incorrect program behavior. I doubt that will be an attractive definition to very many people. > Note that not all errors that I would want to call type errors are necessarily > caught by the runtime -- it might go happily ahead never realising that it had > just allowed one of the constraints of one of the logics I use to reason about > the program. What's known as an undetected bug -- but just because the > runtime > doesn't see it, doesn't mean that I wouldn't say I'd made a type error. (The > same applies to any specific static type system too, of course.) In static type system terminology, this quite emphatically does NOT apply. There may, of course, be undetected bugs, but they are not type errors. If they were type errors, then they would have been detected, unless the compiler is broken. If you are trying to identify a set of dynamic type errors, in a way that also applies to statically typed languages, then I will read on. > But the checks the runtime does perform (whatever they are, and whenever they > happen), do between them constitute /a/ logic of correctness. In many highly > dynamic languages that logic is very close to being maximally optimistic, but > it doesn't have to be (e.g. the runtime type checking in the JMV is pretty > pessimistic in many cases). > > Anyway, that's more or less what I mean when I talk of dynamically typed > language and their dynamic type systems. So my objections, then, are in the first paragraph. > [**] Although there are operations which are not possible, reading another > object's instvars directly for instance, which I suppose could be taken to > induce a non-trivial (and static) type logic. In general, I wouldn't consider a syntactically incorrect program to have a static type error. Type systems are, in fact, essentially a tool so separate concerns; specifically, to remove type-correctness concerns from the grammars of programming languages. By doing so, we are able at least to considerably simplify the grammar of the language, and perhaps also to increase the "tightness" of the verification without risking making the language grammar context-sensitive. (I'm unsure about the second part of that statement, but I can think of no obvious theoretical reason to assume that combining a type system with a regular context- free grammar would yield another context-free grammar. Then again, formal languages are not my strong point.) -- Chris Smith - Lead Software Developer / Technical Trainer MindIQ Corporation -- http://mail.python.org/mailman/listinfo/python-list