What is Expressiveness in a Computer Language

[Joe Marshall]

David Hopwood wrote:
> Joe Marshall wrote:
> >
> > The point is that there exists (by construction) programs that can
> > never be statically checked.
>
> I don't think you've shown that. I would like to see a more explicit
> construction of a dynamically typed [*] program with a given specification,
> where it is not possible to write a statically typed program that meets
> the same specification using the same algorithms.

I think we're at cross-purposes here.  It is trivial to create a static
type system that has a `universal type' and defers all the required
type narrowing to runtime.  In effect, we've `turned off' the static
typing (because everything trivially type checks at compile time).

However, a sufficiently powerful type system must be incomplete or
inconsistent (by Godel).  A type system proves theorems about a
program.  If the type system is rich enough, then there are unprovable,
yet true theorems.  That is, programs that are type-safe but do not
type check.  A type system that could reflect on itself is easily
powerful enough to qualify.

> AFAIK, it is *always* possible to construct such a statically typed
> program in a type system that supports typerec or gradual typing. The
> informal construction you give above doesn't contradict that, because
> it depends on reflecting on a [static] type system, and in a dynamically
> typed program there is no type system to reflect on.

A static type system is usually used for universal proofs:  For all
runtime values of such and such...   Dynamic checks usually provide
existential refutations:  This particular value isn't a string.  It may
be the case that there is no universal proof, yet no existential
refutation.

>
> Note that I'm not claiming that you can check any desirable property of
> a program (that would contradict Rice's Theorem), only that you can
> express any dynamically typed program in a statically typed language --
> with static checks where possible and dynamic checks where necessary.

Sure.  And I'm not saying that you cannot express these programs in a
static language, but rather that there exist programs that have
desirable properties (that run without error and produce the right
answer) but that the desirable properties cannot be statically checked.

The real question is how common these programs are, and what sort of
desirable properties are we trying to check.