In comp.lang.functional Anton van Straaten <[EMAIL PROTECTED]> wrote: [...] > I reject this comparison. There's much more to it than that. The point > is that the reasoning which programmers perform when working with an > program in a latently-typed language bears many close similiarities to > the purpose and behavior of type systems.
> This isn't an attempt to jump on any bandwagons, it's an attempt to > characterize what is actually happening in real programs and with real > programmers. I'm relating that activity to type systems because that is > what it most closely relates to. [...] I think that we're finally getting to the bottom of things. While reading your reponses something became very clear to me: latent-typing and latent- types are not a property of languages. Latent-typing, also known as informal reasoning, is something that all programmers do as a normal part of programming. To say that a language is latently-typed is to make a category mistake, because latent-typing is not a property of languages. A programmer, working in any language, whether typed or not, performs informal reasoning. I think that is fair to say that there is a correspondence between type theory and such informal reasoning. The correspondence is like the correspondence between informal and formal math. *But* , informal reasoning (latent-typing) is not a property of languages. An example of a form of informal reasoning that (practically) every programmer does daily is termination analysis. There are type systems that guarantee termination, but I think that is fair to say that it is not yet understood how to make a practical general purpose language, whose type system would guarantee termination (or at least I'm not aware of such a language). It should also be clear that termination analysis need not be done informally. Given a program, it may be possible to formally prove that it terminates. I'm now more convinced than ever that "(latently|dynamically)-typed language" is an oxymoron. The terminology really needs to be fixed. -Vesa Karvonen -- http://mail.python.org/mailman/listinfo/python-list
