kdmoen@watcgl.UUCP (02/13/87)
In article <814@unc.unc.UUCP> rentsch@unc.UUCP (Tim Rentsch) writes: >Side comment: I detect a hint of confusion between static binding >and static typing. At the risk of repeating myself I caution against >such confusion -- static type checking is perfectly compatible with >dynamic binding. This compatibility does not, however, mean that >statically checked systems can be statically bound. And, I apologize >if in fact no confusion indeed exists. [And, glad to see more people >realizing the value of inheritance etc as an improvement over (ugh!) >C.] (End of side comment.) In article <1040@tekchips.TEK.COM> willc@tekchips.UUCP (Will Clinger) writes: >To the contrary, static type checking is incompatible with dynamic >binding. Unfortunately, what Tim means by dynamic binding is not what Will means. (And I maintain that Will is, in any case, wrong). To clear up the misunderstanding, I will make some definitions: Lexical Scoping: Free variables in a function are inherited from the environment in which the function is *defined*. Examples: Pascal, Scheme. Dynamic Scoping: Free variables in a function are inherited from the environment in which the function is *called*. Examples: Lisp 1.5, Apl. Will Clinger (and much of the Lisp community) also refer to this as Dynamic Binding. Dynamic Message Lookup: In Smalltalk and other object oriented languages, messages are bound to methods at run time, based on the class of the reciever. In Common Loops, the classes of all of the arguments of a message are taken into account. This is what Tim Rensch calls dynamic binding. In other languages, messages (operation names) are bound to methods (procedure bodies) according to the scoping rules. Static Type Checking: Type errors are detected at compile time. Examples: Pascal. Dynamic Type Checking: Type errors are detected at run time. Examples: Lisp, Smalltalk. Here is my thesis: It is possible for a programming language to have any combination of lexical/dynamic scoping, dynamic message lookup (or not), and static/dynamic type checking. In particular, static type checking does *not* conflict with dynamic scoping. To see why, I will first have to note that, in general, static type checking requires type declarations. There are some statically typed languages (like ML) in which you can write programs with no type declarations; these languages will infer the types of every variable and formal parameter. However, type inference is a tricky problem, and can't be done in every language. There are a number of extensions of ML for which type inference has been shown to be undecidable. As Will Clinger has already pointed out, it is probably impossible to infer the types of free variables in a language with dynamic scoping. This means that in a language with dynamic scoping and static type checking, a function will have to declare the types of its free variables, which it 'imports' from the callers environment. If a function is called from an environment in which the declared types of its imported variables do not match the actual types, then a type error is reported by the compiler. Will Clinger: >To understand why static type checking is incompatible with dynamic >binding, let us consider the example of a dynamically bound Lisp in >which the + operation applies only to objects of type number. It >is impossible to perform static type checking on the procedure foo >defined by > > (define (foo n) > (+ x n)) > >because the compiler has no idea what x is going to be bound to >dynamically. In the (fortunately nonexistent) language "dynamically scoped Ada", this example would be written as: FOO: function (N: INTEGER) return INTEGER is import X: INTEGER; begin return X + N; end FOO; In general, every variable mentioned in the body of a function in DSAda must be a formal parameter, a local variable, or an imported variable, which is inherited from the calling environment. Now don't get me wrong, I am not saying that anybody would actually want to *use* a strongly typed language with purely dynamic scoping, I'm just saying that it is *possible*. Frankly, I don't like languages with pure dynamic scoping. I had some bad experiences with large APL programs in my childhood. However, a hybrid language with strong typing, default lexical scoping and optional dynamic scoping is worth investigating. -- Doug Moen (watmath!watcgl!kdmoen) University of Waterloo Computer Graphics Lab
willc@tekchips.UUCP (02/18/87)
I would like to thank Doug Moen and others for their precise definitions. My example wasn't very good, so a number of people still don't see why dynamic scoping is incompatible with static type checking. I'll try again here with the help of the following example: In article <588@watcgl.UUCP> kdmoen@watcgl.UUCP (Doug Moen) writes: >In the (fortunately nonexistent) language "dynamically scoped Ada", >[Will's] example would be written as: > > FOO: function (N: INTEGER) return INTEGER is > import X: INTEGER; > begin > return X + N; > end FOO; > >In general, every variable mentioned in the body of a function in DSAda >must be a formal parameter, a local variable, or an imported variable, >which is inherited from the calling environment. Type declarations aren't enough to support static type checking when the language is dynamically scoped. Yes, the compiler can check that all uses of X within FOO are consistent with the "import" declaration. That's easy. The problem is that the compiler cannot check statically to make sure that FOO will be called only when X is an integer variable in the dynamic calling environment. That is, the compiler cannot tell whether it should believe the declaration. Indeed, it is statically undecidable whether X will denote anything at all when FOO is called. This is the reason that dynamic scoping is incompatible with static type checking. That's not to say that dynamic scoping is incompatible with type declarations. Type declarations can improve performance even though static type checking is impossible. Peace, Will Clinger Tektronix Computer Research Lab
kdmoen@watcgl.UUCP (02/20/87)
Will Clinger (willc@tekchips.UUCP): >I would like to thank Doug Moen and others for their precise definitions. >My example wasn't very good, so a number of people still don't see why >dynamic scoping is incompatible with static type checking. It seems my original posting wasn't clear enough. To rectify this, I am going to define a language called "Dynamically Scoped Pascal". It is exactly like standard Pascal, except that free variables within procedures and functions are bound in the environment from which they are called, instead of the environment in which they are defined. Unlike standard Pascal, procedures and functions must explicitly declare all of their free variables in an "imports" clause. Here is a definition of a dynamically scoped function "FOO" which inherits a variable X from the environment from which it is called: function FOO(N: integer): integer imports(X: integer) begin FOO := X + N; end; Here are the rules for "Dynamically Scoped Pascal": * Every variable mentioned in the body of a function must be a formal parameter, a local variable, or a variable declared in an "imports" clause, which is inherited from the calling environment. * A function can only be called from an environment which defines variables whoses names and types match the names and types of the variables that the function declares using "import". For example, the function FOO may only be called from an environment that declares an integer variable called X, otherwise a type error will be detected at compile time. * The set of variables "imported" by a function is part of its type. Therefore, if FOO were passed as a function parameter, then the corresponding formal parameter would have to be declared like this: function F(N: integer): integer imports (X: integer) In other words, procedure and function parameters do not interfere with our ability to do static type checking. Will Clinger: >Type declarations aren't enough to support static type checking when the >language is dynamically scoped. Yes, the compiler can check that all uses >of X within FOO are consistent with the "import" declaration. That's easy. >The problem is that the compiler cannot check statically to make sure that >FOO will be called only when X is an integer variable in the dynamic >calling environment. In "Dynamically Scoped Pascal", it is straightforward for a compiler to do exactly this. A function can be called either the main block of the program, or from another procedure or function. Suppose FOO is called from a function called BAR. In the environment of BAR, every variable is either a local variable, a parameter, or an imported variable. Each of these variables has a declaration which can be found within the definition of BAR. Since "imports (X: integer)" is part of the type of FOO, the compiler must check that one of the variables declared within BAR is called X, with type INTEGER. If no such binding for X can be found, then a type error is declared. This can be done statically. Note that there really isn't a concept of "global variable" in DSP, only imported variables. If you tried to write a real program in DSP, then you would find that most procedures and functions would end up with rather long import lists. But that's okay, because DSP exists solely to prove that it is possible for a statically typed, dynamically scoped language to exist. Will Clinger: >This is the reason that dynamic scoping is incompatible with static type >checking. If anyone still believes this after reading this article, then they are invited to mail me an example of a DSP program that cannot be statically type checked. -- Doug Moen (watmath!watcgl!kdmoen) University of Waterloo Computer Graphics Lab
willc@tekchips.UUCP (02/23/87)
In article <624@watcgl.UUCP> kdmoen@watcgl.UUCP (Doug Moen) writes: >>This is the reason that dynamic scoping is incompatible with static type >>checking. > >If anyone still believes this after reading this article, then they >are invited to mail me an example of a DSP program >that cannot be statically type checked. What I believe is that dynamic scoping is incompatible with any reasonable form of static type checking. (Next time I'll be sure to include the qualifiers.) In practice I believe Moen's rules for DSP ("Dynamically Scoped Pascal") reduce to the restriction previously characterized as "bizarre" by Michael Condict: ...it is clear that a language cannot be dynamically bound and statically typed, unless you make the bizarre requirement a la FORTRAN that every variable named x must have the same type, even if they are otherwise completely unrelated. Otherwise it is not computable whether a reference to variable x is referring to the x that was defined as an integer or the x that was defined somewhere else as a character string. For example, here is a legal DSP program: program legal(modulo, my, imperfect, remembrance, of, Pascal); procedure a1; var x: integer; begin x := 10; writeln (x:20, glumpf (true)) end; procedure a2; var x: integer; begin x := 11; writeln (x:20, glumpf (false)) end; function glumpf (flag: boolean): integer; imports (x: integer); begin if flag then glumpf := foo(36) else glumpf := bar(37) end; function foo (n: integer): integer; imports (x: integer); begin foo := x + n end; function bar (n: integer): integer; begin bar := 49 * x end; begin a1; a2 end. If the definition of a2 is changed to procedure a2; var x: string; begin x := '49 * 37 = '; /* if Pascal had strings */ writeln (x, glumpf (false)) end; then the program ought to be legal but, according to Moen's rules for DSP, it isn't. (It would be legal if the name of the variable x declared in a2 were changed to y.) Moen's rules do not quite require that all variables named x have the same type, but they come close. > .... If you tried to write a real program in DSP, >then you would find that most procedures and functions would end up >with rather long import lists. This would imply that most variables would indeed fall under the restriction that variables of the same name must have the same type. > .... But that's okay, because DSP exists >solely to prove that it is possible for a statically typed, dynamically >scoped language to exist. Fair enough. I think it should also be clear why such a language is undesirable. William Clinger Tektronix Computer Research Lab
lambert@mcvax.UUCP (02/25/87)
In article <1075@tekchips.TEK.COM> willc@tekchips.UUCP (Will Clinger) writes: > For example, here is a legal DSP program: > > [...] > if flag then glumpf := foo(36) else glumpf := bar(37) > [...] > If the definition of a2 is changed to [...] > x := '49 * 37 = '; /* if Pascal had strings */ > then the program ought to be legal but, according to Moen's rules for > DSP, it isn't. [...] Moen's rules do not quite require that all > variables named x have the same type, but they come close. This shows, clearer than previous postings, a source of confusion in the dynamic/static type checking debate. (At the end of this article I point out some more sources of confusion.) A requirement is imposed here on static type checking that is more stringent than is usually imposed on it in the context of statically bound languages. Consider the following "Theorem": static type checking is impossible in ALL powerful languages (e.g. Pascal). "Proof": Consider begin x: integer; if <very complicated condition that cannot be computed statically but that always happens to yield true> then x := 123 else x := 'Guvf pnaabg unccra'; print(x) end. Since x is declared integer, it is illegal to assign a string to x. But the code assigning the string will never be reached, so no illegal situation will arise. So this is type-correct. A static type checker that can decide this must be able to solve arbitrary complex yes/no problems, which by Goedel is impossible. 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. Think of procedure calls as being statically macro expanded to some level N. (We need a cut off because of recursion. I am ignoring the problem of procedure variables for the sake of simplicity.) For dynamically bound languages we can almost literally expand; for statically bound languages we have to "shield" the bodies first to prevent naming conflicts. Static type-correctness can then be formulated as: no name (or literal) is used inconsistently within a single scope, however large N is chosen. It depends on details of the language what is to be understood to constitute inconsistency. Some languages (e.g. ALGOL 68) have the property that this check is decidable, others (e.g. ALGOL 60) that it is undecidable (as shown by Langmaack). But if ALGOL 60 had dynamic binding, the check would become decidable. What about that! [>> = <624@watcgl.UUCP> kdmoen@watcgl.UUCP (Doug Moen)] >> .... If you tried to write a real program in DSP, >> then you would find that most procedures and functions would end up >> with rather long import lists. > > This would imply that most variables would indeed fall under the > restriction that variables of the same name must have the same type. > >> .... But that's okay, because DSP exists >> solely to prove that it is possible for a statically typed, dynamically >> scoped language to exist. > > Fair enough. I think it should also be clear why such a language is > undesirable. If "such a language" is intended to be more general than just DSP (Dynamically Scoped Pascal), then the conclusion is unwarranted. DSP was invented on the spot by Doug Moen as a hacked variation on Pascal just to show that dynamic binding and static checking are not incompatible per se. A carefully designed language need not have the same problem. Further sources of confusion: On the nature of types. I assume that values such as can arise at run- time have a well-understood type. Call the set of all such types the Vtypes. A type-checking algorithm will try to assign static types to expressions, in particular names. Call these the Stypes. These Stypes are not necessarily taken from the set of Vtypes. For example, in ALGOL 68 the Stypes contain union-types, but a Vtype is never a union-type but simply the actual variant from the union. In polymorphic languages (ML, Miranda, ABC, ...) an Stype is a polymorphic type (containing type variables) that can be instantiated to a Vtype. A good way of thinking about this is to view an Stype as representing a SET of Vtypes. In many languages each Stype gives a singleton set so that the Stypes can be identified with Vtypes; hence the confusion to think that this is necessarily the case. In ALGOL 68, an Stype can represent a set of Vtypes if it is a union-type, but always a finite set. In polymorphic languages, Stypes can model infinite sets (e.g., LIST(*) --> {LIST(number), LIST(string), LIST(LIST(boolean)), ... }.) We cannot compute with infinite sets, so we need a finite representation. This representation must be such that if e.g. @ is an operation of the language and applying @ to a value of type t gives a value of type f(t), then for each Stype T the set {f(t) | t in the types represented by T}, if all these f(t)'s are defined (otherwise we have a type conflict) must also be representable as an Stype. The presence of type-revealing declarations can dramatically simplify static type checking, but is in no way essential. If a decision procedure for type correctness exists for a language with declarations, there also exists an algorithm that will take a source text with typing information from declarations omitted and that will output a type-correct source text with this information restored if that is possible, and otherwise terminate with a message "program cannot be typed". A final confusion I noticed is the tacit assumption that a type-checking algorithm can only assign types to variables. In general, such an algorithm may assign Stypes to all "names", including functions, operation symbols, and for Smalltalk possibly even messages (not that I see a necessity for this at the moment). A conceivable Stype for Smalltalk might be something like: Takes a message "foo" with an object x, but requires that x understands the message "bar". Such Stypes can be computed in principle without requiring declarations, import statements or other additions to the text. (These Stypes can be mutually recursive, in which case it is best to represent them somehow as nodes in a directed graph.) An object of this type will accept "foo" messages with many different Vtype type of x's, as long as they understand "bar". It may happen that for some x's during actual execution the code sending "bar" to them is not reached. This is the same as with the unreachable x := 'Guvf pnaabg unccra'. If some programmers think this imposes an undue restriction on their coding practice, I would like to see an example of reasonably understandable and maintainable code where a weaker form of typing is helpful. Even if there are examples, which I frankly speaking doubt, the merits have to be weighed against the substantive merits of some form of type checking before execution, which if strong enough will tell you about most of the silly errors you made. -- Lambert Meertens, CWI, Amsterdam; lambert@cwi.nl
willc@tekchips.UUCP (02/26/87)
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
mouse@mcgill-vision.UUCP (03/01/87)
In article <1075@tekchips.TEK.COM>, willc@tekchips.TEK.COM (Will Clinger) writes: [in contribution to the current debate] > What I believe is that dynamic scoping is incompatible with any > reasonable form of static type checking. > For example, here is a legal DSP program: > program legal(modulo, my, imperfect, remembrance, of, Pascal); > [...] > function bar (n: integer): integer; > begin > bar := 49 * x > end; From Doug Moen's article ("Article-I.D.: watcgl.624"), in which he defines DSP: > Here are the rules for "Dynamically Scoped Pascal": [...] > Every variable mentioned in the body of a function must be a formal > parameter, a local variable, or a variable declared in an "imports" > clause, which is inherited from the calling environment. ....but inside bar, x isn't a formal parameter, it isn't a local variable, and it doesn't appear in an imports clause, so bar isn't allowed to use x. der Mouse USA: {ihnp4,decvax,akgua,utzoo,etc}!utcsri!musocs!mcgill-vision!mouse think!mosart!mcgill-vision!mouse Europe: mcvax!decvax!utcsri!musocs!mcgill-vision!mouse ARPAnet: think!mosart!mcgill-vision!mouse@harvard.harvard.edu