«

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?

> 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.

> (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!


Pascal

--
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006
http://lisp-ecoop06.bknr.net/

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 Hopwood wrote:
>
> (In the case of eval, OTOH,
> the erroneous code may cause visible side effects before any run-time
> error occurs.)

Not necessarily. You can replace the primitive eval by compile, which
delivers a function encapsulating the program, so you can check the type
of the function before actually running it. Eval itself can easily be
expressed on top of this as a polymorphic function, which does not run
the program if it does not have the desired type:

eval ['a] s = typecase compile s of
f : (()->'a) -> f ()
_ -> raise TypeError

- Andreas

David Hopwood wrote:
> 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).

Whether you consider something you cannot do with statically typed
languages a bad idea or not is irrelevant. You were asking for things
that you cannot do with statically typed languages.

There are at least systems that a lot of people rely on (the JVM, .NET)
that achieve runtime efficiency primarily by executing what is
essentially self-modifying code. These runtime optimization systems have
been researched primarily for the language Self, and also implemented in
Strongtalk, CLOS, etc., to various degrees.

Beyond that, I am convinced that the ability to update a running system
without the need to shut it down can be an important asset.

> 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.


Pascal

--
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006
http://lisp-ecoop06.bknr.net/

Pascal Costanza <> writes:

> Whether you consider something you cannot do with statically typed
> languages a bad idea or not is irrelevant. You were asking for things
> that you cannot do with statically typed languages.

The whole point of static type systems is to make sure that there are
things that one cannot do. So the fact that there are such things are
not an argument per se against static types.

[ ... ]

> Beyond that, I am convinced that the ability to update a running
> system without the need to shut it down can be an important asset.

And I am convinced that updating a running system in the style of,
e.g., Erlang, can be statically typed.

>> 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.

Matthias Blume wrote:
> Pascal Costanza <> writes:
>
>> Whether you consider something you cannot do with statically typed
>> languages a bad idea or not is irrelevant. You were asking for things
>> that you cannot do with statically typed languages.
>
> The whole point of static type systems is to make sure that there are
> things that one cannot do. So the fact that there are such things are
> not an argument per se against static types.

I am not arguing against static type systems. I am just responding to
the question what the things are that you cannot do in statically typed
languages.

> [ ... ]
>
>> Beyond that, I am convinced that the ability to update a running
>> system without the need to shut it down can be an important asset.
>
> 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.

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.

>>> 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.


Pascal

[1] BTW, that's also the approach taken in CLOS.

--
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006
http://lisp-ecoop06.bknr.net/

Andreas Rossberg wrote:
> David Hopwood wrote:
>
>> (In the case of eval, OTOH,
>> the erroneous code may cause visible side effects before any run-time
>> error occurs.)
>
> Not necessarily. You can replace the primitive eval by compile, which
> delivers a function encapsulating the program, so you can check the type
> of the function before actually running it. Eval itself can easily be
> expressed on top of this as a polymorphic function, which does not run
> the program if it does not have the desired type:
>
> eval ['a] s = typecase compile s of
> f : (()->'a) -> f ()
> _ -> raise TypeError

What I meant was, in the case of eval in an untyped ("dynamically typed")
language.

The approach you've just outlined is an implementation of staged compilation
in a typed language.

--
David Hopwood <>

Matthias Blume wrote:
>
> 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.

Pardon my ignorance, but what is the Erlang solution to this problem?


Marshall

Pascal Costanza <> 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.

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.