Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Path: utzoo!utgpu!water!watnot!watmath!clyde!cbatt!ihnp4!ptsfa!lll-lcc!styx!ames!ucbcad!ucbvax!decvax!tektronix!tekcrl!tekchips!willc
From: willc@tekchips.UUCP
Newsgroups: comp.lang.misc
Subject: Re: Static typing with Dynamic binding
Message-ID: <1082@tekchips.TEK.COM>
Date: Thu, 26-Feb-87 15:29:00 EST
Article-I.D.: tekchips.1082
Posted: Thu Feb 26 15:29:00 1987
Date-Received: Sun, 1-Mar-87 12:38:48 EST
References: <364@oracle.tc.fluke.COM> <814@unc.unc.UUCP>
Reply-To: willc@tekchips.UUCP (Will Clinger)
Distribution: comp.lang.misc
Organization: Tektronix, Inc., Beaverton, OR.
Lines: 42

In article <7280@boring.mcvax.cwi.nl> lambert@boring.UUCP (Lambert Meertens) writes:
>This shows, clearer than previous postings, a source of confusion in the
>dynamic/static type checking debate....
>The problem with this is that we happily implement static type checking
>under the assumption that all conditions can return both true and false,
>that generators in for-loops may always generate at least one value, etc.
>This imposes some restriction, but I do not see why this *by itself* is an
>undue restriction.  This can only be judged in the full context of a
>language.

This is true, but the happy experience comes from statically scoped
languages.  My point is that the restrictions required for static type
checking in a statically scoped language are vastly more reasonable than
the restrictions required for a dynamically scoped language.  My reasoning
is that dynamic scoping prevents the compiler from being able to tell
which bindings of X may be in effect when FOO is called.  The compiler must
therefore assume in the most general case that any binding of X that appears
in the program may be in effect when FOO is called.  This would mean that
all variables named X must have the same type.

Meertens observed that the compiler doesn't have to assume the most general
case but can instead unroll the procedure calling graph to form a tree, and
check types as in a statically scoped language using that tree as though it
were the program.  Though the tree is (usually) infinite it is regular, so
type checking is decidable.  My observation is that it is unreasonable to
assume that all paths of the fully unrolled tree correspond to real
computations; to the contrary, it is likely that most paths do not.  This is
completely unlike the reasonable assumption that both branches of an IF can
be executed, and is unlike the other reasonable assumptions required for
static type checking in statically scoped languages.

By the way, separate compilation defeats the unrolling process, while
statically scoped languages can support static type checking even in the
presence of separate compilation.

I have been surprised by the severity of the restrictions people seem
willing to accept in order to get static type checking in a dynamically
typed language, so I withdraw my claim that the two are incompatible.
You certainly couldn't get me to use such a language, but then you couldn't
get me to use a dynamically scoped language of any sort!

Peace, William Clinger