Saying "latently-typed language" is making a category mistake

[Anton van Straaten]

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