What is Expressiveness in a Computer Language

[Chris F Clark]

I wrote:
> These informal systems, which may not prove what they claim to prove
> are my concept of a "type system".

Chris Smith <cdsmith at twu.net> replied:
> Okay, that works.  I'm not sure where it gets us, though....

Ok, we'll get there.  First, we need to step back in time, to when there
was roughly algol, cobol, fortran, and lisp.  Back then, at least as I
understood things, there were only a few types that generally people
understood integer, real, and (perhaps) pointer.  Now, with algol or
fortran things were generally only of the first two types and
variables were statically declared to be one or the other.  With lisp
any cell could hold any one of the 3, and some clever implementor
added "tag bits" to distinguish which the cell held.  As I understood
it, the tag bits weren't originally for type correctness, so much as
they facilitated garbage collection.  The garbage collector didn't
know what type of data you put in a cell and had to determine which
cells contained pointers, so that the mark-and-sweep algorithms could
sweep by following the pointers (and not following the integers that
looked like pointers).  Still, these tag bits did preserve the
"dynamic" type, in the sense that we knew types from the other
languages.  As I remember it, sophistication with type really didn't
occur as a phenomena for the general programmer until the introduction
of Pascal (and to a lesser extent PL/I).  Moreover, as I recall it,
perhaps because I didn't learn the appropriate dialect was that lisp
dialects kept with the more general notion of type (lists and tuples)
and eschewed low-level bit-fiddling where we might want to talk about
a 4 bit integer representing 0 .. 15 or -8 .. 7.

The important thing is the dynamicism of lisp allowed one to write
polymorphic programs, before most of us knew the term.  However, we
still had a notion of type: integers and floating point numbers were
still different and one could not portably use integer operations on
floating pointer values or vice versa.  However, one could check the
tag and "do the right thing" and many lisp primitives did just that,
making them polymorphic.

The way most of us conceived (or were taught to conceive) of the
situation was that there still were types, they were just associated
with values and the type laws we all knew and loved still worked, they
just worked dynamically upon the types of the operand values that were
presented at the time.

Can this be made rigorous?  Perhaps.

Instead of viewing the text of the program staticly, let us view it
dynamicly, that is by introducing a time (or execution) dimension.
This is easier if you take an imperative view of the dynamic program
and imagine things having an operational semantics, which is why we
stepped back in time in the first place, so that we are in a world
where imperative programming is the default model for most
programmers.  

Thus, as we traverse a list, the first element might be an integer,
the second a floating point value, the third a sub-list, the fourth
and fifth, two more integers, and so on.  If you look statically at
the head of the list, we have a very wide union of types going by.
However, perhaps there is a mapping going on that can be discerned.
For example, perhaps the list has 3 distinct types of elements
(integers, floating points, and sub-lists) and it circles through the
types in the order, first having one of each type, then two of each
type, then four of each type, then eight, and so on.  The world is now
patterned.  

However, I don't know how to write a static type annotation that
describes exactly that type.  That may just be my lack of experience
in writing annotations.  However, it's well within my grasp to imagine
the appropriate type structure, even though **I** can't describe it
formally.  More importantly, I can easily write something which checks
the tags and sees whether the data corresponds to my model.

And, this brings us to the point, if the data that my program
encounters doesn't match the model I have formulated, then something
is of the wrong "type".  Equally importantly, the dynamic tags, have
helped me discover that type error.

Now, the example may have seemed arbitrary to you, and it was in some
sense arbitrary.  However, if one imagines a complete binary tree with
three kinds elements stored in memory as rows per depth, one can get
exactly the structure I described.  And, if one were rewriting that
unusual representation to a more normal one, one might want exactly
the "type check" I proposed to validate that the input binary tree was
actually well formed.

Does this help explain dynamic typing as a form of typing?

-Chris