What is Expressiveness in a Computer Language

[Anton van Straaten]

Marshall wrote:
> Joe Marshall wrote:
> 
>>They *do* have a related meaning.  Consider this code fragment:
>>(car "a string")
>>[...]
>>Both `static typing' and `dynamic typing' (in the colloquial sense) are
>>strategies to detect this sort of error.
> 
> 
> The thing is though, that putting it that way makes it seems as
> if the two approaches are doing the same exact thing, but
> just at different times: runtime vs. compile time. But they're
> not the same thing. Passing the static check at compile
> time is universally quantifying the absence of the class
> of error; passing the dynamic check at runtime is existentially
> quantifying the absence of the error. A further difference is
> the fact that in the dynamically typed language, the error is
> found during the evaluation of the expression; in a statically
> typed language, errors are found without attempting to evaluate
> the expression.
> 
> I find everything about the differences between static and
> dynamic to be frustratingly complex and subtle.

Let me add another complex subtlety, then: the above description misses 
an important point, which is that *automated* type checking is not the 
whole story.  I.e. that compile time/runtime distinction is a kind of 
red herring.

In fact, automated type checking is orthogonal to the question of the 
existence of types.  It's perfectly possible to write fully typed 
programs in a (good) dynamically-checked language.

In a statically-checked language, people tend to confuse automated 
static checking with the existence of types, because they're thinking in 
a strictly formal sense: they're restricting their world view to what 
they see "within" the language.

Then they look at programs in a dynamically-checked language, and see 
checks happening at runtime, and they assume that this means that the 
program is "untyped".

It's certainly close enough to say that the *language* is untyped.  One 
could also say that a program, as seen by the language, is untyped.

But a program as seen by the programmer has types: the programmer 
performs (static) type inference when reasoning about the program, and 
debugs those inferences when debugging the program, finally ending up 
with a program which has a perfectly good type scheme.  It's may be 
messy compared to say an HM type scheme, and it's usually not proved to 
be perfect, but that again is an orthogonal issue.

Mathematicians operated for thousands of years without automated 
checking of proofs, so you can't argue that because a 
dynamically-checked program hasn't had its type scheme proved correct, 
that it somehow doesn't have types.  That would be a bit like arguing 
that we didn't have Math until automated theorem provers came along.

These observations affect the battle over terminology in various ways. 
I'll enumerate a few.

1. "Untyped" is really quite a misleading term, unless you're talking 
about something like the untyped lambda calculus.  That, I will agree, 
can reasonably be called untyped.

2.  "Type-free" as suggested by Chris Smith is equally misleading.  It's 
only correct in a relative sense, in a narrow formal domain which 
ignores the process of reasoning about types which is inevitably 
performed by human programmers, in any language.

3.  A really natural term to refer to types which programmers reason 
about, even if they are not statically checked, is "latent types".  It 
captures the situation very well intuitively, and it has plenty of 
precedent -- e.g. it's mentioned in the Scheme reports, R5RS and its 
predecessors, going back at least a decade or so (haven't dug to check 
when it first appeared).

4.  Type theorists like to say that "universal" types can be used in a 
statically-typed language to subsume "dynamic types".  Those theorists 
are right, the term "dynamic type", with its inextricable association 
with runtime checks, definitely gets in the way here.  It might be 
enlightening to rephrase this: what's really happening is that universal 
types allow you to embed a latently-typed program in a 
statically-checked language.  The latent types don't go anywhere, 
they're still latent in the program with universal types.  The program's 
statically-checked type scheme doesn't capture the latent types. 
Describing it in these terms clarifies what's actually happening.

5.  Dynamic checks are only part of the mechanism used to verify latent 
types.  They shouldn't be focused on as being the primary equivalent to 
  static checks.  The closest equivalent to the static checks is a 
combination of human reasoning and testing, in which dynamic checks play 
an important but ultimately not a fundamental part.  You could debug a 
program and get the type scheme correct without dynamic checks, it would 
just be more difficult.

So, will y'all just switch from using "dynamically typed" to "latently 
typed", and stop talking about any real programs in real programming 
languages as being "untyped" or "type-free", unless you really are 
talking about situations in which human reasoning doesn't come into 
play?  I think you'll find it'll help to reason more clearly about this 
whole issue.

Thanks for your cooperation!!

Anton