What is Expressiveness in a Computer Language
Chris Smith
cdsmith at twu.net
Mon Jun 19 13:57:08 EDT 2006
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
More information about the Python-list
mailing list