Re: the forward method [dynamic vs. static typing]

[Joe Marshall <address@hidden>]

"Peter van Rooijen" <ll1@vanrooijen.com> writes:

> I would like to know how well this resonates with the goals that people here
> are thinking of for type systems on this list/in this discussion. 

My goal is to write programs that do interesting things for fun and
profit.  Tools that make this easier, more interesting, or more
entertaining are welcome additions to my toolbox.

> 2.2. Essential Features of a Type System
>
> The major goals of a type system in today's
> programming languages and database
> systems include [Cardelli 1989, 1997,
> Black and Palsberg 1994]:
>
> (1) Provide a programmer with an efficient way of catching
>     programming errors before a program (or a part of it) is
>     actually executed.  This is often considered to be the major
>     objective of a type system in the programming language
>     community. 

The sooner one catches a programming error, the easier it is to deal
with, so this seems to be a reasonable goal.

> (2) Serve as a data structuring tool for design and modeling
>     purposes.  Many design technologies that have emerged through
>     the past decade rely partially or fully on type systems to
>     provide a convenient design and documentation framework for a
>     system development process.  This is especially true of
>     object-oriented design technologies.  This property is often
>     considered to be the major goal of a type system in the database
>     community. 

This, however, is a problem.  The data structure should reflect what
is being modeled, not what is easily expressible by the type system.
It seems to me that the design technologies, especial
`object-oriented' design technologies, are *driven* by the type
system. 

> (3) Provide a convenient framework for program maintenance.  This
>     includes documentation at the production stage of program
>     evolution as well as the ability of a programmer to understand
>     the functionality and interfaces of a completed product.

This addresses the expressibility of the type system.  It is
convenient to know that function foo takes an integer, but it is more
convenient to know that function foo takes an integer that represents
the vertical displacement of a glyph as measured in pixels and is only
meaningful if it is less than the interline spacing.  The former is
usually easy to express in a type system, but the latter is much
harder.

In any case, a type system is just one of many tools that can aid (or
hinder) this goal.

> (4) Provide sufficient information for optimization purposes.  The
>     information provided by the type system can be used by an
>     optimizing compiler, interpreter, or a query optimizer (in
>     persistent systems) to improve the efficiency of a program.

I consider the `type system as programming tool' to be a very
different animal from the `type system as compiler hints'.  The Common
Lisp type system, for example, allows one to sprinkle type decorations
through the code for the purposes of instructing the compiler.  These
declarations are *not* designed to help debug the program or guarantee
anything, they are hints to the compiler about what the programmer
knows that the compiler doesn't.

> In order for a compiler (or interpreter) to be able to typecheck a
> program (or a part of it), there must exist a typechecking
> algorithm.  Existence of such an algorithm for a given type system
> is termed as verifiability of the type system [Cardelli 1997].
> Thus, a type system should be verifiable.  It is preferable that a
> type system should be decidably verifiable; however, one may have to
> put up with an undecidable type system just as one puts up with
> undecidable programs if enough expressive power is desired [Black
> and Palsberg 1994].

These are definitions.

> The verifiability property also implies that a type system should be
> provably sound, i.e. there should exist a formal proof that a
> successfully typechecked program does not generate any type errors
> at runtime.

This, however, does not follow (unless you start fooling around with
definitions).  Let us rather say that one result of type checking a
program is called `success', and that there should exist a formal
proof that if the type checking algorithm produces `success' then
certain runtime invariants hold.  It is ridiculous to assert that a
program that discriminates among an exhaustive partition (and is thus
`type safe' for any argument) but invokes the runtime error handler on
all but the integer case does not generate a runtime type error.

It should be obvious that if the type checker says `success' then it
ought not be wrong about what it claims.  But the cases where the type
checker does not say `success' fall into two classes: 

   a)  ones where the type checker says `always fails'

   b)  ones where the type checker says `i can't tell without running
       the program'

The dual of the soundness property is that if the type checker says
`always fails', then there should exist a formal proof that the
failing program *will* generate a type error at runtime.

The third possible outcome of the type checking algorithm is `can't
decide at compile time'.  Some people (myself included) think that
there are many interesting programs in this group.

> If a compiler finds a type error and reports it to a programmer, the
> latter should have sufficient information to be able to understand
> the reason for the type error in order to correct it.  Thus, the type
> system should be transparent.

Certainly one that is obscure or opaque is a hinderance.

> A type system should also be enforceable in order to prevent an
> execution of type-incorrect programs.  

I'll agree that programs that can be proven to always fail have
limited utility (mostly in exercising error handling and debugging
tools).  Note, however, that this statement is *not* the same as

   ``A type system should only permit programs that type check
     successfully to run.''

> This implies that programs have to be written with as much type
> information as possible to prevent "false alarms."

This does not follow at all.  The implication here is that failure is
the same as lack of success.  While it implies that adding type
information increases the liklihood of success, it fails to recognize
that it also increases the liklihood of failure!  How could this be?
Adding type information reduces the number of programs that fall into
the `i can't tell' category.  If we are optimistic, then perhaps we
assume that all programs that become decidable at compile time move
into the `success' category.  But even the most optimistic person will
realize that people make mistakes.  Every type annotation added to a
program is an opportunity for an error.  Our type system will not
likely interpret these errors as success, but rather will simply
increase the number of programs that provably fail.

> Finally, a type system should be extensible.  This requirement stems
> from the fact that none of the existing type systems were found to
> be satisfactory for all possible applications. Therefore, the chance
> that any new type system will satisfy all application domains is
> remote. If a type system can not be extended, it will sooner or
> later be abandoned for a type system that can adapt to new
> application requirements.  

Agreed.

> Switching from one type system to another is extremely costly both
> in terms of people resources (that have to be reeducated) and in
> terms of data conversion costs.

This is interesting.  I have not seen this problem in runtime
(dynamically) typed systems.