Chuck_Lins.SIAC_QMAIL@gateway.qm.apple.com (Chuck Lins) (01/16/91)
[in <3818@cernvax.cern.ch> roberto@cernvax.cern.ch (roberto bagnara) asks] roberto> is it possible to do static type-checking when roberto> you've [got] dynamic binding? Unless I seriously misunderstand his question, I believe the answer is a qualified yes. There will still be situations where a run-time check is necessary. Consider for example the hierarchy (TFoo is at the top) TFoo --> TBar --> TBaz | |--> TFrob TFrobboz (a separate hierarchy not rooted at TFoo) The compiler can certainly detect that variables typed to one of the subclasses TBar, TBaz, TFrob are definitely also of class TFoo and that they are never TFrobboz's. The run-time checks are required when you have variables of type/class TFoo and wish to distinguish between TBar, TBaz, and TFrob. In other words, the dynamic type is different from the static type. For example, calling a method of TBaz when the static type is TFoo or TBar. The implementation of (and theory behind) the notion of 'type extension' is discussed in the paper: N. Wirth, "Type Extensions", ACM TOPLAS, Vol 10(2), April 1988, 204-214. I presume there's something similar in the work done by various folks (Ralph Johnson's name comes to mind) on typed Smalltalk. The terminology may be different, but I think the concepts are similar. -- Send compilers articles to compilers@iecc.cambridge.ma.us or {ima | spdcc | world}!iecc!compilers. Meta-mail to compilers-request.
gateley@rice.edu (John Gateley) (01/16/91)
Is it possible to do static type checking with dynamic scoping?
Well, not really. Consider the following program:
procedure foo (x:int) ...;
procedure bar (x:string) ...;
procedure baz (...) ... x ...;
What type will baz's x have, int or string? One solution that may be
possible is to construct the call graph and make sure that all bindings of x
which reach a given use have the same type. There are some drawbacks to this
solution - it is a "whole program" strategy, separate compilation is not
allowed (without lots of work). It also cannot correctly type check some
programs which are nevertheless legal. For example, the use in baz may be
limited to the x:string binding, but the call graph (constructed at compile
time) may reflect a call from foo which is never taken.
A more restrictive solution is to treat variables as global - assign them
types at the global level. Then all bindings of the variable has to match
that type.
One thing that really messes life up is 1st-class functions. They make the
call graph impossible to construct at compile time.
Are you sure you really want dynamic binding?
John
gateley@rice.edu
--
Send compilers articles to compilers@iecc.cambridge.ma.us or
{ima | spdcc | world}!iecc!compilers. Meta-mail to compilers-request.brm@Neon.Stanford.EDU (Brian R. Murphy) (01/16/91)
It seems to me that one could consider (dynamically bound) free
variables in a procedure to simply be additional parameters to the
procedure. Then standard ML-like type inference could be done.
Not being fluent with ML syntax, I give an example in (dynamically
scoped) Lisp:
(defun f (x)
(y x)) ;; y free, bound dynamically
Here f might taken to have type:
([y: a->b], a) -> b
that is, it takes an argument of type a, a binding of y with type a->b,
and returns a value of type b.
A place where f is used might look like:
(let ((y sub1))
(f 3))
where y has type
int -> int
and f is applied to ([y:int->int], int) which may be unified with the
above, yielding a result of int as well.
Keeping track of all of the current bindings and determining which
onese were relevant in a particular application would certainly
clutter up the type inference, but it shouldn't make it terribly
more difficult.
-Brian Murphy
brm@cs.stanford.edu
--
Send compilers articles to compilers@iecc.cambridge.ma.us or
{ima | spdcc | world}!iecc!compilers. Meta-mail to compilers-request.brm@Neon.Stanford.EDU (Brian R. Murphy) (01/18/91)
> Does this work even when side-effects to dynamically-bound variables are > allowed, e.g. This should be closely related to how ML would handle side-effects to variables. I'm not really sure how this happens (haven't done type inference for non-functional languages). The problems of type inference for Lisp are actually quite a bit more complex. You could probably do something like what Alex Aiken and I did for FL (described pretty abstractly in our POPL paper which will be presented next week, Type Inference in a Typeless Language, in more detail in my 1990 MIT MS thesis). The mechanism we used should be fairly easily extensible to variable side-effecting, but would suffer from terrible performance problems without further improvements. Does anyone know a reference for how ML handles side-effects to variables? -Brian -- Send compilers articles to compilers@iecc.cambridge.ma.us or {ima | spdcc | world}!iecc!compilers. Meta-mail to compilers-request.
mac@eleazar.dartmouth.edu (Alex Colvin) (01/21/91)
As an aside - languages such as C++ do static type checking on
dynamically bound (virtual) methods. In that case the dynamic chain
isn't the call chain, but the derived class chain. It turns out that
this covers a number of the classic uses of dynamic binding, such as
passing a radix to your print function.
[From mac@eleazar.dartmouth.edu (Alex Colvin)]
--
Send compilers articles to compilers@iecc.cambridge.ma.us or
{ima | spdcc | world}!iecc!compilers. Meta-mail to compilers-request.