What is Expressiveness in a Computer Language

[rossberg at ps.uni-sb.de]

Anton van Straaten wrote:
>
> Languages with latent type systems typically don't include type
> declarations in the source code of programs.  The "static" type scheme
> of a given program in such a language is thus latent, in the English
> dictionary sense of the word, of something that is present but
> undeveloped.  Terms in the program may be considered as having static
> types, and it is possible to infer those types, but it isn't necessarily
> easy to do so automatically, and there are usually many possible static
> type schemes that can be assigned to a given program.
>
> Programmers infer and reason about these latent types while they're
> writing or reading programs.  Latent types become manifest when a
> programmer reasons about them, or documents them e.g. in comments.

I very much agree with the observation that every programmer performs
"latent typing" in his head (although Pascal Constanza's seems to have
the opposite opinion).

But I also think that "latently typed language" is not a meaningful
characterisation. And for the very same reason! Since any programming
activity involves latent typing - naturally, even in assembler! - it
cannot be attributed to any language in particular, and is hence
useless to distinguish between them. (Even untyped lambda calculus
would not be a counter-example. If you really were to program in it,
you certainly would think along lines like "this function takes two
chuch numerals and produces a third one".)

I hear you when you define latently typed languages as those that
support the programmer's latently typed thinking by providing dynamic
tag checks. But in the very same post (and others) you also explain in
length why these tags are far from being actual types. This seems a bit
contradictory to me.

As Chris Smith points out, these dynamic checks are basically a
necessaity for a well-defined operational semantics. You need them
whenever you have different syntactic classes of values, but lack a
type system to preclude interference. They are just an encoding for
differentiating these syntactic classes. Their connection to types is
rather coincidential.

- Andreas