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

[Vesa Karvonen]

In comp.lang.functional Anton van Straaten <anton at appsolutions.com> 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