What is Expressiveness in a Computer Language

[Chris F Clark]

I wrote:
> The important thing is the dynamicism of lisp allowed one to write
> polymorphic programs, before most of us knew the term.

Chris Smith <cdsmith at twu.net> writes:

> Sure.  In exchange for giving up the proofs of the type checker, you 
> could write all kinds of programs.  To this day, we continue to write 
> programs in languages with dynamic checking features because we don't 
> have powerful enough type systems to express the corresponding type 
> system.

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.

> I believe that, in fact, it would be trivial to imagine a type system 
> which is capable of expressing that type.  Okay, not trivial, since it 
> appears to be necessary to conceive of an infinite family of integer 
> types with only one value each, along with range types, and 
> relationships between them; but it's probably not completely beyond the 
> ability of a very bright 12-year-old who has someone to describe the 
> problem thoroughly and help her with the notation.

Well, it look like you are right in that I see following is a Haskell
program that looks essentially correct.  I wanted something that was
simple enough that one could see that it could be computed, but which
was complex enough that it had to be computed (and couldn't be
statically expressed with a system that did no "type computations").
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.

> You would, of course, need a suitable type system first.  For example, 
> it appears to me that there is simply no possible way of expressing what 
> you've described in Java, even with the new generics features.  Perhaps 
> it's possible in ML or Haskell (I don't know).  My point is that if you 
> were allowed to design a type system to meet your needs, I bet you could 
> do it.

Or, I could do as I think the dynamic programmers do, dispense with
trying to formulate a sufficiently general type system and just check
the tags at the appropriate points.

> Sure.  The important question, then, is whether there exists any program 
> bug that can't be formulated as a type error.

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.

-Chris