What is Expressiveness in a Computer Language

[David Hopwood]

Pascal Costanza wrote:
> David Hopwood wrote:
>> Pascal Costanza wrote:
>>> David Hopwood wrote:
>>>> Marshall wrote:
>>>>
>>>>> 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?
>>>>
>>>> In a statically typed language that has a "dynamic" type, all
>>>> dynamically typed programs are straightforwardly expressible.
>>>
>>> What about programs where the types change at runtime?
>>
>> Staged compilation is perfectly compatible with static typing.
>> Static typing only requires that it be possible to prove absence
>> of some category of type errors when the types are known; it
>> does not require that all types are known before the first-stage
>> program is run.
> 
> Can you change the types of the program that is already running, or are
> the levels strictly separated?

In most staged compilation systems this is intentionally not permitted.
But this is not a type system issue. You can't change the types in a
running program because you can't change the program, period. And you
can't do that because most designers of these systems consider directly
self-modifying code to be a bad idea (I agree with them).

Note that prohibiting directly self-modifying code does not prevent a
program from specifying another program to *replace* it.

>> There are, however, staged compilation systems that guarantee that
>> the generated program will be typeable if the first-stage program
>> is.
> 
> ...and I guess that this reduces again the kinds of things you can express.

Yes. If you don't want that, use a system that does not impose this
restriction/guarantee.

>> (It's clear that to compare the expressiveness of statically and
>> dynamically typed languages, the languages must be comparable in
>> other respects than their type system. Staged compilation is the
>> equivalent feature to 'eval'.)
> 
> If it is equivalent to eval (i.e., executed at runtime), and the static
> type checker that is part of eval yields a type error, then you still
> get a type error at runtime!

You can choose to use a system in which this is impossible because only
typeable programs can be generated, or one in which non-typeable programs
can be generated. In the latter case, type errors are detected at the
earliest possible opportunity, as soon as the program code is known and
before any of that code has been executed. (In the case of eval, OTOH,
the erroneous code may cause visible side effects before any run-time
error occurs.)

I don't know what else you could ask for.

-- 
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>