RE: dynamic vs. static typing

["Anton van Straaten" <address@hidden>]

Steve Dekorte wrote:
> On Nov 24, 2003, at 11:57 AM, Anton van Straaten wrote:
> > Abstract interpretation is, essentially, running a program
> > before runtime - i.e. before a full set of inputs exist.
> > Compilers effectively do this when they analyze a program's
> > types.  In a program containing type annotations, those
> > annotations essentially form part of an independent program
> > that can be run before the program in which they are embedded
> > is run.  The notes that Shriram previously referenced are a
> > nice and accessible intro for this concept[1].
>
> So when we want to do something like have a development system
> where everything is live (like older LISPs, Smalltalk, Self, etc),
> and we can change anything at runtime (rearrange inheritance
> hierarchies, add and remove methods, variables, etc), of what
> use are the checks that were done at compile time and are no
> longer valid?

The checks would have been of use while the scenario they applied to was in
effect.  If they change, so what?  New checks can assure things that
wouldn't otherwise be assured.

I think you may have missed the point of my post (my own fault, it was
long).  I'm saying, don't think in terms of "the checks that were done at
compile time".  Instead, think in terms of computations on different
parts/aspects of the program, that can occur at different times, and can be
shifted in time.

The example of a live development system is a perfect one: when you change
some code, that change needs to be integrated into the running system, which
can involve a range of computations from all three of the categories we
often call "compile time", "link time", and "run time".

Those computations might all happen at "run time" from the point of view of
the development system, but you might still want to be able to deploy that
code in an environment that doesn't involve the development system.  In the
latter environment, some of what is done at runtime w.r.t. the development
system can occur earlier for the production system, with corresponding
benefits for verifiability, performance, etc.

In the distributed systems business, they talk about dynamically
"partitioning" the distribution of an application, e.g. deciding late in the
cycle which parts of an application will run on a server or on a client
machine.  I don't see anything theoretically to prevent something similar
being done with type-checking.

I'm saying that type-checking is a computation that can span the entire
execution lifecycle of a program, and if we recognize and understand that,
we can develop systems that can make better use of type information at all
stages of that lifecycle, and do so flexibly, without having to be shackled
by it.

Anton