What is Expressiveness in a Computer Language

[Matthias Blume]

Pascal Costanza <pc at p-cos.net> writes:

>> And I am convinced that updating a running system in the style of,
>> e.g., Erlang, can be statically typed.
>
> Maybe. The interesting question then is whether you can express the
> kinds of dynamic updates that are relevant in practice. Because a
> static type system always restricts what kinds of runtime behavior you
> can express in your language. I am still skeptical, because changing
> the types at runtime is basically changing the assumptions that the
> static type checker has used to check the program's types in the first
> place.

That's why I find the Erlang model to be more promising.

I am extremely skeptical of code mutation at runtime which would
"change types", because to me types are approximations of program
invariants.  So if you do a modification that changes the types, it is
rather likely that you did something that also changed the invariants,
and existing code relying on those invariants will now break.

> For example, all the approaches that I have seen in statically typed
> languages deal with adding to a running program (say, class fields and
> methods, etc.), but not with changing to, or removing from it.

Of course, there are good reasons for that: removing fields or
changing their invariants requires that all /deployed/ code which
relied on their existence or their invariants must be made aware of
this change.  This is a semantic problem which happens to reveal
itself as a typing problem.  By making types dynamic, the problem does
not go away but is merely swept under the rug.

>>>> Note that prohibiting directly self-modifying code does not prevent a
>>>> program from specifying another program to *replace* it.
>>> ...and this creates problems with moving data from one version of a
>>> program to the next.
>> How does this "create" such a problem?  The problem is there in
>> either
>> approach.  In fact, I believe that the best chance we have of
>> addressing the problem is by adopting the "replace the code" model
>> along with a "translate the data where necessary at the time of
>> replacement".  Translating the data, i.e., re-establishing the
>> invariants expected by the updated/replaced code, seems much harder
>> (to me) in the case of self-modifying code.  Erlang got this one
>> right.
>
> ...and the "translate the date where necessary" approach is
> essentially triggered by a dynamic type test (if value x is of an old
> version of type T, update it to reflect the new version of type T
> [1]). QED.

But this test would have to already exist in code that was deployed
/before/ the change!  How did this code know what to test for, and how
did it know how to translate the data?  Plus, how do you detect that
some piece of data is "of an old version of type T"?  If v has type T
and T "changes" (whatever that might mean), how can you tell that v's
type is "the old T" rather than "the new T"!  Are there two different
Ts around now?  If so, how can you say that T has changed?

The bottom line is that even the concept of "changing types at
runtime" makes little sense.  Until someone shows me a /careful/
formalization that actually works, I just can't take it very
seriously.