[Prev][Next][Index][Thread]
Re: type safety
Phil, if you're merely looking for a historical account, you may ignore my
message. My comments are aimed at clarifying the confusion concerning the
connection between safety and types.
1. I believe that it is useless to distinguish "dynamic" and "static"
type safety. There is only one concept and it has nothing to do with the
type concept as staked out by the PL community over the past 10 or 20
years.
2. Saftey is a completely dynamic discipline. You look at the universe of
values in your language and the computational operations on them. Then
you partition the set of values for each operation into "good" and "bad"
values. If all operations can deal with all values, it makes no sense to
speak of safety. You have an "assembly language."
In LC (intrepreted as a programming language), the set of values is the
set of lambda's. The only operation is application. If programs are
closed terms, nothing can go wrong. (That's CBN or CBV, LandinPlotkin
style)
In LC + numbers, the set of values is the set of lambdas plus
constants. Now a constant (say 5) could show up in a function position,
and hell breaks loose. If your implementation catches all such
constants, it's safe. If it randomly says (5 V) = U for some random U,
it's a fancy version of C.
3. Types (and type checking) are a completely syntactic discipline.
They help us prove that certain things are true about a program without
running it. In particular, some type systems help us prove that a
program won't viololate certain safety restrictions that they
implementation imposes on computational operations.
Throw your standard simple type system at LC + numbers. You can prove a
type soundness theorem, which states that no basic constant will flow
into a function position. [This helps implementors who may now eliminate
the checks that catch constants in application positions and who can
thus speed up the execution by about 22%. Of course, it is to the
disadvantage of your programmer who can now write far fewer programs
than in LC + numbers alone.]
4. Types can never prove that all safety restrictions will be respected.
That shouldn't be surprising but it is too many people because of
Milner's misleading first paper on type soundness and the subsequent
work by others on similar languages.
Take LC + numbers plus division. We now have two computational
operations:
* application, which may only consume closures in the function position [A]
* division, which may only consume numbers in both positions [B]
and which may not consume a 0 in the second position [C]
Your standard simple type system can eliminate the restrictions labeled
A and B, but not C. So, a program in this language may still signal an
error: attempt to divide by 0. Call this an exception or whatever you
will, it is a behavior that you don't want.
I wrote that papers have been misleading because they tend to shy away
from partial operations like division or array dereference. In this
setting, a reasonably type system can prove that all restrictions are
enforcable with a type discipline. Unfortunately, this tends to give the
impression that types are almighty.
5. For years I have taught the following chart in my juniorlevel
programmig languages course:
SAFETY
YES NO
*
YES  ML (good) C/C++ (insidious
 because it pretends
 to help programmers
TYPED  and doesn't)


NO  Scheme (okay, Assembly (necessary)
 but needs a soft
typer)
I felt pretty much alone because the standard papers don't say it this
way. Esp Milner and Cardelli& Wegner let me down on this one. BUT to
Luca's credit: his paper on the handbook remedies this and contains a
similar chart. So I do know that there is at least one person in the
type community who understands that
safety and types are independent concepts.
Happy new year  Matthias
P.S. And no, saying Scheme is UNItyped doesn't change a thing. And no, the
above view on safety has nothing to do with modules. Both views
scale. Though I do admit that in a typed module world, safety is much
cheaper than in a Schemeish world (the 22% comes from a study that didn't
use modular languages.)