Chris Uppal wrote: >>> >>>Well, it seems to me that you are /assuming/ a notion of what kinds of >>>logic can be called type (theories), and I don't share your >>>assumptions. No offence intended. >> >>OK, but can you point me to any literature on type theory that makes a >>different assumption? > > 'Fraid not. (I'm not a type theorist -- for all I know there may be lots, but > my suspicion is that they are rare at best.)
I would suspect the same :-). And the reason is that "type" has a well-established use in theory. It is not just my "assumption", it is established practice since 80 or so years. So far, this discussion has not revealed the existence of any formal work that would provide a theory of "dynamic types" in the sense it is used to characterise "dynamically typed" languages. So what you are suggesting may be an interesting notion, but it's not what is called "type" in a technical sense. Overloading the same term for something different is not a good idea if you want to avoid confusion and misinterpretations. > But, as a sort of half-way, semi-formal, example: consider the type > environment > in a Java runtime. The JVM does formal type-checking of classfiles as it > loads > them. In most ways that checking is static -- it's treating the bytecode as > program text and doing a static analysis on it before allowing it to run (and > rejecting what it can't prove to be acceptable by its criteria). However, it > isn't /entirely/ static because the collection of classes varies at runtime in > a (potentially) highly dynamic way. So it can't really examine the "whole" > text of the program -- indeed there is no such thing. So it ends up with a > hybrid static/dynamic type system -- it records any assumptions it had to make > in order to find a proof of the acceptability of the new code, and if > (sometime > in the future) another class is proposed which violates those assumptions, > then > that second class is rejected. Incidentally, I know this scenario very well, because that's what I'm looking at in my thesis :-). All of this can easily be handled coherently with well-established type machinery and terminology. No need to bend existing concepts and language, no need to resort to "dynamic typing" in the way Java does it either. > In code which will be executed at instant A > obj aMessage. "type correct" > obj anotherMessage. "type incorrect" > > In code which will be executed at instant B > obj aMessage. "type incorrect" > obj anotherMessage. "type correct" > > I don't see how a logic with no temporal element can arrive at all four those > judgements, whatever it means by a union type. I didn't say that the type system cannot have temporal elements. I only said that a type itself cannot change over time. A type system states propositions about a program, a type assignment *is* a proposition. A proposition is either true or false (or undecidable), but it is so persistently, considered under the same context. So if you want a type system to capture temporal elements, then these must be part of a type itself. You can introduce types with implications like "in context A, this is T, in context B this is U". But the whole quoted part then is the type, and it is itself invariant over time. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
