gudeman@cs.arizona.edu (David Gudeman) (04/27/91)
There seems to be a certain entropy operating in comp.lang.misc: first a lot of the hot air gets generated over misunderstandings because people are using different definitions for terms. Then some definitions get posted and everyone uses the same terminology for a month or so. Then new posters start appearing who haven't seen the original defs and recreate the misunderstandings. This seems to have happened in the typing debates, so I'm going to post definitions again. I've added definitions for binding as well as typing since there seems to have been some confusion over that as well. I for one didn't even know that binding was part of the debate :-). Each definition is given in a formal version, followed by an implementation description for those who don't like formalism. It should be remembered though that the formalism is the definition and the implementation description is only one way (the most common way) to implement the formalism. I've decided to be a little more explicit about the fact that typing refers to machine representations, since that seems to be the major difference between the two extreme views. In other words, if typing only refers to an arbitrary set of values, then most of the differences of opinion disappear. Typing: the machine representation of a value. You must know the typing of a memory location to know how to interpret the bits as a value. Static typing: the assignment of a typing to all the values that a given syntactic expression might produce. This is generally implemented by having the programmer declare the typings of the variables, and then inferring the typing of compound expressions by the types of the operations. Dynamic typing: a programming language feature where the typing of a value can be determined from the value alone, without reference to the way in which the value is used. This is generally implemented by adding a type tag to all values at runtime. Note that since the sizes of values are not known statically, some form of automatic storage management is needed to implement dynamic typing. Strong typing: the feature that an operation cannot return an undefined result because it did not know the typing of one of its operands. Strong static typing is implemented by only allowing operators to be applied to operands whose typing can be statically inferred to be correct for that operator. Strong dynamic typing is implemented by having each operator dynamically check the type tags of its operands to make sure they are correct. Weak typing: the lack of strong typing. Generally, this means that when you call an operation on a value with an unrecognized typing, the operator will return some strange result or core dump. Static binding: the operation represented by a given name or symbol is determined by the program text alone. The simplest way to implement this is to make sure each token represents a unique operation. Some languages allow a token to represent different operations as long as the correct operation can be uniquely determined by considering the static typing. Dynamic binding: the operation represented by a given expression cannot be determined by text alone -- it depends on the execution of the program. Usually the dynamic choice of operation is made based on dynamic typing tags. -- David Gudeman gudeman@cs.arizona.edu noao!arizona!gudeman
rockwell@socrates.umd.edu (Raul Rockwell) (04/29/91)
I mostly agree with the recent posts giving definitions of things like dynamic/static typing, ... But I think the definitions given for Strong typing were a bit cloudy. David Gudeman [] [] Strong typing: the feature that an operation cannot return an [] undefined result because it did not know the typing of one of its [] operands. Strong typing also means that the function will terminate. [] Strong static typing is implemented by only allowing operators to [] be applied to operands whose typing can be statically inferred to [] be correct for that operator. [] Strong dynamic typing is implemented by having each operator [] dynamically check the type tags of its operands to make sure they [] are correct. Note that checking type tags, without checking operand values is not adequate for all cases. This is why you cannot statically insure that an inverse function is being applied to operands which are correct for that function (or operator). Darren New :: :: Strong typing: values of the wrong type cannot be stored into :: accessors (i.e., lvalues, function parameters, etc) I believe this is static typing, not strong typing. :: and functions may not be applied to values outside of their domain :: without a compiletime or runtime error. This, however, is strong typing. :: (Note: a catchable runtime error (or exception), like "message not :: understood" in Smalltalk, is not a runtime error. A non-catchable :: error, like "new" running out of space in Pascal, is a runtime :: error.) Talk about foggy explanations ;-) Maybe we need to define "error" ? :: Values of the wrong type are assumed to possibly have incompatible :: representations; i.e., valid integers may not be valid floats, etc. "assumed to possibly" ??? I suppose this could mean that you can have an integer bignum which is too large to represent using floating point notation in some implementation of a language??? In any event, I don't think this is a meaningful way of describing strong typing. Raul Rockwell
hrubin@pop.stat.purdue.edu (Herman Rubin) (04/29/91)
I was of the opinion that strong typing meant that objects (bit patterns in
memory, registers, discs, etc.) of one type could not be used as objects of
another type. As someone who has deliberately used this of course highly
non-portable feature often, it is this aspect to which I object.
--
Herman Rubin, Dept. of Statistics, Purdue Univ., West Lafayette IN47907-1399
Phone: (317)494-6054
hrubin@l.cc.purdue.edu (Internet, bitnet) {purdue,pur-ee}!l.cc!hrubin(UUCP)rockwell@socrates.umd.edu (Raul Rockwell) (04/29/91)
Herman Rubin: > I was of the opinion that strong typing meant that objects (bit patterns in > memory, registers, discs, etc.) of one type could not be used as objects of > another type. As someone who has deliberately used this of course highly > non-portable feature often, it is this aspect to which I object. It is entirely possible to define a function of the form pun(to_type, from_type, source_object) All versions of this are portable, but defining such a function so that it is efficient on one machine does not always mean that it is efficient on another machine. In the general case (arbitrary types, arbitrary platform) you will need to copy the object when you change its type. Tomas Breuel: > Dynamically typed programs are also impossible to prove type-correct, > and many trivial errors go unchecked. This is true when you are using a statically typed language (which does not provide support of dynamically typed programs). This is not true in general, however. On the hunch you've killed the subject thread where we've been discussing this, I will repeat: You can implement static typing in a dynamically typed language by introducing "functions" which do no processing but which have limited domains. These functions are equivalent to type declarations. In a well-written program, in a well-designed language, you should not _usually_ need such a function. All primitive functions of the language should have such functionality built-in. Raul Rockwell
new@ee.udel.edu (Darren New) (04/30/91)
In article <333124@socrates.umd.edu> rockwell@socrates.umd.edu (Raul Rockwell) writes: >I think the definitions given for >Strong typing were a bit cloudy. >Strong typing also means that the function will terminate. Excuse me? Any language implementing while loops has functions which won't terminate, strong typing or not. Or do you mean it will terminate when passed values of the wrong type? >Note that checking type tags, without checking operand values is not >adequate for all cases. Nor is it in static typing. >Darren New :: >:: Strong typing: values of the wrong type cannot be stored into >:: accessors (i.e., lvalues, function parameters, etc) >I believe this is static typing, not strong typing. No. Static typing is when you know what types of values are supposed to be stored into variables. For example, old K&R C (or old FORTRAN) allows integers to be passed into float parameters of functions. Hence, even tho these languages are statically typed (because each syntactic expression (e.g., variable) has a certain type), they are not strongly typed because the language does not guarantee that there won't be type errors. Similarly with printf(). Contrast this with Pascal, where function calls and writeln() calls cannot cause the wrong type values to be stored into properly-declared variables. >:: and functions may not be applied to values outside of their domain >:: without a compiletime or runtime error. >This, however, is strong typing. I disagree. If I convert assignment to a function call, does this change the fundamental strength of the typing system? Preventing wrong-type assignments is just as strong or dynamic as preventing invalid function calls. >:: (Note: a catchable runtime error (or exception), like "message not >:: understood" in Smalltalk, is not a runtime error. A non-catchable >:: error, like "new" running out of space in Pascal, is a runtime >:: error.) >Talk about foggy explanations ;-) >Maybe we need to define "error" ? My point is that if you have an exception-handling mechanism that the programmer can use to catch "message not understood" errors, then one cannot really say that the behavior of a function generating a message-not-understood is "undefined". Something that aborts the program without giving the program a chance to clean up could be considered a runtime error. Undetected errors are also "errors". >:: Values of the wrong type are assumed to possibly have incompatible >:: representations; i.e., valid integers may not be valid floats, etc. >"assumed to possibly" ??? Merely meaning that the strong vs weak distinction is moot if there is only one type of value. >In any event, I don't think this is a meaningful way of describing >strong typing. So how would you describe it clearly and concisely? -- --- Darren New --- Grad Student --- CIS --- Univ. of Delaware --- ----- Network Protocols, Graphics, Programming Languages, FDTs ----- +=+ Nails work better than screws, when both are driven with hammers +=+
yodaiken@chelm.cs.umass.edu (victor yodaiken) (04/30/91)
In article <52164@nigel.ee.udel.edu> new@ee.udel.edu (Darren New) writes: >Excuse me? Any language implementing while loops has functions which >won't terminate, strong typing or not. Or do you mean it will terminate Not necessarily. Only if we allow "types" that are not well-founded. And, why we would want to do that in a computer programming language is beyond me. >My point is that if you have an exception-handling mechanism that >the programmer can use to catch "message not understood" errors, then >one cannot really say that the behavior of a function generating a >message-not-understood is "undefined". Something that aborts the >program without giving the program a chance to clean up could be >considered a runtime error. Undetected errors are also "errors". > Not undefined, but not well defined. i.e. f(x) = { g(x) or unroll program state ...} Not very nice.
tmb@ai.mit.edu (Thomas M. Breuel) (04/30/91)
T[h]omas Breuel: > Dynamically typed programs are also impossible to prove type-correct, > and many trivial errors go unchecked. This is true when you are using a statically typed language (which does not provide support of dynamically typed programs). This is not true in general, however. Dynamic typing lets you write programs like the following: ;;; Scheme (define (fermat-conjecture-is-true?) ...) (define (f) (if (fermat-conjecture-is-true?) 9 #f)) (define (g) (+ (f) 1)) (g) Now, you cannot determine statically whether this program is type-correct (i.e., whether this program will never give you a runtime type error). A statically typed language will simply not allow you to write such functions: (* SML *) fun f () = if fermat_conjecture_is_true_p() then 9 else false ---> type error In order to express the same concept in a statically typed language like SML, you have to use unions: (* SML *) datatype bool_or_int = BOOL of bool | INT of int; fun f () = if fermat_conjecture_is_true_p() then INT(9) else BOOL(false) ---> f: unit -> bool_or_int In essence, you are introducing a little bit of dynamic typing into the statically typed language. You can implement static typing in a dynamically typed language by introducing "functions" which do no processing but which have limited domains. These functions are equivalent to type declarations. You can write: ;;; Scheme (define (NUMBER-+ x y) (if (not (and (number? x) (number? y))) (error "number+") (+ x y))) (define (DOUBLE x) (NUMBER-+ 'a 'b)) However, this does not give you static typing, since the Scheme compiler is not required to check statically whether all uses of NUMBER-+ satisfy the type constraints. In fact, in most cases, it cannot even determine the type correctness of your program statically because of language semantics. For example, in the above example, the compiler cannot flag a type error for the function DOUBLE because NUMBER-+ could have been rebound by the time DOUBLE is called. Static typing is added functionality in the compiler. If you want to, you can use dynamic typing on top of a statically typed language, but the converse is not true. In a well-written program, in a well-designed language, you should not _usually_ need such a function. All primitive functions of the language should have such functionality built-in. I disagree. It is very useful to be able to flag the type error in the function DOUBLE shown above at compile time. DOUBLE may be called only very rarely, so that it doesn't get detected on testing, but the runtime type error might "make your airplane crash". Trivial type errors like this occur even in well-written programs, and cannot be caught by many well-designed dynamically typed languages (like Scheme) at compile time. Thomas.
olson@juliet.ll.mit.edu ( Steve Olson) (05/01/91)
In article <TMB.91Apr29182914@volterra.ai.mit.edu> tmb@ai.mit.edu (Thomas M. Breuel) writes:
Static typing is added functionality in the compiler. If you want to,
you can use dynamic typing on top of a statically typed language, but
the converse is not true.
Perhaps this statement is correct in many specific cases, but its not
correct in general. Common Lisp supports a wide variety of compile-time
type declarations. The definition of CL does not force an implementation to
use the declarations, but the major UNIX CL implementations do use the
declarations. The CL compiler I use (Lucid) is much better at using the
decls for optimization than for error checking, but this undoubtably will
improve in the future.
This lead to s semi-related pet observation of mine --
In general, type errors are quite rare when programming in a Lisp enviroment.
How many times do I confuse a pathanme with a array? How many times do I
confuse a number and a window? N-E-V-E-R. But a funny thing started happening
when I started to optimize the inner loops of some of my CL programs ...
I started getting type errors. Getting a integer and a float confused or
a single and a double confused is something that does happen quite a bit.
To make matters worse, my compiler isn't too great at detecting these types of
errors. In this situation I do need static type checking.
My contention is that a typical statically typed language causes type errors
by forcing the programmer to make micro-decisions about storage layout and
machine representation of data. Sometimes you may want to do this for
efficiency, but often its a needless burden.
--
-- Steve Olson
-- MIT Lincoln Laboratory
-- olson@juliet.ll.mit.edu
--mathew@mantis.co.uk (mathew) (05/02/91)
yodaiken@chelm.cs.umass.edu (victor yodaiken) writes: > In article <52164@nigel.ee.udel.edu> new@ee.udel.edu (Darren New) writes: > >Excuse me? Any language implementing while loops has functions which > >won't terminate, strong typing or not. Or do you mean it will terminate > > Not necessarily. Only if we allow "types" that are not well-founded. So in what way is function f() := while true do-nothing return using a type which is not well founded? For that matter, what about function f() := f() ? mathew -- mathew - mathew@mantis.co.uk or mcsun!ukc!ibmpcug!mantis!mathew
yodaiken@chelm.cs.umass.edu (victor yodaiken) (05/03/91)
In article <2494@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes: >I've decided to be a little more explicit about the fact that typing >refers to machine representations, since that seems to be the major >difference between the two extreme views. In other words, if typing >only refers to an arbitrary set of values, then most of the >differences of opinion disappear. > >Typing: the machine representation of a value. You must know the >typing of a memory location to know how to interpret the bits as a >value. > Oh, well, here's the problem. To me a "type" is not necessarily a machine-related notion. The "type" of a mathematical object refers to the operations which are meaningful on the object and the laws which govern the behavior of the object. For example "1" can be an element of a boolean algebra, the identity element of a group, an integer, or an abbreviation for the textual symbol "successor(zero())". Depending on the type which we assign to "1" we will interpret "1+1" differently. >Static typing: the assignment of a typing to all the values that a >given syntactic expression might produce. This is generally >implemented by having the programmer declare the typings of the >variables, and then inferring the typing of compound expressions by the >types of the operations. > >Dynamic typing: a programming language feature where the typing of a >value can be determined from the value alone, without reference to the >way in which the value is used. This is generally implemented by >adding a type tag to all values at runtime. Note that since the sizes >of values are not known statically, some form of automatic storage >management is needed to implement dynamic typing. > >Strong typing: the feature that an operation cannot return an >undefined result because it did not know the typing of one of its >operands. Strong static typing is implemented by only allowing >operators to be applied to operands whose typing can be statically >inferred to be correct for that operator. Strong dynamic typing is >implemented by having each operator dynamically check the type tags of >its operands to make sure they are correct. > In fact, "dynamic typing" as you have defined it, forbids strong typing unless we are willing to allow for "bad type" aborts and to consider these to be well defined results.