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

["Peter van Rooijen" <address@hidden>]

From: "Joe Marshall" <jrm@ccs.neu.edu>
> John Clements <clements@brinckerhoff.org> writes:
>
> > Typically, type systems help you to construct a proof that certain
> > errors cannot arise during evaluation.  When parts of that proof are
> > used to alter the evaluation itself, you suddenly have a class of
> > _runtime_ errors (or rather, "mis-behaviors") that can only be
> > understood by examining the type proof.
>
> I think that John has identified what it is that made me uncomfortable
> with this style.  I generally think of the type system as meta
> information.

Based on this I started to wonder, "what exactly is the goal of a type
system?" and quickly googled for "goal of a type system" and found an
interesting variety of insights, and on "goals of a type system" and found
what I quote below in :

On Type Systems for Object-Oriented Database
Programming Languages
YURI LEONTIEV
Intuit Canada Limited
M. TAMER ¨ OZSU
University of Waterloo
AND
DUANE SZAFRON
University of Alberta

(see 2.2 quoted below).

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. I mostly
work in the (dynamically typed) Smalltalk language and I always wonder "how
would a type system that uses type annotations help me?".

It seems to me that in order to be able to answer this question I would be
helped by the answer to the question "what does (the designer/implementer
of) a type system intend to give me?", which I translated into the above
google queries.

Do people agree with the quoted article? I am very interested in any
(additional) insights about why we might want a type system, especially one
that uses type annotations.

I'd also be very interested to see other people's lists of what they feel
the goals of a type system are, preferably an exhaustive list (i.e.,
something better than "the major goals [...] include" as in the quoted
article), and preferably in order of importance ;-).

Hope this makes sense to someone.

Regards,

Peter van Rooijen

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.

(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 objectoriented design technologies.
This property is often considered to be
the major goal of a type system in the
database community.

(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.

(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.

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]. 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.

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.

A type system should also be enforceable
in order to prevent an execution of typeincorrect
programs. This implies that programs
have to be written with as much
type information as possible to prevent
"false alarms."

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.
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.