What is Expressiveness in a Computer Language

[Joe Marshall]

Marshall wrote:
>
> 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.

It would depend on the type system, naturally.

It isn't clear to me which programs we would have to give up, either.
I don't have much experience in sophisticated typed languages.  It is
rather easy to find programs that baffle an unsophisticated typed
language (C, C++, Java, etc.).

Looking back in comp.lang.lisp, I see these examples:

(defun noisy-apply (f arglist)
  (format t "I am now about to apply ~s to ~s" f arglist)
  (apply f arglist))

(defun blackhole (argument)
  (declare (ignore argument))
  #'blackhole)

But wait a sec.  It seems that these were examples I invented in
response to the same question from you!


>
> 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?

Certainly!  As soon as you can reflect on the type system you can
construct programs that type-check iff they fail to type-check.

> > 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.

I think templates only have to expand to seven levels, so you are
severely limited here.

> > 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.)

I agree.  The point of static checking is to *not* run the program.  If
the type system gets too complicated, it may be a de-facto interpreter.