I wrote: > The important thing is the dynamicism of lisp allowed one to write > polymorphic programs, before most of us knew the term.
Chris Smith <[EMAIL PROTECTED]> writes: > Sure. In exchange for giving up the proofs of the type checker, you > could write all kinds of programs. To this day, we continue to write > programs in languages with dynamic checking features because we don't > have powerful enough type systems to express the corresponding type > system. And to me the question is what kinds of types apply to these dynamic programs, where in fact you may have to solve the halting problem to know exactly when some statement is executed. I expect that some programs have type signatures that exceed the expressibility of any static system (that is Turing complete). Therefore, we need something that "computes" the appropriate type at run-time, because we need full Turing power to compute it. To me such a system is a "dynamic type system". I think dynamic tags are a good approximation, because they only compute what type the expression has this time. > I believe that, in fact, it would be trivial to imagine a type system > which is capable of expressing that type. Okay, not trivial, since it > appears to be necessary to conceive of an infinite family of integer > types with only one value each, along with range types, and > relationships between them; but it's probably not completely beyond the > ability of a very bright 12-year-old who has someone to describe the > problem thoroughly and help her with the notation. Well, it look like you are right in that I see following is a Haskell program that looks essentially correct. I wanted something that was simple enough that one could see that it could be computed, but which was complex enough that it had to be computed (and couldn't be statically expressed with a system that did no "type computations"). Perhaps, there is no such beast. Or, perhaps I just can't formulate it. Or, perhaps we have static type checkers which can do computations of unbounded complexity. However, I thought that one of the characteristics of type systems was that they did not allow unbounded complexity and weren't Turing Complete. > You would, of course, need a suitable type system first. For example, > it appears to me that there is simply no possible way of expressing what > you've described in Java, even with the new generics features. Perhaps > it's possible in ML or Haskell (I don't know). My point is that if you > were allowed to design a type system to meet your needs, I bet you could > do it. Or, I could do as I think the dynamic programmers do, dispense with trying to formulate a sufficiently general type system and just check the tags at the appropriate points. > Sure. The important question, then, is whether there exists any program > bug that can't be formulated as a type error. If you allow Turing Complete type systems, then I would say no--every bug can be reforumlated as a type error. If you require your type system to be less powerful, then some bugs must escape it. -Chris -- http://mail.python.org/mailman/listinfo/python-list
