[Prev][Next][Index][Thread]

Re: type safety

Dear Type Gurus,

This has been an interesting discussion.  I would like to add a bit to
it, partly in the hopes that my comments will help others and partly
because it will help me to write down some of the ideas that have been
floating around in my head for the last few years.

I will begin with some definitions.  I am quite certain that these
definitions are incomplete, i.e., there are some valid uses of the
defined phrases which are not covered.  I feel reasonably confident
that the definitions are sound, i.e., we can use the defined phrases
this way without being horribly wrong.  Here they are:

  safety:  at a minimum, well definedness of the behavior of program
    execution.

  types:  syntactic expressions which are associated with program
    fragments according to a set of typing rules and which (if the
    rules are sound) represent propositions satisfied by the program
    fragments.

  type soundness:  for a set of typing rules, the validity of
    propositions represented by typing judgements derivable using the
    rules.

  well typedness:  for a program fragment and a type system, the
    existence of a typing judgement with that program fragment as its
    subject which can be derived following the typing rules of that
    type system.

  type safety:  safety (for one program or for an entire programming
    language) enforced by requiring well typedness in some type
    system.

  static typing:  for a programming language, the requirement of well
    typedness in some non-trivial type system.

    (E.g., Ada, C, C++, Java, Haskell, ML, and Pascal have static
    typing.)
    
  strong typing:  for a programming language, the requirement of well
    typedness in some type system which provides type safety for all
    programs.

    (E.g., Ada, Java, Haskell, and ML have strong typing, but C, C++,
    and Pascal do not.)

  dynamic typing:  for a programming language, the lack of static
    typing together with obtaining (some amount of) safety by making
    the behavior of operations on arguments of the wrong "type" well
    defined.

    (E.g., LISP, Perl, and Scheme have dynamic typing.)

  soft typing:  for a programming language, the use a type system
    which is not specified as part of the language definition.

As I mentioned, these definitions are incomplete, but I think they are
adequate for this discussion.  I am interested in comments and
improvements for the definitions.  I have a few of my own comments on
these definitions:

  * For the word "types" I know that this community can quickly supply
    a dozen alternate definitions, but in the context of this
    discussion most can be shown to be equivalent or at least close to
    the definition above.
    
  * Some people might define safety to also require the absence of
    uncatchable exceptions.  However, as long as these uncatchable
    exceptions generate well defined behavior (e.g., halting), I think
    it is better to consider them safe.
    
  * I disagree with the idea that safety is a language-relative
    notion.  In particular, I an strongly opposed to any definition of
    safety by which the language C can be considered safe.
    
  * It seems there are good reasons for completely avoiding the phrase
    "dynamic typing", but when it is used the meaning generally seems
    to be as I have described it above.

Having given some definitions, I now have some comments on the
discussion.

1. Safety does have _something_ to do with types, in the following
   sense:  If a programming language has unsafe programs, then it is
   always possible to define type systems which will exclude all of
   the unsafe programs.  Types can indeed prove that all safety
   restrictions will be respected.  Unfortunately, there are serious
   potential drawbacks:

   feasibility --- Such type systems may be unfeasible to use with
     current technology, in several different ways:
   
       A. The space/time complexity of algorithms implementing the
          type system may be unacceptable.

       B. The type system may be too complicated for the implementors
          to comprehend, preventing implementation.
       
       C. Although some of the type information for each program may
          be inferable automatically, the amount left to be supplied
          by the programmer may be too voluminous or too complicated.

   expressiveness --- It is very difficult to design feasible type
     systems without excluding too many safe programs.  The type
     system may effectively force programmers to duplicate lots of
     code and insert lots of redundant checks.  This tends to obscure
     program structure and make maintenance difficult.

   About half of my research and much of research of the members of
   this mailing list is related to exploring how to overcome these
   drawbacks.

   Most of the discussion on this point is orthogonal to whether the
   type system in question is part of the language definition (static
   typing vs. soft typing).

2. I think it is probably an error to categorize assembly languages as
   (un)typed or (un)safe.

   First, whether an assembly language is safe can depend heavily on
   whether the target CPU is safe.  Although many modern CPUs are
   somewhat lacking in safety, for some CPUs the corresponding
   assembly language is safe because all program executions have well
   defined behavior.  (Hardware bugs in this case can prevent a
   program's behavior from following its definition, but they do not
   make the correct behavior undefined.)

   Second, there are assembly languages which have strong type systems
   as part of their definition.  (The type systems of these languages
   tend to look quite different from the ones for high level
   languages.)

3. I disagree strongly with the thesis that:

     Type structure is a syntactic discipline for enforcing
     levels of abstraction.

   I believe certain kinds of types can be very useful for enforcing
   abstraction.  However, by including this use of types in the
   definition of types, I believe the above thesis confuses WHAT types
   are with HOW they can be used.

   (The above thesis has been quoted from a paper by Reynolds which I
   haven't read.  It is possible that in the context of that paper I
   would agree with it, but I haven't seen the context.)

-- 
Joe Wells
http://www.cee.hw.ac.uk/~jbw/