What is Expressiveness in a Computer Language

[Marshall]

Chris F Clark wrote:
>
> And to me the question is what kinds of types apply to these dynamic
> programs, where in fact you may have to solve the halting problem to
> know exactly when some statement is executed.  I expect that some
> programs have type signatures that exceed the expressibility of any
> static system (that is Turing complete).  Therefore, we need something
> that "computes" the appropriate type at run-time, because we need full
> Turing power to compute it.  To me such a system is a "dynamic type
> system".  I think dynamic tags are a good approximation, because they
> only compute what type the expression has this time.

Yes, an important question (IMHO the *more* important question
than the terminology) is what *programs* do we give up if we
wish to use static typing? I have never been able to pin this
one down at all.

Frankly, if the *only* issue between static and dynamic was
the static checking of the types, then static typing woud
unquestionably be superior. But that's not the only issue.
There are also what I call "packaging" issues, such as
being able to run partly-wrong programs on purpose so
that one would have the opportunity to do runtime analysis
without having to, say, implement parts of some interface
that one isn't interested in testing yet. These could also
be solved in a statically typed language. (Although
historically it hasn't been done that way.)

The real question is, are there some programs that we
can't write *at all* in a statically typed language, because
they'll *never* be typable? I think there might be, but I've
never been able to find a solid example of one.


> Perhaps, there is no such beast.  Or, perhaps I just can't formulate
> it.  Or, perhaps we have static type checkers which can do
> computations of unbounded complexity.  However, I thought that one of
> the characteristics of type systems was that they did not allow
> unbounded complexity and weren't Turing Complete.

The C++ type system is Turing complete, although in practical terms
it limits how much processing power it will spend on types at
compile time.


> If you allow Turing Complete type systems, then I would say no--every
> bug can be reforumlated as a type error.  If you require your type
> system to be less powerful, then some bugs must escape it.

I don't think so. Even with a Turing complete type system, a program's
runtime behavior is still something different from its static behavior.
(This is the other side of the "types are not tags" issue--not only
is it the case that there are things static types can do that tags
can't, it is also the case that there are things tags can do that
static types can't.)


Marshall