[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, Landin-Plotkin
   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 junior-level
   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 Scheme-ish world (the 22% comes from a study that didn't
use modular languages.)