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

Re: type safety

Hi Corky,

  In your recent post you say:

> In general, I fail to see the myriad distinctions that you are making
> between soft typing and static typing.  Soft typing clearly depends a
> well-chosen language for expressing type assertions just like static
> typing.  Moreover, it can and does use exactly the same form of
> analyses.  The only essential difference between our approach and
> yours is that we decouple complex static analyses from the definition
> of what constitutes a well-formed program.

This essential difference, however, has important consequences:

- In the modular construction of software, the programmer can rely on
components conforming to a static type discipline.  There must be an interface
specification, however weak it may be.  In a soft typing discipline, this is
not required.  In my experience programming on large (in the academic sense)
software projects in Lisp and ML with multiple programmers, this small
difference has a huge impact on overall productivity and correctness.  Perhaps
this can be ameliorated by conventions (such as forcing programmers to use
soft types :-) plus good modularity constructs along the lines Matthias was
suggesting.

- A static type discipline comes with a certain programming discipline.  For
example, the fact that union types in ML are tagged at the source level means
that the programmer often has to declare DATATYPEs and use constructors where
you might not use the corresponding constructs in Scheme.  This makes programs
slightly more verbose, but also more explicit.  This has advantages and
disadvantages, but, again from personal experience, I favor enforcing a
discipline: it just makes programs easier to read, understand, and maintain in
the long run.

- It seems to me there is also the danger that a static analysis tool (as
compared to a formally defined type system) may not be completely specified
and evolve over time.  As a result, softly well-typed programs may no longer
be recognized as satisfying specified invariants under revision of the
analysis tool and vice versa.  I could easily see being frustrated by being
unable to predict if the soft typer would be able to establish a stated
invariant or not.  But I haven't seriously used soft type systems, so I am not
sure how much of an issue this is.

> The complex part of the type system can be separated from the language
> definition and encapsulated in a separate tool called a soft type
> checker.  All of the same compiler optimizations that are applicable
> of a rich static type system are applicable in the context of the
> corresponding soft type system.  The compiler simply performs much
> less optimization if the information extracted by soft type analysis
> is not available.

As Greg mentions, with complex type systems such as refinement types,
dependent types, or linear types, it is an art to find the right compromise
between various desiderata pulling in all directions.  In particular, if the
type system is too complicated, the programmer may lose his understanding of
what is well-typed and what is not.

Rather than completely separating the "complex part", we have used the design
principle of "conservative extension" to help control this difficulty.  We try
to design an extension of a type system so that any program which does not use
the new features is well-typed if and only if it is well-typed in the original
language.  In this way, one can use a feature (such as indexed types to
eliminate array bounds checks) locally, without affecting the program as
whole.  As one becomes more confident in a language, one can express more and
more invariants without having to buy into it wholesale from the outset.
Conservativity also means that the type system can be explained incrementally.

At present, I believe the jury is still out to what extent complex, static
type systems can be effective in practice.  Nonetheless, I think there is a
big pragmatic difference between a program analysis tool, even when cast as a
soft type system, and a statically enforced type system which is part of a
language definition.

  - Frank
----------------------------------------------------------------------
Frank Pfenning                          Phone: +1 412 268-6343       
Department of Computer Science            Fax: +1 412 268-5576       
Carnegie Mellon University              Email: fp@cs.cmu.edu         
Pittsburgh, PA 15213-3891, U.S.A.         URL: http://www.cs.cmu.edu/~fp/
----------------------------------------------------------------------