What is Expressiveness in a Computer Language

[Chris Smith]

Pascal Costanza <pc at p-cos.net> wrote:
> Types can be represented at runtime via type tags. You could insist on 
> using the term "dynamically tagged languages", but this wouldn't change 
> a lot. Exactly _because_ it doesn't make sense in a statically typed 
> setting, the term "dynamically typed language" is good enough to 
> communicate what we are talking about - i.e. not (static) typing.

Okay, fair enough.  It's certainly possible to use the same sequence of 
letters to mean two different things in different contexts.  The problem 
arises, then, when Torben writes:

: That's not really the difference between static and dynamic typing.
: Static typing means that there exist a typing at compile-time that
: guarantess against run-time type violations.  Dynamic typing means
: that such violations are detected at run-time.

This is clearly not using the word "type" to mean two different things 
in different contexts.  Rather, it is speaking under the mistaken 
impression that "static typing" and "dynamic typing" are varieties of 
some general thing called "typing."  In fact, the phrase "dynamically 
typed" was invented to do precisely that.  My argument is not really 
with LISP programmers talking about types, by which they would mean 
approximately the same thing Java programmers mean by "class."  My point 
here concerns the confusion that results from the conception that there 
is this binary distinction (or continuum, or any other simple 
relationship) between a "statically typed" and a "dynamically typed" 
language.

Torben's (and I don't mean to single out Torben -- the terminology is 
used quite widely) classification of dynamic versus static type systems 
depends on the misconception that there is some universal definition to 
the term "type error" or "type violation" and that the only question is 
how we address these well-defined things.  It's that misconception that 
I aim to challenge.

> No, there is more: There is safe and unsafe code (i.e., code that throws 
> exceptions or that potentially just does random things). There are also 
> runtime systems where you have the chance to fix the reason that caused 
> the exception and continue to run your program. The latter play very 
> well with dynamic types / type tags.

Yes, I was oversimplifying.

> What type system catches division by zero? That is, statically?

I can define such a type system trivially.  To do so, I simply define a 
type for integers, Z, and a subtype for non-zero integers, Z'.  I then 
define the language such that division is only possible in an expression 
that looks like << z / z' >>, where z has type Z and z' has type Z'.  
The language may then contain an expression:

  z 0? t1 : t2

in which t1 is evaluated in the parent type environment, but t2 is 
evaluated in the type environment augmented by (z -> Z'), the type of 
the expression is the intersection type of t1 and t2 evaluated in those 
type environments, and the evaluation rules are defined as you probably 
expect.

> Would you like to program in such a language?

No.  Type systems for real programming languages are, of course, a 
balance between rigor and usability.  This particular set of type rules 
doesn't seem to exhibit a good balance.  Perhaps there is a way to 
achieve it in a way that is more workable, but it's not immediately 
obvious.

As another example, from Pierce's text "Types and Programming 
Languages", Pierce writes: "Static elimination of array-bounds checking 
is a long-standing goal for type system designers.  In principle, the 
necessary mechanisms (based on dependent types) are well understood, but 
packaging them in a form that balances expressive power, predictability 
and tractability of typechecking, and complexity of program annotations 
remains a significant challenge."  Again, this could quite validly be 
described as a type error, just like division by zero or ANY other 
program error... it's just that the type system that solves it doesn't 
look appealing, so everyone punts the job to runtime checks (or, in some 
cases, to the CPU's memory protection features and/or the user's ability 
to fix resulting data corruption).

Why aren't these things commonly considered type errors?  There is only 
one reason: there exists no widely used language which solves them with 
types.  (I mean in the programming language type theory sense of "type"; 
since many languages "tag" arrays with annotations indicating their 
dimensions, I guess you could say that we do solve them with types in 
the LISP sense).

> Your problem doesn't exist. Just say "types" when you're amongst your 
> own folks, and "static types" when you're amongst a broader audience, 
> and everything's fine.

I think I've explained why that's not the case.  I don't have a 
complaint about anyone speaking of types.  It's the confusion from 
pretending that the two definitions are comparable that I'm pointing 
out.

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