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

[Chris Smith]

Vesa Karvonen <vesa.karvonen at cs.helsinki.fi> 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