[Prev][Next][Index][Thread]
PS on Negative results about the power of static typing
In my message yesterday, I wrote
Suppose we formalize a programming language as an (effectively
presented) triple
(P, ->, A)
where
P is the set of programs
-> is the finitely branching transition relation
A is the set of answers
We assume that the elements of A are irreducible, but there may be
other elements of P that are irreducible - and we consider these to be
bad.
Let's assume that our language is interesting, so that it won't be
decidable whether every execution sequence of a program terminates
with an answer.
On the other hand, we can easily augment our programming language with
a type system so that every program with a type will have this
property.
What I meant to say in the last paragraph was
On the other hand, we can easily augment our programming language
with a type system so that a program will be typable IFF it has this
property.
(Thanks to Matthias in a private message for pointing out the omission.)
Here was the notion of typing I proposed:
As types we choose all the execution trees of (P, ->) that are finite
and whose leaves are all in A. The set of all types will then be
recursive. Say that a program p has type t iff the root of t is p.
The set of all pairs (p, t) such that p has type t will be recursive,
even though it won't be decidable whether a program has a type.
Then every execution sequence of a program that has a type terminates
with an answer, AND if every execution sequence of a program
terminates with an answer, the program will have a type.
The point of the message was not to argue that this was a useful
approach, but just to suggest that if one wants to prove negative
results about the power of static typing, one needs to consider
languages that take in inputs or otherwise interact with their
environment.
Allen