What is Expressiveness in a Computer Language

[Joachim Durchholz]

Pascal Costanza schrieb:
> Static type systems potentially change the semantics of a 
> language in ways that cannot be captured by dynamically typed languages 
> anymore, and vice versa.

Very true.

I also suspect that's also why adding type inference to a 
dynamically-typed language doesn't give you all the benefits of static 
typing: the added-on type system is (usually) too weak to express really 
interesting guarantees, usually because the language's semantics isn't 
tailored towards making the inference steps easy enough.

Conversely, I suspect that adding dynamic typing to statically-typed 
languages tends to miss the most interesting applications, mostly 
because all the features that can "simply be done" in a 
dynamically-typed language have to be retrofitted to the 
statically-typed language on a case-by-case basis.

In both cases, the language designers often don't know the facilities of 
the opposed camp well enough to really assess the trade-offs they are doing.

> There is, of course, room for research on performing static type checks 
> in a running system, for example immediately after or before a software 
> update is applied, or maybe even on separate type checking on software 
> increments such that guarantees for their composition can be derived. 
> However, I am not aware of a lot of work in that area, maybe because the 
> static typing community is too focused on compile-time issues.

I think it's mostly because it's intimidating.

The core semantics of an ideal language fits on a single sheet of paper, 
to facilitate proofs of language properties. Type checking 
dynamically-loaded code probably wouldn't fit on that sheet of paper.
(The non-core semantics is then usually a set of transformation rules 
that map the constructs that the programmer sees to constructs of the 
core language.)

Regards,
Jo