What is Expressiveness in a Computer Language

[Chris Smith]

Anton van Straaten <anton at appsolutions.com> wrote:
> The problem is that there are no useful sound definitions for the type 
> systems (in the static sense) of dynamically-typed languages.  Yet, we 
> work with type-like static properties in those languages all the time, 
> as I've been describing.

I honestly don't find it very compelling that there are similarities 
between the kinds of reasoning that goes on in static type systems 
versus those used by programmers in dynamically typed languages.  
Rather, of course there are similarities.  It would be shocking if there 
were not similarities.  These similarities, though, have nothing to with 
the core nature of types.

Basically, there are ways to reason about programs being correct.  
Static type systems describe their reasoning (which is always axiomatic 
in nature) by assigning "types" to expressions.  Programmers in 
dynamically typed languages still care about the correctness of their 
programs, though, and they find ways to reason about their programs as 
well.  That reasoning is not completely axiomatic, but we spend an 
entire lifetime applying this basic logical system, and it makes sense 
that programmers would try to reason from premises to conclusions in 
ways similar to a type system.  Sometimes they may even ape other type 
systems with which they are familiar; but even a programmer who has 
never worked in a typed language would apply the same kind of logic as 
is used by type systems, because it's a form of logic with which 
basically all human beings are familiar and have practiced since the age 
of three (disclaimer: I am not a child psychologist).

On the other hand, programmers don't restrict themselves to that kind of 
pure axiomatic logic (regardless of whether the language they are 
working in is typed).  The also reason inductively -- in the informal 
sense -- and are satisfied with the resulting high probabilities.  They 
generally apply intuitions about a problem statement that is almost 
surely not written clearly enough to be understood by a machine.  And so 
forth.

What makes static type systems interesting is not the fact that these 
logical processes of reasoning exist; it is the fact that they are 
formalized with definite axioms and rules of inference, performed 
entirely on the program before execution, and designed to be entirely 
evaluatable in finite time bounds according to some procedure or set of 
rules, so that a type system may be checked and the same conclusion 
reached regardless of who (or what) is doing the checking.  All that, 
and they still reach interesting conclusions about programs.  If 
informal reasoning about types doesn't meet these criteria (and it 
doesn't), then it simply doesn't make sense to call it a type system 
(I'm using the static terminology here).  It may make sense to discuss 
some of the ways that programmer reasoning resembles types, if indeed 
there are resemblances beyond just that they use the same basic rules of 
logic.  It may even make sense to try to identify a subset of programmer 
reasoning that even more resembles... or perhaps even is... a type 
system.  It still doesn't make sense to call programmer reasoning in 
general a type system.

In the same post here, you simultaneously suppose that there's something 
inherently informal about the type reasoning in dynamic languages; and 
then talk about the type system "in the static sense" of a dynamic 
language.  How is this possibly consistent?

> We know that we can easily take dynamically-typed program fragments and 
> assign them type schemes, and we can make sure that the type schemes 
> that we use in all our program fragments use the same type system.

Again, it would be surprising if this were not true.  If programmers do, 
in fact, tend to reason correctly about their programs, then one would 
expect that there are formal proofs that could be found that they are 
right.  That doesn't make their programming in any way like a formal 
proof.  I tend to think that a large number of true statements are 
provable, and that programmers are good enough to make a large number of 
statements true.  Hence, I'd expect that it would be possible to find a 
large number of true, provable statements in any code, regardless of 
language.

> So we actually have quite a bit of evidence about the presence of static 
> types in dynamically-typed programs.

No.  What we have is quite a bit of evidence about properties remaining 
true in dynamically typed programs, which could have been verified by 
static typing.

> We're currently discussing something that so far has only been captured 
> fairly informally.  If we restrict ourselves to only what we can say 
> about it formally, then the conversation was over before it began.

I agree with that statement.  However, I think the conversation 
regarding static typing is also over when you decide that the answer is 
to weaken static typing until the word applies to informal reasoning.  
If the goal isn't to reach a formal understanding, then the word "static 
type" shouldn't be used; and when that is the goal, it still shouldn't 
be applied to process that aren't formalized until they manage to become 
formalized.

Hopefully, this isn't perceived as too picky.  I've already conceded 
that we can use "type" in a way that's incompatible with all existing 
research literature.  I would, however, like to retain some word with 
actually has that meaning.  Otherwise, we are just going to be 
linguistically prevented from discussing it.

-- 
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation