What is Expressiveness in a Computer Language

[Chris F Clark]

Chris F Clark wrote:
> A static
> type system eliminates some set of tags on values by syntactic
> analysis of annotations (types) written with or as part of the program
> and detects some of the disallowed compuatations (staticly) at compile
> time.

Adreas relied:
> Explicit annotations are not a necessary ingredient of a type system,
> nor is "eliminating tags" very relevant to its function.

While this is true, I disagree at some level with the second part.  By
eliminating tags, I mean allowing one to perform "type safe"
computations without requiring the values to be tagged.  One could
argue that the tags were never there.  However, many of the
interesting polymorphic computations reaquire either that the values
be tagged or that some other process assures that at each point one
can determine apriori what the correct variant of computation is which
applies.

To me a static type system is one which does this apriori
determination.  A dynamic type system does not do a apriori and
instead includes explicit information in the values being computed to
select the corret variant computations.

In that sense, a static type system is eliminating tags, because the
information is pre-computed and not explicitly stored as a part of the
computation.  Now, you may not view the tag as being there, but in my
mind if there exists a way of perfoming the computation that requires
tags, the tag was there and that tag has been eliminated.

To put it another way, I consider the tags to be axiomatic.  Most
computations involve some decision logic that is driven by distinct
values that have previously been computed.  The separation of the
values which drive the compuation one-way versus another is a tag.
That tag can potentially be eliminated by some apriori computation.

In what I do, it is very valuable to move information from being
explicitly represented in the computed result into the tag, so that I
often have distinct "types" (i.e. tags) for an empty list, a list with
one element, a list with two elements, and a longer list.  In that
sense, I agree with Chris Smith's assertion that "static typing" is
about asserting general properties of the algorithm/data.  These
assertions are important to the way I am manipulating the data.  They
are part of my type model, but they may not be part of anyone else's,
and to me toe pass a empty list to a function requiring a list with
two elements is a "type error", because it is something I expect the
type system to detect as incorrect.  The fact that no one else may
have that expectation does not seem relevant to me.

Now, to carry this farther, since I expect the type system to validate
that certain values are of certain types and only be used in certain
contexts, I am happy when it does not require certain "tags" to be
actualy present in the data.  However, because other bits of code are
polymorphic, I do expect certain values to require tags.  In the end,
this is still a win for me.  I had certain data elements that in the
abstract had to be represented explicitly.  I have encoded that
information into the type system and in some cases the type system is
not using any bits in the computed representation to hold that
information.  Whenever that happens, I win and that solves one of the
problems that I need solved.

Thus, a type system is a way for me to express certain axioms about my
algorithm.  A dynamic type system encodes those facts as part of the
computation.  A static type system pre-calculates certain "theorems"
from my axioms and uses those theorems to allow my algorithm to be
computed without all the facts being stored as part of the computation.

Hopefully, this makes my point of view clear.

-Chris

*****************************************************************************
Chris Clark                    Internet   :  compres at world.std.com
Compiler Resources, Inc.       Web Site   :  http://world.std.com/~compres  
23 Bailey Rd                   voice      :  (508) 435-5016
Berlin, MA  01503  USA         fax        :  (978) 838-0263  (24 hours)
------------------------------------------------------------------------------