What is Expressiveness in a Computer Language

[Anton van Straaten]

Vesa Karvonen wrote:
> 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.

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.

Usually, formal type theory ignores such things, because of course 
what's in the programmer's head is outside the domain of the formal 
definition of an untyped language.  But all that means is that formal 
type theory can't account for the entirety of what's happening in the 
case of programs in untyped languages.

Unless you can provide some alternate theory of the subject that's 
better than what I'm offering, it's not sufficient to complain "but that 
goes beyond (static/syntactic) type theory".  Yes, it goes beyond 
traditional type theory, because it's addressing with something which 
traditional type theory doesn't address.  There are reasons to connect 
it to type theory, and if you can't see those reasons, you need to be 
more explicit about why.

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

The problem with "untyped" is that there are obvious differences in 
typing behavior between the untyped lambda calculus and, say, a language 
like Scheme (and many others).  Like all latently-typed languages, 
Scheme includes, in the language, mechanisms to tag values in a way that 
supports checks which help the programmer to ensure that the program's 
behavior matches the latent type scheme that the programmer has in mind. 
  See my other recent reply to Marshall for a more detailed explanation 
of what I mean.

I'm suggesting that if a language classifies and tags values in a way 
that supports the programmer in static reasoning about the behavior of 
terms, that calling it "untyped" does not capture the entire picture, 
even if it's technically accurate in a restricted sense (i.e. in the 
sense that terms don't have static types that are known within the 
language).

Let me come at this from another direction: what do you call the 
classifications into number, string, vector etc. that a language like 
Scheme does?  And when someone writes a program which includes the 
following lines, how would you characterize the contents of the comment:

; third : integer -> integer
(define (third n) (quotient n 3))

In my experience, answering these questions without using the word 
"type" results in a lot of silliness.  And if you do use "type", then 
you're going to have to adjust the rest of your position significantly.

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

The first point I was making is that *automated* checking has very 
little to do with anything, and conflating static types with automated 
checking tends to lead to a lot of confusion on both sides of the 
static/dynamic fence.

But as to your point, latently typed languages have informal type 
systems.  Show me a latently typed language or program, and I can tell 
you a lot about its type system or type scheme.

Soft type inferencers demonstrate this by actually defining a type 
system and inferring type schemes for programs.  That's a challenging 
thing for an automated tool to do, but programmers routinely perform the 
same sort of activity on an informal basis.

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

Again, the type system is informal.  What you're essentially saying is 
that only things that are formally defined make sense.  But you can't 
wish dynamically-checked languages out of existence.  So again, how 
would you characterize these issues in dynamically-checked languages?

Saying that it's just a matter of well-defined semantics doesn't do 
anything to address the details of what's going on.  I'm asking for a 
more specific account than that.

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

I agree, to make the comparison perfect, you'd need to define a type 
system.  But that's been done in various cases.  So is your complaint 
simply that most programmers are working with informal type systems? 
I've already stipulated that.

However, I think that you want to suggest that those programmers are not 
working with type systems at all.

This reminds me of a comedy skit which parodied the transparency of 
Superman's secret identity: Clark Kent is standing in front of Lois Lane 
and removes his glasses for some reason.  Lois looks confused and says 
"where did Clark go?"  Clark quickly puts his glasses back on, and Lois 
breathes a sigh of relief, "Oh, there you are, Clark".

The problem we're dealing with in this case is that anything that's not 
formally defined is essentially claimed to not exist.  It's lucky that 
this isn't really the case, otherwise much of the world around us would 
vanish in a puff of formalist skepticism.

We're discussing systems that operate on an informal basis: in this 
case, the reasoning about the classification of values which flow 
through terms in a dynamically-checked language.  If you can produce a 
useful formal model of those systems that doesn't omit significant 
information, that's great, and I'm all ears.

However, claiming that e.g. using a universal type is a complete model 
what's happening misses the point: it doesn't account at all for the 
reasoning process I've just described.

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

Again, your two suggested replacements don't come close to capturing 
what I'm talking about.  Without better alternatives, "type" is the 
closest appropriate term.  I'm qualifying it with the term "latent", 
precisely to indicate that I'm not talking about formally-defined types.

I'm open to alternative terminology or ways of characterizing this, but 
they need to address issues that exist outside the boundaries of formal 
type systems, so simply applying terms from formal type theory is not 
usually sufficient.

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

This and my other recent post give a fair amount of qualification, so 
let me know if you need anything else to be convinced. :)

But to be fair, I'll start using "untyped" if you can come up with a 
satisfactory answer to the two questions I asked above, just before I 
used the word "silliness".

Anton