Vesa Karvonen 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. > > 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.
Well, it's obviously the case that latent types as I've described them are not part of the usual semantics of dynamically typed languages. In other messages, I've mentioned types like "number -> number" which have no meaning in a dynamically typed language. You can only write them in comments (unless you implement some kind of type handling system), and language implementations aren't aware of such types. OTOH, a programmer reasoning explicitly about such types, writing them in comments, and perhaps using assertions to check them has, in a sense, defined a language. Having done that, and reasoned about the types in his program, he manually erases them, "leaving" code written in the original dynamically-typed language. You can think of it as though it were generated code, complete with comments describing types, injected during the erasure process. So, to address your category error objection, I would say that latent typing is a property of latently-typed languages, which are typically informally-defined supersets of what we know as dynamically-typed languages. I bet that doesn't make you happy, though. :D Still, if that sounds a bit far-fetched, let me start again at ground level, with a Haskell vs. Scheme example: let double x = x * 2 vs.: (define (double x) (* x 2)) Programmers in both languages do informal reasoning to figure out the type of 'double'. I'm assuming that the average Haskell programmer doesn't write out a proof whenever he wants to know the type of a term, and doesn't have a compiler handy. But the Haskell programmer's informal reasoning takes place in the context of a well-defined formal type system. He knows what the "type of double" means: the language defines that for him. The type-aware Scheme programmer doesn't have that luxury: before he can talk about types, he has to invent a type system, something to give meaning to an expression such as "number -> number". Performing that invention gives him types -- albeit informal types, a.k.a. latent types. In the Haskell case, the types are a property of the language. If you're willing to acknowledge the existence of something like latent types, what are they a property of? Just the amorphous informal cloud which surrounds dynamically-typed languages? Is that a satisfactory explanation of these two quite similar examples? I want to mention two other senses in which latent types become connected to real languages. That doesn't make them properties of the formal semantics of the language, but the connection is a real one at a different level. The first is that in a language without a rich formal type system, informal reasoning outside of the formal type system becomes much more important. Conversely, in Haskell, even if you accept the existence of latent types, they're close enough to static types that it's hardly necessary to consider them. This is why latent types are primarily associated with languages without rich formal type systems. The second connection is via tags: these are part of the definition of a dynamically-typed language, and if the programmer is reasoning explicitly about latent types, tags are a useful tool to help ensure that assumptions about types aren't violated. So this is a connection between a feature in the semantics of the language, and these extra-linguistic latent types. > 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. Right. And this is partly why talking about latent types, as opposed to the more general "informal reasoning", makes sense: because latent types are addressing the same kinds of things that static types can capture. Type-like things. > I'm now more convinced than ever that "(latently|dynamically)-typed > language" is an oxymoron. The terminology really needs to be fixed. I agree that fixing is needed. The challenge is to do it in a way that accounts for, rather than simply ignores, the many informal correlations to formal type concepts that exist in dynamically-typed languages. Otherwise, the situation won't improve. Anton -- http://mail.python.org/mailman/listinfo/python-list