Vesa Karvonen <[EMAIL PROTECTED]> wrote: > 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.
It's pretty clear to me that there are two different things here. There is the set of reasoning that is done about programs by programmers. This may or may not have some subset called "type reasoning", depending on whether there's a real difference between type reasoning and any other reasoning about program behavior, or it's just a word that we've learned from early experience to use in certain rather arbitrary contexts. In either case, then there are language features that look sort of type-like which can support that same reasoning about program behavior. It is, to me, an interesting question whether those language features are really intrinsically connected to that form of reasoning about program behavior, or whether they are just one way of doing it where others would suffice as well. Clearly, there is some variation in these supporting language features between languages that have them... for example, whether there are only a fixed set of type tags, or an infinite (or logically infinite, anyway) set, or whether the type tags may have other type tags as parameters, or whether they even exist as tags at all or as sets of possible behaviors. Across all these varieties, the phrase "latently typed language" seems to be a reasonable shorthand for "language that supports the programmer in doing latent-type reasoning". Of course, there are still problems here, but really only if you share my skepticism that there's any difference between type reasoning and any other reasoning that's done by programmers on their programs. Perhaps, if you wanted to be quite careful about your distinctions, you may want to choose different words for the two. However, then you run into that same pesky "you can't choose other people's terminology" block again. > 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. I'd be more careful in the analogy, there. Since type theory (as applied to programming languages, anyway) is really just a set of methods of proving arbitrary statements about program behaviors, a corresponding "informal type theory" would just be the entire set of informal reasoning by programmers about their programs. That would agree with my skepticism, but probably not with too many other people. > An example of a form of informal reasoning that (practically) every > programmer does daily is termination analysis. Or perhaps you agree with my skepticism, here. This last paragraph sounds like you're even more convinced of it than I am. -- Chris Smith - Lead Software Developer / Technical Trainer MindIQ Corporation -- http://mail.python.org/mailman/listinfo/python-list
