What is Expressiveness in a Computer Language

[Vesa Karvonen]

In comp.lang.functional Anton van Straaten <anton at appsolutions.com> wrote:
[...]

This static vs dynamic type thing reminds me of one article written by
Bjarne Stroustrup where he notes that "Object-Oriented" has become a
synonym for "good".  More precisely, it seems to me that both camps
(static & dynamic) think that "typed" is a synonym for having
"well-defined semantics" or being "safe" and therefore feel the need
to be able to speak of their language as "typed" whether or not it
makes sense.

> 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.

I agree.  I think that instead of "statically typed" we should say
"typed" and instead of "(dynamically|latently) typed" we should say
"untyped".

> 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.

That is not unreasonable.  You see, you can't have types unless you
have a type system.  Types without a type system are like answers
without questions - it just doesn't make any sense.

> 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".

Not in my experience.  Either a *language* specifies a type system or
not.  There is little room for confusion.  Well, at least unless you
equate "typing" with being "well-defined" or "safe" and go to great
lengths to convince yourself that your program has "latent types" even
without specifying a type system.

> It's certainly close enough to say that the *language* is untyped.

Indeed.  Either a language has a type system and is typed or has no
type system and is untyped.  I see very little room for confusion
here.  In my experience, the people who confuse these things are
people from the dynamic/latent camp who wish to see types everywhere
because they confuse typing with safety or having well-defined
semantics.

> 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.

There is a huge hole in your argument above.  Types really do not make
sense without a type system.  To claim that a program has a type
scheme, you must first specify the type system.  Otherwise it just
doesn't make any sense.

> 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.

No - not at all.  First of all, mathematics has matured quite a bit
since the early days.  I'm sure you've heard of the axiomatic method.
However, what you are missing is that to prove that your program has
types, you first need to specify a type system.  Similarly, to prove
something in math you start by specifying [fill in the rest].

> 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.

Untyped is not misleading.  "Typed" is not a synonym for "safe" or
"having well-defined semantics".

> So, will y'all just switch from using "dynamically typed" to "latently 
> typed"

I won't (use "latently typed").  At least not without further
qualification.

-Vesa Karvonen