craig@leland.Stanford.EDU (Craig Chambers) (04/20/91)
Here's a simple example that cannot be described by a static type
system in most statically-typed object-oriented languages. I'm using
it to help me make sure that the static type system in my new OO
language is sufficiently powerful, but you could use it as another
example of a simple, useful program that is handled simply in a
dynamically-typed system that requires a lot of sophistication in a
statically-typed system.
Consider the general min function (written in a dynamically-typed
C-like language):
min(x, y) {
if (x < y) {
return x;
} else {
return y;
}
}
Assume that we have two kinds of numbers in our language, integers and
floats, and that we've defined implementations of "<" for all four
combinations of integer and float arguments. We define number as the
common supertype of both integers and floats; since we've defined all
possible combinations, "<" is defined over pairs of numbers.
We also have a collection hierarchy. The "<" message is defined for
all collections of things that themselves understand "<" to do
lexicographic ordering of two collections.
Note that we do NOT have a "<" message that can take a number as one
argument and a collection as the other.
Here's the problem: we'd like to describe the type of the min
function, so that this one piece of source code can be used to compute
the minimum of two numbers or of two collections of numbers or of two
collections of collections of numbers, etc.
So here are some examples that should type-check:
min(3, 4)
min(3, 4.5)
min({3,4}, {4,5,6})
min({{3,4.5},{5},{6,8.9}}, {{1.2,4},{2}})
And here are some that shouldn't:
min(3, {4})
min({3,4}, {{4,6},{2,3.4,6}})
We're only allowed to use static type systems that actually make
static guarantees about no message-not-understood problems; otherwise,
we'd just be using dynamic typing. This therefore disallows using
Eiffel's (old, currently implemented) type system based on covariant
typing.
I'm not saying that this cannot be done in a static type system; I'm
hoping that it can, in fact. I will claim (with the hope of being
disproved) that no "practical" existing language can statically
type-check this example.
-- Craig Chambersguido@cwi.nl (Guido van Rossum) (04/22/91)
craig@leland.Stanford.EDU (Craig Chambers) writes: >Consider the general min function (written in a dynamically-typed >C-like language): >[...] >Here's the problem: we'd like to describe the type of the min >function, so that this one piece of source code can be used to compute >the minimum of two numbers or of two collections of numbers or of two >collections of collections of numbers, etc. This can be done in ABC, a statically typed interpreted language developed at CWI [1]. ABC knows a single type "number" which can hold a float or arbitrary-precision rational, and "lists" that are sorted collections of values with the same type; list items may be lists if their types are the same, etc.; lists are sorted lexicographically. If you don't want the items sorted there is a "table" type that lets you determine the order; tables are really associative arrays. The function you describe is written in ABC as follows: HOW TO RETURN min(x, y): IF x < y: RETURN x RETURN y and now you will have min(3.14, 1) = 1, min({1;2;3}, {1;2}) = {1;2}, etc., and min(3.14, {}) will not type-check. [2] --Guido van Rossum, CWI, Amsterdam <guido@cwi.nl> Founder of the Royal Society for Prevention of Cruelty to Amoebae [1] %T ABC Programmer's Handbook %A Leo Geurts %A Lambert Meertens %A Steven Pemberton %I Prentice-Hall %C London %D 1990 %O ISBN 0-13-000027-2 [2] ABC is implemented; I typed the example in and here's the session log: piring& abc ABC Release 1.02.01. Copyright (c) Stichting Mathematisch Centrum, Amsterdam, 1989. Type '?' for help. >first >>> HOW TO RETURN min(x, y): HOW TO RETURN min(x, y): IF x < y: RETURN x RETURN y >>> WRITE min(3.14, 1) 1 >>> WRITE min({1; 2; 3}, {1; 2}) {1; 2} >>> WRITE min(1, {}) *** Cannot reconcile the types in your command WRITE min(1, {}) *** The problem is: I found type EG (0, list or table) where I expected (?, ?) >>> QUIT piring&
sakkinen@jyu.fi (Markku Sakkinen) (04/22/91)
In article <1991Apr20.010347.28984@leland.Stanford.EDU> craig@self.stanford.edu writes: > >Here's a simple example that cannot be described by a static type >system in most statically-typed object-oriented languages. I'm using >it to help me make sure that the static type system in my new OO >language is sufficiently powerful, but you could use it as another >example of a simple, useful program that is handled simply in a ^^^^^^^^^^^^^^^^^^^^^^^^^^^ >dynamically-typed system that requires a lot of sophistication in a ^^^^^^^^^^^^^^^^^^^^^^^^ >statically-typed system. > ... >Assume that we have two kinds of numbers in our language, integers and >floats, and that we've defined implementations of "<" for all four >combinations of integer and float arguments. We define number as the >common supertype of both integers and floats; since we've defined all >possible combinations, "<" is defined over pairs of numbers. > >We also have a collection hierarchy. The "<" message is defined for >all collections of things that themselves understand "<" to do >lexicographic ordering of two collections. > >Note that we do NOT have a "<" message that can take a number as one >argument and a collection as the other. > ... It appears to me that the given starting point for this problem (although somewhat fuzzily defined) itself requires additional work in a purely dynamically-typed system, but is simple in a statically-typed system with the appropriate features, i.e. first-class set types. (I don't know about SETL except that it's built mainly upon set handling; is it statically typed?) It seems that you require homogeneous sets, i.e. sets of numbers, sets of sets of numbers, etc. In a statically-typed language that really supports sets of any order, you can get that homogeneity automatically with the correct type definition. If you then try to add a NUMBER to a SET OF SET OF NUMBER you get a compile-time error. In a dynamically-typed language, you have to program yourself the run-time tests to check: (1) when you try to add a new element to a non-empty set, that it is of the same "degree" as the previous elements (2) when applying the '<' operator to two objects, that they are of the same "degree" On the other hand, I don't know if any current statically-typed language allows a convenient single recursive definition of '<' for all such set types (some functional language perhaps?). In a dynamically-typed object-oriented language, it would obviously suffice to define a class StratifiedOrderedCollection, which would have the "degree" as one instance variable. P.S. The word 'degree' is in quotes above because I am uncertain about the established term. Is it 'order' (what an overloaded word: no wonder that the misnomer 'sorting' is so commonly used for 'ordering')? Markku Sakkinen Department of Computer Science and Information Systems University of Jyvaskyla (a's with umlauts) PL 35 SF-40351 Jyvaskyla (umlauts again) Finland SAKKINEN@FINJYU.bitnet (alternative network address)
jlophel@watmsg.waterloo.edu (John Ophel) (04/22/91)
> Article: 7556 of comp.lang.misc > From: craig@leland.Stanford.EDU (Craig Chambers) > Here's a simple example that cannot be described by a static type > system in most statically-typed object-oriented languages. > Consider the general min function (written in a dynamically-typed > C-like language): > min(x, y) { > if (x < y) { > return x; > } else { > return y; > } > } > So here are some examples that should type-check: > min(3, 4) > min(3, 4.5) > min({3,4}, {4,5,6}) > min({{3,4.5},{5},{6,8.9}}, {{1.2,4},{2}}) > And here are some that shouldn't: > min(3, {4}) > min({3,4}, {{4,6},{2,3.4,6}}) > -- Craig Chambers Here is a solution in watML, an experimental dialect of ML developed here at the University of Waterloo. watML basically adds ideas presented in the paper by Cormack and Wright "Type-dependent Parameter Inference" SIGPLAN'90 Conference to ML. The work on watML is being done by Gord Cormack and me. The first problem is that if min (3,4.5) is permitted, then what is the result type of min (integer or real)? The solution in ML is to introduce a discriminated (tagged) union - datatype number = Int of int | Real of real; Now min (Int 3, Real 4.5) will return a number object. watML adds overloading to ML. - fun min (x,y) = if x < y then x else y; > val min = [?<: ('a * 'a) -> bool]('a * 'a) -> 'a The reading of the type of min is, if an appropriate instance of < can be found by searching the environment, then min is a function that takes two arguments of the same type and returns the lesser (as defined by the < function that was chosen). An appropriate instance of < is selected based on having a matching type. [As an aside, min is implemented by the compiler as a function that takes an extra parameter (<), and for any use of min, the compiler automatically supplies the appropriate < function to use.] We now define an instance working over numbers (the overload construct is not in ML) - overload < = fn (Int i, Int j) => i < j | (Int i, Real r) => (real i) < r | (Real r, Int i) => r < (real i) | (Real r, Real s) => r < s; > val < = fn : (number * number) -> bool In ML syntax "fn" is "lambda", so if < gets two nums, it pattern-matches on their constructors and selects the appropriate instance of < to use. For example, the first case will select integer < as i and j are both integers. The next three cases will select real <. We can now define an instance working over lists - overload < = fn ([],[]) => false | ([],_) => true | (_,[]) => false | ((a::b),(c::d)) => (a<c) orelse (b<d); > val < = [?<: ('a * 'a) -> bool](('a list) * ('a list)) -> bool Notice that in the last case, there are two uses of <, the first cannot be resolved (as the list arguments are polymorphic), the second is the instance we are defining (< over lists). The unresolved instance of < is reflected in the type of this instance that requires an instance of <. - min (Int 3, Int 4); Int 3 : number - min (Int 3, Real 4.5); Int 3 : number - min ([Int 3, Int 4],[Int 4, Int 5, Int 6]); [Int 3, Int 4] : number list - min ([[Int 3, Int 4, Int 5],[Int 5], [Int 6, Real 8.9]], [[Real 1.2,Int 4],[Int 2]]); [[Real 1.2,Int 4],[Int 2]] : (number list) list but - min (Int 3, [Int 4]); - min ([Int 3, Int 4], [[Int 4, Int 6], [Int 2, Real 3.4, Int 6]]); both give type errors. Comments ======== - I have not attempted to explain how overloaded instances are resolved. We are currently working on a paper that describes the system. - There are problems with overloading resolution, the selection process can get into an infinite loop (in obscure cases). This needs to be investigated. - Static typing solutions are occassionally more involved than dynamic typing solutions. As more work is done with static systems, however, more and more problems that were previously clumsy or difficult with static typing can be naturally expressed with static typing; for example, ML's parameteric polymorphism permits polymorphic functions to be written with the security of static typing; ML's type inference removes the need for redundant type declarations; watML adds overloading to a static type system. Experience with dynamic type systems has suggested valuable concepts that languages should be able to support; modern static type systems are attempting to provide these concepts within secure, efficient systems. - Overloading with type classes is part of the Haskell language definition (see the Haskell report or Blott & Wadler's very readable POPL'89 paper). John Ophel
boehm@parc.xerox.com (Hans Boehm) (04/23/91)
Aside from syntactic issues, this doesn't seem very hard in languages like Russell, Quest, or Poly. I either need a built-in type number, or I need to explicitly define something that is the tagged union of integers and floats. (The tag may be a method suite.) I then define min to take a type (or algebra, or your favorite term...) with a "<" operation and its two "real" arguments. (When I apply min, the type argument can be inferred.) This forces a static check that the two argument types are the same. This still involves at least some dynamic method selection. But that seems inherent in the problem. Whether you consider these languages to be practical is a matter of taste. They have all been used to build nontrivial programs. Hans
euaabt@eua.ericsson.se (Anders.Bjornerstedt) (04/23/91)
I suspect that you could express this, or something very close to it, in the language CLU. The problem is I dont have the relevant references accessible, I am short of time, I am lazy, etc etc. So why do I write this ? Well to encourage any person out there knowlegable in CLU to try! -------------------------------------------- Anders Bjornerstedt Software Development Environments ELLEMTEL Box 1505 S-125 25 Alvsjo SWEDEN Tel: +46-8-727 40 67 Fax: +46-8-647 82 76 E-mail: Anders.Bjornerstedt@eua.ericsson.se
craig@elaine35.Stanford.EDU (Craig Chambers) (04/24/91)
In article <1991Apr23.152110.6500@eua.ericsson.se> euaabt@eua.ericsson.se (Anders.Bjornerstedt) writes: >I suspect that you could express this, or something very close to it, in >the language CLU. The problem is I dont have the relevant references >accessible, I am short of time, I am lazy, etc etc. So why do I write >this ? Well to encourage any person out there knowlegable in CLU to try! I used to work with the CLU people and have written a number of CLU programs while a student at MIT. CLU's where clauses provide some of the solution (they act like the type patterns I alluded to in an earlier message), but CLU has no subtyping, so it can't handle comparing subtypes of number. -- Craig Chambers
new@ee.udel.edu (Darren New) (04/24/91)
I think it is important to remember the differences between dynamic
typing and dynamic binding. Many of the arguments in this thread get
confused because the distinction is not made clear and some systems
have one without the other while other systems intertwine both. For
example, Hermies has dynamic typing (via polymorph) without dynamic
binding (in the normal OO sense). C++ has some limited dynamic binding
without dynamic typing. Smalltalk intermixes the dynamic typing and
the dynamic binding semantically, muddying the waters.
Personally, I think both are necessary, but for different tasks.
--
--- Darren New --- Grad Student --- CIS --- Univ. of Delaware ---
----- Network Protocols, Graphics, Programming Languages, FDTs -----
+=+=+ My time is very valuable, but unfortunately only to me +=+=+
+=+ Nails work better than screws, when both are driven with screwdrivers +=+duchier@cs.yale.edu (Denys Duchier) (04/24/91)
Haskell has the notion of classes, and below is the code taken verbatim from the implementation of the Prelude. `instance (Ord a) => Ord [a] where ...' basically means, if `a' is a type of class Ord, then `list of a' is also a type of class Ord, and the following operations are defined on it...'. Implementing this functionality typically requires passing a dictionnary (as an additional argument) that specifies the operations defined on type `a' as a member of class Ord (something like this; I'm a little fuzzy on the exact details). module PreludeListInst where import PreludeRealCore instance (Eq a) => Eq [a] where [] == [] = True (a:b) == (c:d) = a == c && b == d _ == _ = False instance (Ord a) => Ord [a] where [] <= _ = True _ <= [] = False (a:b) <= (c:d) = a <= c || a == c && b <= d _ < [] = False [] < _ = True (a:b) < (c:d) = a < c || a == c && b < d See "Report on the programming Language Haskell, A non-strict, Purely Functional Language" (YALEU/DCS/RR-777). Does this answer your question, or did I misunderstand the point you were trying to make? --Denys
wright@gefion.rice.edu (Andrew Wright) (04/24/91)
In article <1991Apr22.151149.9661@watmath.waterloo.edu> jlophel@watmsg.waterloo.edu (John Ophel) writes: ... > - Static typing solutions are occassionally more involved than dynamic typing >solutions. As more work is done with static systems, however, more and more >problems that were previously clumsy or difficult with static typing can >be naturally expressed with static typing; for example, ML's parameteric >polymorphism permits polymorphic functions to be written with the security >of static typing; ML's type inference removes the need for redundant type >declarations; watML adds overloading to a static type system. Experience >with dynamic type systems has suggested valuable concepts that languages >should be able to support; modern static type systems are attempting to provide >these concepts within secure, efficient systems. Furthermore, static type systems are able to accomplish some things which cannot be accomplished in dynamic type systems. Overloading is a case in point - the appropriate definition of a overloaded name is selected based on information which is not part of a dynamic language. In simple systems, overloading may be regarded as simple syntactic convenience, however in systems like watML and Haskell, it is much more than simple syntactic convenience, as the "min" solutions posted by John indicate. Andrew K. Wright Computer Science, Rice University wright@rice.edu Houston Texas 77251-1892
pwd@cl.cam.ac.uk (Peter Dickman) (04/24/91)
In article <1991Apr23.152110.6500@eua.ericsson.se> euaabt@eua.ericsson.se (Anders.Bjornerstedt) writes: >I suspect that you could express this, or something very close to it, in >the language CLU. You mean like this? (Please excuse the style... :-) Please read carefully - including the notes below, before telling me that I haven't solved the problem. min = PROC [T : TYPE] (x, y : T) RETURNS (T) WHERE T HAS lt : PROCTYPE (T,T) RETURNS (bool) IF (x < y) THEN RETURN (x) ELSE RETURN (y) ENDIF END min Note that both arguments must be the same type; but int & real aren't the same so you'd have to explicitly convert the int into a real first (*). Also, < is just syntactic sugar for an invocation of the lt function, so (x < y) is read by the compiler as type_of(x)$lt(x,y), in other words I could have put T$lt(x,y) instead of x < y. CLU doesn't distinguish between built-in & user-defined types - it treats them all the same. If the instantiating type for T doesn't support a lt operation there'll be a compile-time error. Calls would then be things like: a : int := min[int](5,6) b : list := min[list](c,d) % where list is a user-defined cluster % (type) supporting an lt operation and % c & d are of type list e : real := min[real](real$i2r(6), 2.0) % convert an int to a real first (the type declaration would, obviously, be omitted if the variables were previously declared). Many other languages can be used in EXACTLY the same way. If it has constrained genericity you can do this. All of the CLU family (CLU, CCLU, Argus, Troy etc) for example. Sadly Eiffel has inheritance & unconstrained genericity but the constrained genericity was left out (I don't like Bertrand Meyer's justification for this I'm afraid - but accept that he had his reasons). Doesn't Ada have some form of generics too? Note that CLU is strongly typed. There is the possibility of over-riding the static typing by use of the ANY type, however the only way you can apply an operation to an ANY is by FORCEing it to a type (otherwise all you can do is assign the ANY value to a variable of type ANY). And the only type that an object can be forced to is the one it started as (otherwise there's a run-time exception). Note also that because of the signal mechanism (and the fact that the CCLU compiler (& maybe others) warns you if you fail to catch all possible signals) you have no-one to blame but yourself if there is a run-time type failure which can't be handled by your code. The FORCE operation is defined as: FORCE = PROC [T: TYPE] (x : ANY) RETURNS (T) SIGNALS (wrong_type) This solves the resource-manager problem that's being discussed in the "Run-time Type Errors in Smalltalk" thread. ---------------- (*) By the way - int and real AREN'T the same. I certainly don't want a compiler 'helping' me when I use 2 instead of 2.0 (or, worse still, 'number_readings : int' instead of 'latest_reading : real'). It helps to keep the lid on bugs to be explicit about what you are doing - and helps the compiler to optimise things too. Because of this lack of sub-typing the problem as originally posed cannot be answered in CLU. Finding the min of a real and an int would be faulted. What's the problem with an explicit coercion though? Is it merely a matter of taste? Or down to the "minimal thought vs maximal confidence" religious war? Those who believe this problem should be solvable as originally posed, please read & reflect on the following: Assume that A is of type M, B is of type N and both M & N are subtypes of type P, which defines a < operation; it doesn't necessarily make sense to assume automatically that A & B can be compared with <, since either M or N may have redefined <. In particular, if <P is the P < operator and <M is a reimplemented < operator for M. We could have A,C of type M and B of type N with A <P B, B <P C and C <M A; but, one hopes, A <P C in order to maintain transitivity of <P. So how would this hoped-for super-min function cope? Any one invocation might be reasonable but a mutually inconsistent set of invocations could easily result. The only way I can see to handle this is to say that the reimplemented <M must be consistent with the original <P function - I don't believe anyone knows how to ensure this sort of thing, let alone has actually built it into a real language. Besides, in this case such a constraint renders <M redundant (unless it has side-effects :-). -- Peter
new@ee.udel.edu (Darren New) (04/24/91)
In article <1991Apr24.042652.23886@rice.edu> wright@gefion.rice.edu (Andrew Wright) writes: >Furthermore, static type systems are able to accomplish some things >which cannot be accomplished in dynamic type systems. Overloading is >a case in point - the appropriate definition of a overloaded name is >selected based on information which is not part of a dynamic language. Excuse me? Have you looked at Smalltalk lately? The difference between overloading and dynamic binding is the difference between static typing and dynamic typing. Any dynamically typed language with dynamic binding has "the appropriate definition of an overloaded name [] selected based on information" is *is* a part of a dynamic language. Or do I misunderstand what you are saying? -- Darren -- --- Darren New --- Grad Student --- CIS --- Univ. of Delaware --- ----- Network Protocols, Graphics, Programming Languages, FDTs ----- +=+=+ My time is very valuable, but unfortunately only to me +=+=+ +=+ Nails work better than screws, when both are driven with screwdrivers +=+
gudeman@cs.arizona.edu (David Gudeman) (04/25/91)
In article <51669@nigel.ee.udel.edu> Darren New writes:
]... Hermies has dynamic typing (via polymorph) without dynamic
]binding (in the normal OO sense). C++ has some limited dynamic binding
]without dynamic typing. Smalltalk intermixes the dynamic typing and
]the dynamic binding semantically, muddying the waters.
OK, I give up. What is the difference between dynamic typing and
dynamic binding?
--
David Gudeman
gudeman@cs.arizona.edu
noao!arizona!gudemanwg@opal.cs.tu-berlin.de (Wolfgang Grieskamp) (04/25/91)
gudeman@cs.arizona.edu (David Gudeman) writes: >In article <51669@nigel.ee.udel.edu> Darren New writes: >]... Hermies has dynamic typing (via polymorph) without dynamic >]binding (in the normal OO sense). C++ has some limited dynamic binding >]without dynamic typing. Smalltalk intermixes the dynamic typing and >]the dynamic binding semantically, muddying the waters. >OK, I give up. What is the difference between dynamic typing and >dynamic binding? I guess the following: C++ is "strongly typed" with dynamic binding (according to "virtuals"), since the error "message not understood" is not part of the languages operational semantics. Each message send to an object will be understood by one of its classes in the class hierarchy (however, the final superclass may implement the message by printing "message not understood" and just exit()...). Smalltalk is "dynamically typed" with dynamic binding, since the error "message not understood" is part of the languages operational semantics. -- Wolfgang Grieskamp wg@opal.cs.tu-berlin.de tub!tubopal!wg wg%opal@DB0TUI11.BITNET
bertrand@eiffel.UUCP (Bertrand Meyer) (04/26/91)
From <1991Apr20.010347.28984@leland.Stanford.EDU> by craig@leland.Stanford.EDU (Craig Chambers): > > Here's a simple example that cannot be described by a static type > system in most statically-typed object-oriented languages. I'm using > it to help me make sure that the static type system in my new OO > language is sufficiently powerful. > > Here's the problem: we'd like to describe the type of the min > function, so that this one piece of source code can be used to compute > the minimum of two numbers or of two collections of numbers or of two > collections of collections of numbers, etc. > > So here are some examples that should type-check: > > min(3, 4) > min(3, 4.5) > min({3,4}, {4,5,6}) > min({{3,4.5},{5},{6,8.9}}, {{1.2,4},{2}}) > > And here are some that shouldn't: > > min(3, {4}) > min({3,4}, {{4,6},{2,3.4,6}}) I don't know about ``most statically-typed object-oriented languages'' but in Eiffel this does not appear particularly difficult. Class COMPARABLE describes order relations; one could define `min' in that class as min (other: like Current): like Current is -- Minimum of current element and `other' do if Current < other then Result := Current else Result := other end end -- min In COMPARABLE, the operator "<" means a call to the following function: infix "<" (other: like Current): BOOLEAN is -- Is current element less than or equal to `other'? deferred end -- "<" Then INT, FLOAT and SORTED_LIST (a generic class) may inherit from COMPARABLE and provide an effective declaration for infix "<". The ``like'' keyword used in these declarations is one of the key parts of the type system, known as anchored declarations. What it means is that `other' and the result of `min' must be of the same type as Current (the current object), even if redefined in a descendant class. In SORTED_LIST [X], for example, the actual argument to both of the above functions must also be of type SORTED_LIST [X], or a conforming (descendant) type. Anchored declarations of this kind are what makes typing possible and useful; they directly reflect the covariant rule, without which typing, in our experience, would not work. With the proper declarations for arguments a and b, the call a.min (b) for the six examples given by Mr. Chambers will yield the desired behavior: acceptance in the first four cases, rejection in the last two. This assumes the following declarations (respectively): 1 a, b: INT 2 a: INT; b: FLOAT 3 a, b: SORTED_LIST [INT] 4 a, b: SORTED_LIST [SORTED_LIST [INT]] 5 a: INT; b: SORTED_LIST [INT] 6 a: SORTED_LIST [INT]; b: SORTED_LIST [SORTED_LIST [INT]] In the last two cases, you can cheat the type system in Eiffel 2.3 by declaring for example a and b as being of type COMPARABLE, and then assigning to them the values given in the corresponding examples. This is because the detection of such erroneous cases requires system-level checking (as opposed to class-level checking), which will only be provided in Eiffel version 3. However such cases occur rarely except if specially contrived. Eiffel 3 will also have two properties which are relevant to this discussion: - - It will be possible to anchor a function result to an argument of the function. In function `min', for example, it will be possible to declare the function result as being of type `like other', which provides more flexibility than `like Current'. (With the above declaration, if `n' is integer and `r' real, you have to write a call as r.min (n) rather than n.min (r); with the relaxed rule both are possible. - Support for manifest arrays makes it possible to write examples such as min({3,4}, {{4,6},{2,3.4,6}}) in almost exactly this syntax, with << for the opening brace and >> for the closing brace. The rule is that <<a, b, ...>> conforms to ARRAY [T] for any T for which all of a, b, ... conform to T. This will mean that even without any entity declarations (of the forms numbered 1 to 6 above) the type checking will yield the desired effect. -- -- Bertrand Meyer Interactive Software Engineering Inc., Santa Barbara bertrand@eiffel.uucp
rockwell@socrates.umd.edu (Raul Rockwell) (04/26/91)
Wolfgang Grieskamp writes: > C++ is "strongly typed" with dynamic binding (according to > "virtuals"), since the error "message not understood" is not part of > the languages operational semantics. If C++ is strongly typed because of the lack of this error, then so is machine language. I'm not sure I see the point of calling this property "strongly typed". My own definition of "strongly typed" was that the language will not return a result for applying a function to values which are outside its domain. Note that except for trivial cases you most definitely can get "domain errors" (or "message not understood") at runtime. Now, I understand that classic works have claimed that a type error is a value which puts the program in an infinite loop. However, I would say that a language where this happens is weakly typed. In fact, I think that from this point of view, a "strongly typed" language is one which only allows finite looping constructs, and which guarantees a well-behaved "run-time error" whenever a partial function is applied incorrectly (or maybe we should call this "absolutely typed"?). Raul Rockwell
euaabt@eua.ericsson.se (Anders.Bjornerstedt) (04/26/91)
craig@elaine35.Stanford.EDU (Craig Chambers) writes: >In article <1991Apr23.152110.6500@eua.ericsson.se> euaabt@eua.ericsson.se (Anders.Bjornerstedt) writes: >>I suspect that you could express this, or something very close to it, in >>the language CLU. The problem is I dont have the relevant references >>accessible, I am short of time, I am lazy, etc etc. So why do I write >>this ? Well to encourage any person out there knowlegable in CLU to try! >I used to work with the CLU people and have written a number of CLU >programs while a student at MIT. CLU's where clauses provide some of >the solution (they act like the type patterns I alluded to in an >earlier message), but CLU has no subtyping, so it can't handle >comparing subtypes of number. >-- Craig Chambers Yes, but CLU does have parameterized types. If I remeber correctly you could specify the type parameters of a new type by requiring that the parameter types "conform" by having one or more methods with a certain signature. This might be more flexible than using inheritance (of specification), although less safe since signatures say very little about semantics. On the other hand maybe the type parameters have to be bound at compile time in CLU? in which case i guess CLU could not solve the problem. -------------------------------------------- Anders Bjornerstedt Software Development Environments ELLEMTEL Box 1505 S-125 25 Alvsjo SWEDEN Tel: +46-8-727 40 67 Fax: +46-8-647 82 76 E-mail: Anders.Bjornerstedt@eua.ericsson.se
rick@tetrauk.UUCP (Rick Jones) (04/26/91)
In article <1991Apr24.144714.17740@cl.cam.ac.uk> pwd@cl.cam.ac.uk (Peter Dickman) writes: > [ ... ] Sadly Eiffel has inheritance & unconstrained genericity but the >constrained genericity was left out (I don't like Bertrand Meyer's >justification for this I'm afraid - but accept that he had his reasons). Just to correct a misunderstanding, Eiffel DOES have constrained genericity. This was introduced in version 2.2 of the language (released about 18 months ago). Dr. Meyer has revised a few of the opinions he expressed in his book OOSC since it was first published, and Eiffel has evolved as a result. It does mean that OOSC is out of date as far as a true definition of the language is concerned. On this subject, the book "Eiffel: the Language" is due for publication very soon, and will define version 3 of the language. This addresses many issues, large and small, which have been found in practice by users of the language, and should prove very interesting reading for anyone concerned with programming languages. -- Rick Jones, Tetra Ltd. Maidenhead, Berks, UK rick@tetrauk.uucp Any fool can provide a solution - the problem is to understand the problem
craig@leland.Stanford.EDU (Craig Chambers) (04/27/91)
In article <554@eiffel.UUCP>, bertrand@eiffel.UUCP (Bertrand Meyer) writes: |> I don't know about ``most statically-typed object-oriented |> languages'' but in Eiffel this does not appear particularly |> difficult. Class COMPARABLE describes order relations; |> one could define `min' in that class as |> |> min (other: like Current): like Current is |> -- Minimum of current element and `other' |> do |> if Current < other then |> Result := Current |> else |> Result := other |> end |> end -- min |> |> In COMPARABLE, the operator "<" means a call to the following |> function: |> |> infix "<" (other: like Current): BOOLEAN is |> -- Is current element less than or equal to `other'? |> deferred |> end -- "<" |> |> Then INT, FLOAT and SORTED_LIST (a generic class) may inherit |> from COMPARABLE and provide an effective declaration for infix "<". Eiffel's rules allow this to be type checked by having broken type checking rules, in my opinion. Covariant type-checking rules do not enure type safety statically (you mention this towards the end of your message). The newer proposed rules (as yet unimplemented, I believe) do ensure type safety statically, but by effectively enforcing a contravariant typing discipline which then prevents this example from being type checked. I suspect that the new type checking rules will never actually be implemented and widely adopted since they will disallow many existing Eiffel programs which have relied on the covariant type checking rule. The main purpose of my example was to convince fans of static type checking as done in most existing OO languages that these type systems are not powerful enough to describe relatively simple, useful programs (and preserve static type safety), and that OO language designers should incorporate more powerful type systems if they really want to claim that their type systems do not reduce expressive power over what exists naturally in dynamically-typed OO languages. -- Craig Chambers
new@ee.udel.edu (Darren New) (04/27/91)
In article <ROCKWELL.91Apr25193638@socrates.socrates.umd.edu> rockwell@socrates.umd.edu (Raul Rockwell) writes: >If C++ is strongly typed because of the lack of this error, then so is >machine language. I'm not sure I see the point of calling this >property "strongly typed". Machine language is weakly and dynamically typed. C++ is (mostly) strongly statically typed. They both have similar effects on "message not understood" errors. Isn't "segmentation violation" a "message not understood" message? It all depends on how you look at it. From the point of view of the programmer who didn't expect this error, this is a type error (e.g., that "mov.l (a4)+,d0" didn't put a long into d0). From the point of view of the OS, usually only bus errors trying to access the interrupt vector are "undefined" resulting usually in a CPU halt which can only be recovered by a reset. >My own definition of "strongly typed" was that the language will not >return a result for applying a function to values which are outside >its domain. Note that except for trivial cases you most definitely >can get "domain errors" (or "message not understood") at runtime. Sounds like a good definition. I'll give some examples below. >Now, I understand that classic works have claimed that a type error is >a value which puts the program in an infinite loop. How else are you going to "not return a value"? >However, I would >say that a language where this happens is weakly typed. In fact, I >think that from this point of view, a "strongly typed" language is one >which only allows finite looping constructs, and which guarantees a >well-behaved "run-time error" whenever a partial function is applied >incorrectly (or maybe we should call this "absolutely typed"?). Terrible example. Smalltalk is "strongly typed" and when you get a type error, the message call does not return any value; instead, it goes into an infinite loop reading the keyboard and interpreting what the debugger says to do and so on. Why restrict yourself to finite looping constructs? Why not just guarantee a well-behaved "run-time error"? Of course, this gets kind of hairy, because the computer never really gets into an infinite loop, so some value is always returned somewhere (unless the computer can never ever be made to work again, at which point the question again appears moot). Hence, when you say "doesn't return a value" you have to clarify it. If I catch "message not understood" have I returned a value or have I had a type mismatch or both? This is part of the confusion in this discussion. Let's use these definitions, or at least choose *some* definitions before we start another round of "yes it is"/"no it isn't". (Somebody want to save these so I don't have to keep reposting the definitions?:-) Dynamic typing (one more time for the expiration-impaired :-): syntactic elements (like variables or expressions) do not have types. Static typing: syntactic elements (like variables or expressions) do have types and these types can be determined at compile time. It doesn't matter whether the use specifies the types implicitly or explicitly or a combination of both. It *does* matter that each variable is supposed to hold one type of data only, and the representation of that data is assumed to be known at compile time. Strong typing: values of the wrong type cannot be stored into accessors (i.e., lvalues, function parameters, etc) and functions may not be applied to values outside of their domain without a compiletime or runtime error. (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.) Values of the wrong type are assumed to possibly have incompatible representations; i.e., valid integers may not be valid floats, etc. Weak typing values of the wrong type can be stored into accessors and/or functions may be applied to values outside their range without an immediately detectable error. Examples of all four combinations: Static weak typing: K&R (pre-ANSI C) Array subscripting, bad pointers, passing int's as float's into separately compiled functions, etc, etc, etc are all not caught, but each and every syntactic value-carrying expression (function calls, variables, etc) has a declared or determinable type. Static strong typing: Modula-3 (safe subset) There are no operations (supposedly) which cause the wrong type of value to be stored into a variable; variables are initialized to legal values; dangling pointers cannot dangle, etc. Dynamic weak typing: Most machine languages (as seen from the OS point of view) The same memory location can hold both integers or addresses, and checks are not made that the value is used in the right way. Dynamic strong typing: Smalltalk Every operation returns a defined result for every value, yet no variable or function needs to know the "type" it will hold, explicitly or implicitly. (Note again that "message not understood" in Smalltalk is a defined catchable error and therefore returns a value.) -- --- 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 +=+
new@ee.udel.edu (Darren New) (04/27/91)
In article <554@eiffel.UUCP> bertrand@eiffel.UUCP (Bertrand Meyer) writes: >by craig@leland.Stanford.EDU (Craig Chambers): >> Here's the problem: we'd like to describe the type of the min >> function >one could define `min' in that class as > min (other: like Current): like Current is Doesn't look like you've answered the question here. What's the type of `min'? All you've shown is how Eiffel can express restrictions on the patterns of inputs that min can accept and the type that min will return given certain input types. You have not said what the type of min is. In Smalltalk, I can say Class Mary method zelda: thing code ^ thing and say that the zelda: message will always return the same type as its argument. That doesn't make Smalltalk statically typed. I'm not bashing Eiffel. I don't even know Eiffel. Maybe the response would be obvious if I *did* know Eiffel. But so far, it looks like `min' is a dynamically-typed function. (Either that, or it is a polymorphic function, at which point the *declaration* is dynamically typed and the *application* is statically typed; i.e. "min(other : like Current)" is dynamically typed, but "min(3,5)" is statically typed as an integer and "min(<<3,4>>,<<5,6>>)" is statically typed as a list.) -- Darren -- --- 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 +=+
bertrand@eiffel.UUCP (Bertrand Meyer) (04/29/91)
In <554@eiffel.UUCP> I offered a straightforward Eiffel solution to Craig Chambers's problem, supposedly intractable by typed languages. In <51986@nigel.ee.udel.edu>, new@ee.udel.edu (Darren New) replies: [Quoting from my solution]: >> one could define `min' in that class as >> min (other: like Current): like Current is [His comment]: > Doesn't look like you've answered the question here. What's the > type of `min'? Now let us repeat patiently: the type of `min' is `like Current'. `like' is an Eiffel keyword whose meaning was explained in my message, and the corresponding typing mechanism (declaration by association) is makes static typing possible in practice. Thank you for your attention. > I don't even know Eiffel. Maybe the response would > be obvious if I *did* know Eiffel. It is generally considered preferable to know first and then criticize. But it is never too late to know. Here now is the response by Craig Chambers: > > Eiffel's rules allow this to be type checked by having broken type > checking rules, in my opinion. Covariant type-checking rules do not > enure type safety statically (you mention this towards the end of your > message). The newer proposed rules (as yet unimplemented, I believe) > do ensure type safety statically, but by effectively enforcing a > contravariant typing discipline which then prevents this example from > being type checked. I suspect that the new type checking rules will > never actually be implemented and widely adopted since they will > disallow many existing Eiffel programs which have relied on the > covariant type checking rule. > > The main purpose of my example was to convince fans of static type > checking as done in most existing OO languages that these type systems > are not powerful enough to describe relatively simple, useful programs > (and preserve static type safety), and that OO language designers > should incorporate more powerful type systems if they really want to > claim that their type systems do not reduce expressive power over what > exists naturally in dynamically-typed OO languages. I have quoted this text in full because I can't repress a feeling of admiration for the skill it takes to accumulate so many misrepresentations in so few lines. To call Eiffel's rules ``contravariant'', for example, is a quite remarkable achievement. This forum has seen the same claims made time and again, and time and again rebuked, but whenever you cut the dragon's head a new one grows back. Rational debate is useless; dynamic typing is good, and static typing is at once bad, useless, and impossible. I have always felt sympathy towards the biologists who accept to debate creationists. Now I also understand them better; one can fight opinions, not articles of faith. Not having the infinite amount of both time and patience which it would take to continue, I quit, declaring total rhetorical defeat. -- -- Bertrand Meyer Interactive Software Engineering Inc., Santa Barbara bertrand@eiffel.com
rick@tetrauk.UUCP (Rick Jones) (04/29/91)
In article <556@eiffel.UUCP> bertrand@eiffel.UUCP (Bertrand Meyer) writes: BM>In <554@eiffel.UUCP> I offered a straightforward Eiffel solution to BM>Craig Chambers's problem, supposedly intractable by typed languages. BM> BM>Here now is the response by Craig Chambers: CC> Eiffel's rules allow this to be type checked by having broken type CC> checking rules, in my opinion. Covariant type-checking rules do not CC> enure type safety statically (you mention this towards the end of your CC> message). The newer proposed rules (as yet unimplemented, I believe) CC> do ensure type safety statically, but by effectively enforcing a CC> contravariant typing discipline which then prevents this example from ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ !?! CC> being type checked. I suspect that the new type checking rules will CC> never actually be implemented and widely adopted since they will CC> disallow many existing Eiffel programs which have relied on the ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ !?! CC> covariant type checking rule. CC> CC> The main purpose of my example was to convince fans of static type CC> checking as done in most existing OO languages that these type systems CC> are not powerful enough to describe relatively simple, useful programs CC> (and preserve static type safety), and that OO language designers CC> should incorporate more powerful type systems if they really want to CC> claim that their type systems do not reduce expressive power over what CC> exists naturally in dynamically-typed OO languages. BM>I have quoted this text in full because I can't repress a feeling of BM>admiration for the skill it takes to accumulate so many BM>misrepresentations in so few lines. To call Eiffel's rules BM>``contravariant'', for example, is a quite remarkable achievement. BM> BM>Not having the infinite amount of both time and patience which BM>it would take to continue, I quit, declaring total rhetorical BM>defeat. I have avoided getting embroiled in this debate as I feel it has been rather academic, and, like Bertrand, I don't have infinite time & patience. However, the above attack on Eiffel's new type-checking system embodies so many misunderstandings I feel compelled to take up the cause. There have been a number of passing criticisms of the concept, all of which have shown a lack of understanding, but failed to discuss the issue in any depth. Although I am usually averse to acronymns, I don't want to write "extended type checking" or the like any more than I have to, so for now I shall christen it "Global Type Analysis", or GTA for short (ETC sounds too trivial :-). The following explains why it can in fact work. Fact: A program is type-safe if no feature is ever called on an object which does not support that feature. The problem is how to establish the truth of this. The extremes are either a completely unbreakable, simple static type system, or dynamic typing. The former is so strict it is unusable for non-trivial applications. The latter requires 100% branch coverage testing, or total static data-flow analysis, both of which are either impossible or impractical. They also require an embedded run-time error trap system. The compromise is GTA. To understand what GTA does, it is useful to consider the idea of a partial type. Static type systems are always discussed in terms of complete types - i.e. the type of an object is defined by the total set of features which it supports. However, an object can also be considered as having a number of partial types, represented by all the possible subsets of its features. Each of these partial types is clearly a supertype of the complete type, or if you prefer the other way, the complete type conforms to each of the partial types. E.g. if object A supports features F, G, & H, then we can draw an implicit partial type tree as follows: F G H |\ /|\ /| | \ / | \ / | | F,G | G,H | | | | | | |____|____|____|____| | F,G,H The total number of partial types is a function of the total number of features, using the formulae from combination theory (which off the top of my head I forget :-). If we now consider a class variable in a program (i.e. one which can refer to an object, whose actual type is dynamic), that variable has an IMPLICIT type. The implicit type is defined by the set of features which are actually coded as called from that variable. This is true regardless of whether the language is statically or dynamically typed. If the language is statically typed, then the variable also has an EXPLICIT type; this is the complete type of the class for which it is declared. Simple static type checking will guarantee that the implicit type is a supertype of the explicit type. E.g. if class A exports the features F, G, & H, then the declaration (Eiffel style): var: A defines var with an explicit type F,G,H. If the only code which uses var if of the form: var.F; var.G; i.e. there is no occurrence of var.H, then the implicit type of var is F,G. By contrast, the whole basis of a dynamically typed language is that all variables are implicitly typed by their usage - there are no explicit types. The "holes" in Eiffel's current type system, pricipally resulting from covariance, are that it may allow var to refer to an object which is a supertype of A. However, var's implicit type is also a supertype of A. Provided no object is ever attached to var which is a supertype of var's IMPLICIT type, then the system is type-safe. This analysis is statically feasible, and is what GTA sets out to do. The total effect is not a lot different from running a test with 100% branch coverage. Suppose in the above example, as part of a complete program, GTA detected that an object could be assigned to var which did not support feature G - it would generate a compile-time error. The same scenario would only be safe in a dynamically typed language if the code guaranteed never to call G at the times when var referred to the offending object. This implies that there would be code which tested that object's actual type, and behaved accordingly. This is contrary to all the principles of object oriented design, and suggests that the program should be re-written. Note that it does NOT mean that feature G can never be called on any object which may at some time be attached to var. It simply means that feature G must be applied to those objects which support it via some other variable which never references objects which don't support G. It should also be noted that GTA resolves the infamous polygon/rectangle problem. Here we have a class POLYGON, whose number of vertices can be altered. A descendant of POLYGON is RECTANGLE, which is intuitively a sub-type, but clearly must have a fixed number of vertices. Thus RECTANGLE inherits POLYGON, but does not export the add_vertex feature (and probably some other non-applicable ones as well). The effect in terms of types is that RECTANGLE is not a subtype of POLYGON is terms of complete types, but it is a subtype of a particular set of POLYGON partial types - those which exclude the features inapplicable to rectangles. Thus a variable of type POLYGON may safely have a RECTANGLE object assigned to it provided the implicit type of the variable is a supertype of RECTANGLE. A program which includes an assignment of a RECTANGLE object to a POLYGON variable of an invalid implicit type will be caught be the GTA system. This quite clearly does not "reduce Eiffel's type system to contravariance", but allows covariance to be used completely safely. It is worth noting that Craig Chambers' "hard problem" is only irresolvable in a static type system if you demand contravariance (which he did in his initial posting) - but then most problems are irresolvable in a useful way with contravariance. His point really seems to be that static type checking with covariance isn't type checking at all, so dynamic typing is better. However, GTA allows covariant flexibility combined with static checking, which in fact checks exactly the same things that a dynamically typed language checks at run-time. I do not wish to claim that "static typing is better than dynamic typing", since such wars are futile - both forms have a useful place. However, such debate should focus on useful differences, not on prejudice and dogma. As a footnote, I have written a lot of code in Eiffel over the last year or so, with extensive use of genericity and polymorphism, and I have NEVER encountered a covariance-induced type failure. I would be extremely surprised if GTA objected to any existing, reliably working Eiffel programs - if it did, they would have shown up run-time failures by now. -- Rick Jones, Tetra Ltd. Maidenhead, Berks, UK rick@tetrauk.uucp Any fool can provide a solution - the problem is to understand the problem
dl@g.g.oswego.edu (Doug Lea) (04/29/91)
[I attempted to post this 3 months ago in reply to a similar posting about contravariance, etc., but apparently the posting never made it out. Now seems as good a time as any to try again.] Bertrand Meyer wrote: > The question represents an attempt on my part to understand > how the contravariant rule (which may at first be theoretically > appealing because it makes type checking easier) can be made to > work at all in practice. I don't think the solution is all that complicated or even controversial. > Assume the following situation [Example recast in a C++-ish form -- Sorry (especially since C++ doesn't have any any useful rules about contra- or co- variant arguments), but I don't know Eiffel syntax well enough. I also gave `Register' a return value to make it easier to distinguish the cases.] The contravariance-breaking declarations look like: class Driver { ... }; class Professional_Driver : public Driver {...}; class Vehicle { virtual int Register(Driver& d) { return 0; } }; class Truck : public Vehicle { virtual int Register(Professional_Driver& p) { return 1; } }; The first question to ask in finding a contravariance-conforming strategy is what behavior you want in each of the following situations, assuming Driver d, Professional_Driver p, Vehicle v, and Truck t: [1] v.Register(d); [2] v.Register(p); [3] t.Register(d); [4] t.Register(p); Most likely, you want cases [1], [2], and [3] to invoke Vehicle::Register, and case [4] to invoke Truck::Register. Since this dispatch pattern depends on the types of two kinds of objects, the way to express it is through some form of multiple dispatch. In a language directly supporting multiple dispatch (e.g., CLOS), it might be stated in this way: class Driver { ... }; class Professional_Driver : public Driver {...}; class Vehicle {...}; class Truck : public Vehicle {...}; int Register(Vehicle& v, Driver& d) { return 0; } int Register(Truck& t, Professional_Driver& p) { return 1; } This would be handled in the intended manner by CLOS-type resolution and dispatch rules (which are implictly contravariance maintaining when the functions are of this form.) (Note: this is valid in C++ too, but overload resolution is only done statically, so it doesn't always have the desired effect.) But this resolution strategy can also be obtained with `manual' double dispatch in other languages (including, finally, C++ and Eiffel), to look something like class Driver { virtual int RegisterVehicle(Vehicle& v) { return 0; } virtual int RegisterTruck(Truck& t) { return RegisterVehicle(t); } }; class Professional_Driver : public Driver { virtual int RegisterTruck(Truck& t) { return 1; } }; class Vehicle { virtual int Register(Driver& d) { return d.RegisterVehicle(*this); } }; class Truck : public Vehicle { virtual int Register(Driver& d) { return d.RegisterTruck(*this); } }; which is legal, does what you want, and obeys contravariance. You can always do this conversion mechanically (algorithmically). A perfectly valid objection is that people don't want to have to do conversion into double dispatch themselves, especially since the definition of one special case involves 3 other classes besides the one programmers have in mind. I agree with this objection. Languages and their compilers should help automate this. The CLOS generic function approach is one attractive method to do this in C++-like and Eiffel-like langauges. -- Doug Lea dl@g.oswego.edu || dl@cat.syr.edu || (315)341-2688 || (315)443-1060 || Computer Science Department, SUNY Oswego, Oswego, NY 13126 || Software Engineering Lab, NY CASE Center, Syracuse Univ., Syracuse NY 13244
new@ee.udel.edu (Darren New) (04/30/91)
In article <556@eiffel.UUCP> bertrand@eiffel.UUCP (Bertrand Meyer) writes: > > Doesn't look like you've answered the question here. What's the > > type of `min'? > >Now let us repeat patiently: the type of `min' is `like Current'. >`like' is an Eiffel keyword whose meaning was explained in my message, >and the corresponding typing mechanism (declaration by association) >is makes static typing possible in practice. Thank you for your attention. Yup. I caught that. What's the type of Current? If "Current" might be an integer when the call is "min(4,6)" and "Current" may be a list when the call is "min(<<3,4>>,<<5,6>>)" then it looks to me like the single definition of "min" specifices that "min" shall return different types on different calls. Whether you call this "dynamic typing" or "static typing" or "automatic polymorphism" or "generics" or what is beside the point. In the definition most of us have been using, "dynamic typing" means that syntactic elements don't have types. Here, it seems to me that the syntactic element "min" has a type which changes depending on the arguments on the rest of the line of text representing the functional application. It looks to me as tho the *declaration* is dynamically typed and the *application* is statically typed. This is one of those inbetweens for which I have not heard a good buzzword. > > I don't even know Eiffel. Maybe the response would > > be obvious if I *did* know Eiffel. >It is generally considered preferable to know first and then criticize. What criticism? I merely asked you to clarify the type of "min". To define a type by saying it is "like current" and then define "like" but not "current" does not illuminate me to the point where I fully understand the ramifiations of why it *isn't* dynamic typing. I really don't care whether Eiffel is dynamically or statically typed. >But it is never too late to know. That is certainly true. >This forum has seen the same claims made time and again, and time and >again rebuked, but whenever you cut the dragon's head a new one >grows back. Rational debate is useless; dynamic typing is good, >and static typing is at once bad, useless, and impossible. You mean, debate that disagrees with you. I think that most of the discussion has been beneficial at least to me. Just beause you claim that static typing is all you ever need doesn't mean it is so. Just because somebody claims that dynamic typing is better doesn't make it so. "Rebukes" are generally ineffective when the pperson rebuking is in a different situation than the person whose beliefs are being rebuked. (See, for example, the "formal semantics" thread; people who communicate with others a lot tend to like formal semantics more than those who just try to get something out. Formalisms themselves are neither good nor bad in and of themselves.) Besides, I still haven't seen a good example of how to do hetrogeneous lists in a statically-typed language. >I have always felt sympathy towards the biologists who accept >to debate creationists. Now I also understand them better; >one can fight opinions, not articles of faith. >Not having the infinite amount of both time and patience which >it would take to continue, I quit, declaring total rhetorical >defeat. That's funny. I don't argue to "win". I argue to "learn", whether it be to learn what your faith is, or to learn how you came to a rational decision. Even when I finish an argument I've "won" or "lost" or didn't really finish at all, I usually manage to keep an open enough mind that I might admit that the other side *could* have *some* validity to their claims, and thereby expand my own horizons. By not assuming that since the other side doesn't agree then they must be working on blind faith, I find that I often manage to converse long enough to get something out of the conversation, if only a better understanding of how to deal with people stuck in a blind-faith trap. Of course, we are all busy. I have no time to learn Eiffel right now (especially as it does not seem to present any truely novel-to-me concepts), and you may not have time to continue this argument. I accept and respect that. Have fun! -- Darren -- --- 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 +=+
boehm@parc.xerox.com (Hans Boehm) (05/01/91)
rick@tetrauk.UUCP (Rick Jones) writes: >... It is worth noting that >Craig Chambers' "hard problem" is only irresolvable in a static type system if >you demand contravariance (which he did in his initial posting) - but then most >problems are irresolvable in a useful way with contravariance... Craig Chambers' problem is resolvable in at least some statically typed languages, as is the Polygon-Rectangle example. There are elegant solutions that don't involve inheritance at all. See the discussion in comp.object. (There may also be some that do use inheritance. I'm less of an expert on those. But I haven't seen any discussion of the more aggressive type systems that incorporate inheritance, but obey the contravariance rule, e.g. Cardelli's Quest, or Cook's system.) The original sentence strikes me as a substantial overgeneralization. The problem appears to be unsolvable in a straightforward way using a version of Eiffel's type system that enforces contravariance. Nothing else has been established. Hans (boehm@xerox.com) Usual disclaimers ...
craig@leland.Stanford.EDU (Craig Chambers) (05/01/91)
In article <1146@tetrauk.UUCP>, rick@tetrauk.UUCP (Rick Jones) writes: |> The "holes" in Eiffel's current type system, pricipally resulting from |> covariance, are that it may allow var to refer to an object which is a |> supertype of A. However, var's implicit type is also a supertype of A. |> Provided no object is ever attached to var which is a supertype of var's |> IMPLICIT type, then the system is type-safe. This analysis is statically |> feasible, and is what GTA sets out to do. I don't think you are describing the proposal to fix Eiffel's typing rules, at least as I understand it. Bertrand has explicitly stated that he isn't proposing complete flow analysis of the program to detect type errors. If there is a call to feature F *anywhere in the program* then the type checker assumes that feature F will be called for any variable declared to be a type that includes F. This then prevents the program you are describing to type-check (assuming that all three features of the declared type in your example are called somewhere in the program). Put another way, the type system you describe completely ignores the declared types of variables, using interprocedural flow analysis to compute what you call the implicit type of a variable; see the above quote for an example (the explicit type of "var" is never used). Although I like the results of this kind of type system (nearly all legal programs will type check with little effort on the part of the programmer), I don't believe that the necessary flow analysis is particularly feasible. The Typed Smalltalk people do include a type-checking system that uses flow-sensitive analysis like you describe (abstract interpretation of the program in the type domain), but the algorithm is exponential (double-exponential?) in the worst case. |> It should also be noted that GTA resolves the infamous polygon/rectangle |> problem. Here we have a class POLYGON, whose number of vertices can be |> altered. A descendant of POLYGON is RECTANGLE, which is intuitively a |> sub-type, but clearly must have a fixed number of vertices. Thus RECTANGLE |> inherits POLYGON, but does not export the add_vertex feature (and probably some |> other non-applicable ones as well). The effect in terms of types is that |> RECTANGLE is not a subtype of POLYGON is terms of complete types, but it is a |> subtype of a particular set of POLYGON partial types - those which exclude the |> features inapplicable to rectangles. Thus a variable of type POLYGON may |> safely have a RECTANGLE object assigned to it provided the implicit type of the |> variable is a supertype of RECTANGLE. A program which includes an assignment |> of a RECTANGLE object to a POLYGON variable of an invalid implicit type will be |> caught be the GTA system. No. If there is a call to add_vertex *anywhere in the program*, then *all* assignments of rectangles to polygons will be declared illegal by Eiffel's proposed type system. |> This quite clearly does not "reduce Eiffel's type system to contravariance", |> but allows covariance to be used completely safely. It is worth noting that |> Craig Chambers' "hard problem" is only irresolvable in a static type system if |> you demand contravariance (which he did in his initial posting) - but then most |> problems are irresolvable in a useful way with contravariance. I admit I was a bit hasty in my implication that Eiffel's new rules are nothing more than requiring contravariance. I should have said that the following rules will type-check the same programs, no more and no less, as Eiffel's new rules: 1) Remove all features that are never invoked in the program. 2) Construct a type hierarchy from the class hierarchy such that one class is a subtype of another iff it obeys the normal subtype conformance rules using contravariance. 3) Disallow all assignments in the program where an expression of one class is being assigned to a variable (or passed as a parameter) that is declared to be a class that's not a legal supertype. This phrasing of the rules make it easier to compare Eiffel's new type system with those of other languages, and highlights the fact that assignments from one type to another can only take place where normal contravariant subtyping rules would allow. This is only natural, since some form of these rules is necessary to allow static type safety. But it does pose problems for existing Eiffel programs that rely on covariant type checking (more akin to the implicit type checking that you describe). If I have misunderstood Eiffel's new rules (again), I'd appreciate being set straight. The easiest way to do that is to post an example program that will type-check under Eiffel's new rules that won't under the rules I've listed above. |> His point |> really seems to be that static type checking with covariance isn't type |> checking at all, so dynamic typing is better. However, GTA allows covariant |> flexibility combined with static checking, which in fact checks exactly the |> same things that a dynamically typed language checks at run-time. No, I'm saying that covariance (by itself) isn't statically type safe, so a better type system is needed. Some fairly powerful type systems have been developed for more theoretical languages and for functional languages, and I'm sure that one could be developed to handle the "min" example I posed. The main point is that current popular OO languages are a far cry from these type systems. -- Craig Chambers
rick@tetrauk.UUCP (Rick Jones) (05/01/91)
In article <1991Apr30.213115.9990@leland.Stanford.EDU> craig@self.stanford.edu writes: } In article <1146@tetrauk.UUCP>, rick@tetrauk.UUCP (Rick Jones) writes: } |> The "holes" in Eiffel's current type system, pricipally resulting from } |> covariance, are that it may allow var to refer to an object which is a } |> supertype of A. However, var's implicit type is also a supertype of A. } |> Provided no object is ever attached to var which is a supertype of var's } |> IMPLICIT type, then the system is type-safe. This analysis is statically } |> feasible, and is what GTA sets out to do. } } I don't think you are describing the proposal to fix Eiffel's typing } rules, at least as I understand it. We clearly have a different interpretation of the proposal. } Bertrand has explicitly stated } that he isn't proposing complete flow analysis of the program to } detect type errors. If there is a call to feature F *anywhere in the } program* then the type checker assumes that feature F will be called } for any variable declared to be a type that includes F. This is where we disagree. The proposal as I read it (I have just gone through my copy again) clearly relates the application of a feature to the variable used to apply it. Your interpretation would be no more complex to implement than the existing checker, just a lot more restrictive. If this were the case, I would also consider it to be unusable. } Put another way, the type system you describe completely ignores the } declared types of variables, using interprocedural flow analysis to } compute what you call the implicit type of a variable; see the above } quote for an example (the explicit type of "var" is never used). Not quite. The use of simple type conformance based on inheritance as a starting point enables the full type checking to be done without actually indulging in flow analysis. I will not attempt to formally justify this, as I am not a language theoretician; I am merely explaining my understanding of Bertrand Meyer's description of how it will work. } Although I like the results of this kind of type system (nearly all } legal programs will type check with little effort on the part of the } programmer), I don't believe that the necessary flow analysis is } particularly feasible. The Typed Smalltalk people do include a } type-checking system that uses flow-sensitive analysis like you } describe (abstract interpretation of the program in the type domain), } but the algorithm is exponential (double-exponential?) in the worst } case. This I can believe, but since Smalltalk starts off with no explicit types or simple static type conformance rules, this is the only way to work it out. I believe it _can_ be done in Eiffel, and without flow analysis per-se. Since we seem to be debating different understandings of Bertrand Meyer's description, perhaps the simplest thing would be for Bertrand to comment on which of us (if either!) has got it right. -- Rick Jones, Tetra Ltd. Maidenhead, Berks, UK rick@tetrauk.uucp Any fool can provide a solution - the problem is to understand the problem
mario@cs.man.ac.uk (Mario Wolczko) (05/02/91)
In article <1146@tetrauk.UUCP>, rick@tetrauk.UUCP (Rick Jones) writes: > Fact: A program is type-safe if no feature is ever called on an object which > does not support that feature. [description of GTA with example deleted] > supertype of A. However, var's implicit type is also a supertype of A. > Provided no object is ever attached to var which is a supertype of var's > IMPLICIT type, then the system is type-safe. > This analysis is statically feasible, and is what GTA sets out to do. ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Nonsense. It is easy to construct a program which is type-safe by your definition but cannot be verified as type-correct by static analysis. If you could verify all such programs, you would have solved the Halting Problem. Consider this program in a dynamically-typed language: var X; if predicate1 then X := L1; /* L1 is an object that has feature F */ else X := L2; /* L2 is an object that does not have feature F */ fi X.F; There is no way at compile time to tell whether this program is type-safe or not. Predicate1 could invoke an artbirary amount of computation, but always result in "true". It could be based on user input (isodd(readnum())), which cannot be foreseen. There will always be programs that are type-safe, but cannot be verified as type-safe by a static type system. Mario Wolczko ______ Dept. of Computer Science Internet: mario@cs.man.ac.uk /~ ~\ The University uucp: mcsun!ukc!man.cs!mario ( __ ) Manchester M13 9PL JANET: mario@uk.ac.man.cs `-': :`-' U.K. Tel: +44-61-275 6146 (FAX: 6236) ____; ;_____________the mushroom project___________________________________
craig@leland.Stanford.EDU (Craig Chambers) (05/02/91)
In article <1150@tetrauk.UUCP>, rick@tetrauk.UUCP (Rick Jones) writes: |> We clearly have a different interpretation of the proposal. |> |> In article <1991Apr30.213115.9990@leland.Stanford.EDU> craig@self.stanford.edu writes: |> } Bertrand has explicitly stated |> } that he isn't proposing complete flow analysis of the program to |> } detect type errors. If there is a call to feature F *anywhere in the |> } program* then the type checker assumes that feature F will be called |> } for any variable declared to be a type that includes F. |> |> This is where we disagree. The proposal as I read it (I have just gone |> through my copy again) clearly relates the application of a feature to the |> variable used to apply it. Your interpretation would be no more complex to |> implement than the existing checker, just a lot more restrictive. If this were |> the case, I would also consider it to be unusable. I just finished reading through my copy again, and I think I have to retract what I said about Eiffel's new rules. There is some sort of analysis more precise than "any assignment in the program" that Bertrand calls "alias analysis" in the proposal. This analysis tracks which variables have been assigned to which other variables or formal parameters, and then does checking of feature application based on the statically declared types of any variable/parameter which could be assigned/passed to the receiver of the message and the parameter to the message. It's not as precise as the Typed Smalltalk type inference and checking algorithm, though. I don't know if your GTA is closer to (my new interpretation of) Bertrand's proposal or to the Typed Smalltalk approach. It's hard for me to guess what the results of Bertrand's proposal are likely to be in practice. Will most Eiffel programs type-check, or will most not type-check (in the interesting cases)? It's hard to say. It's also hard for me to say how long the alias analysis will take in practice. Since these rules are much more complex than my earlier interpretation of them, I'm no longer sure that they guarantee static type safety, either. |> Since we seem to be debating different understandings of Bertrand Meyer's |> description, perhaps the simplest thing would be for Bertrand to comment on |> which of us (if either!) has got it right. I think that's probably a wise idea. But I wish there were some more illustrative discussion of these new typing rules, complete with examples. Perhaps this will be included in the new Eiffel language book? To relate these last few messages then to the subject line, I'm no longer sure whether Eiffel's new rules will handle the "min" example. -- Craig Chambers
bertrand@eiffel.UUCP (Bertrand Meyer) (05/02/91)
First I would like to thank Rick Jones for a very clear expose of system-level type rules, and Craig Chambers for not overreacting to my somewhat overreacting response to his message. That was very classy of him. I forgot my Net Rule #1 - if you are going to post anything negative, let a night pass first. True, I was rather irritated by Mr. Chambers's message, since I had the impression that it ignored my earlier answer and was starting on the old route again. But then Rule #2 says either you don't join the net or you have to accept that repeating things is part of the game. I apologize for the heated reaction. (What worries me is that I did not receive the usual hate mail this time, only one gentle note of reproach; am I doing something wrong?) Now about message <1991May1.194620.1141@leland.Stanford.EDU> by craig@leland.Stanford.EDU (Craig Chambers): [!! indicates Mr. Chambers's quotations from message by Rick Jones. Question numbers in square brackets added by BM.] > It's hard for me to guess what the results of [system-level checking] are > going to be in practice. [1] Will most Eiffel programs type-check, or > will most not type-check (in the interesting cases)? It's hard to > say. [2] It's also hard for me to say how long the alias analysis will > take in practice. Since these rules are much more complex than my > earlier interpretation of them, I'm no longer sure that they guarantee > static type safety, either. > !! [3] Since we seem to be debating different understandings of Bertrand Meyer's > !! description, perhaps the simplest thing would be for Bertrand to comment on > !! which of us (if either!) has got it right. > I think that's probably a wise idea. [4] But I wish there were some more > illustrative discussion of these new typing rules, complete with > examples. [5] Perhaps this will be included in the new Eiffel language > book? > [6] To relate these last few messages then to the subject line, I'm no > longer sure whether Eiffel's new rules will handle the "min" example. Some partial answers: [1] I am convinced that 99.5% of Eiffel systems will typecheck under the complete rules. (I don`t like to talk about the ``new rules'' because for me they were always there implicitly, although not completely stated.) The 0.5% that will not typecheck will be rejected because of actual inadequacies which could have led to incorrect situations at run time; full checking will thus be beneficial in this case. [2] Clearly we are working hard to make the full type analysis very efficient. I'd rather refrain from any more boasting until we have actual timing figures to announce, but I am very optimistic. [3] I think Rick Jones has presented a quite clear picture of the system-level type validity rules. [4] Yes, there is a need for more examples. I have tried to be as clear as possible in the chapter on Type Checking in the forthcoming revised version of ``Eiffel: The Language''. I'd like to be able to extract a subset of that chapter and post it on comp.lang.eiffel, but frankly I don't see how I can find the time to do this in the next few weeks. On the other hand, the paper ``Static Typing for Eiffel'', which was posted twice (either on comp.object or comp.lang.eiffel, I forgot), presents a reasonably coherent view in spite of a few material errors. (I have not published that paper in a widely available printed form because I couldn't think of a publication or conference that would have accepted it. It is part of a book that our company distributes, ``An Eiffel Collection''.) [5] Yes, to some extent. See above. [6] The complete rules certainly handle the `min' example. Don't forget, they are the same as the old rules; they simply exclude certain erroneous cases which would have escaped the incomplete rules. But they certainly don't limit the expressive power of the language. Let me expand. (Since my earlier message conceded defeat, just consider this as just playing for sheer fun once the ball game is over.) My fundamental disagreement with Mr. Chambers is that I do *not* think the problem of static vs. dynamic typing is one of expressive power. If the type system has been designed properly then types help you, rather than constraining you. They make your software much more clear (through declarations, i.e. useful redundancy); they help the compiler generate good code; and they enable a static checker (usually a part of the compiler) to catch errors early rather than late in the development cycle. This is only true, of course, if the type system is complete enough; this means the presence of genericity, constrained and unconstrained, of the reverse assignment attempt for forcing a type on a known object, and of anchored declarations (the `like something' type construct). Without these mechanisms, static typing in an object-oriented language is, as believe, either impossible or simply a joke (as in C extensions when you spend your time casting back and forth between pointer types). Furthermore, although this is more controversial, I am convinced by my experience, confirmed by that of many Eiffel users and by the absence of any practical argument to the contrary, that for typing to work in practice with inheritance requires a covariant redefinition policy. If the mathematical models for contravariance are simpler, then that's too bad for mathematics. Denotational semantics 0, software engineering 1. (By the way I love denotational semantics, even wrote a book on it, but I believe that scientists should build theories to fit the practice, not the other way around.) As a consequence I believe that *conceptually* a good statically typed O-O languages is *always* better than a dynamically typed one, because you don't lose anything: if what you want is a fast, non-type-checking interpreter or compiler, then you can always build one for a statically typed languages; programmers then won't lose anything as compared to Smalltalk or CLOS, save for the effort needed to write a few declarations, which they'll probably find helpful anyway. But the reverse is not true: if you have a dynamically typed language, you will *never* be able to write a type checker for it because it would lack the necessary information. (ML fans might disagree here, but we'll have to wait until they have produced OOML.) Does this mean that static typing is always good and dynamic typing always bad? (I can hear the rumblings: who is the creationist here?) The answer would be yes except for one strong argument in favor of dynamically typed languages: they can be processed very quickly, enabling developers to try out new ideas without the interference of a static type checker, which may take some time to perform its duties. If speed of development is more important than reliability and efficiency of the resulting product, this makes dynamically typed languages attractive if they are backed by tools ensuring a fast turnaround. In other words, I don't think, as Mr. Chambers does, that the static vs. dynamic debate is a conceptual discussion at all. Conceptually, static wins hands down every time. What the debate is about is much more mundane: It's purely a question of implementation. If we were able to build static checkers that were totally unobtrusive performance-wise, and did their work in - say - ten seconds after a comparatively small change even to a very large system, then who in the world would forsake the extra benefits of type checking? Solving this problem - that is to say, a Very Fast Reexecution Cycle, comparable to the change-to-reexecute cycle of the best interpreters, without sacrificing any of the fantastic advantages of full type checking - has been our obsession for several years. We are convinced we now have the technology to do it, but no one has to believe this until the day it's out on the desks of Eiffel users. You can count on us for not sparing our time to make this happen as quickly as possible, and for not being too shy about it then. -- -- Bertrand Meyer Interactive Software Engineering Inc., Santa Barbara bertrand@eiffel.uucp
rick@tetrauk.UUCP (Rick Jones) (05/02/91)
In article <boehm.673043278@siria> boehm@parc.xerox.com (Hans Boehm) writes: } rick@tetrauk.UUCP (Rick Jones) writes: } >... It is worth noting that } >Craig Chambers' "hard problem" is only irresolvable in a static type system if } >you demand contravariance (which he did in his initial posting) - but then most } >problems are irresolvable in a useful way with contravariance... } The original sentence strikes me as a substantial overgeneralization. The } problem appears to be unsolvable in a straightforward way using a version of } Eiffel's type system that enforces contravariance. Nothing else has been } established. Criticism accepted - I was assuming a context of types related by inheritance, which was the general context of the discussion. The statement was not intended to be as sweeping as it might sound. -- Rick Jones, Tetra Ltd. Maidenhead, Berks, UK rick@tetrauk.uucp Any fool can provide a solution - the problem is to understand the problem
rick@tetrauk.UUCP (Rick Jones) (05/02/91)
In article <1991May1.194620.1141@leland.Stanford.EDU> craig@self.stanford.edu writes: > [ ... ] >I wish there were some more >illustrative discussion of these new typing rules, complete with >examples. Perhaps this will be included in the new Eiffel language >book? I can't say for certain, but I have just received some personal mail from Bertrand Meyer in which he mentions that he has been extremely busy just recently finishing the book (which probably explains his lack of patience!). It should be available very soon now - there are apparently a lot of advance orders for it. In the meantime, I shall try to compose an illustrative example which will explain the solution as I see it. >To relate these last few messages then to the subject line, I'm no >longer sure whether Eiffel's new rules will handle the "min" example. I think it can, but I guess we shall have to wait and see. -- Rick Jones, Tetra Ltd. Maidenhead, Berks, UK rick@tetrauk.uucp Any fool can provide a solution - the problem is to understand the problem
cjeffery@optima.UUCP (Clinton Jeffery) (05/02/91)
From article <566@eiffel.UUCP>, by bertrand@eiffel.UUCP (Bertrand Meyer): > If we were able to build static checkers that were totally > unobtrusive performance-wise, and did their work in - say - > ten seconds after a comparatively small change even to a very large > system, then who in the world would forsake the extra benefits of type > checking? I would. I am not willing to type one keystroke (e.g. type declarations) more than I have to in order to satisfy your need for everyone to do so. What is this sweeping generalization doing here after your very nice concession to dynamically typed languages earlier in your post? The closest I am willing to come to your cumbersome world is to let my type inference system insert comments into my code when it notices I am using a variable for different types of values at different times. Keystrokes. How many keystrokes does it take me to solve my problem?
rockwell@socrates.umd.edu (Raul Rockwell) (05/02/91)
Bertrand Meyer: > But the reverse is not true: if you have a dynamically typed language, > you will *never* be able to write a type checker for it because it > would lack the necessary information. ... > In other words, I don't think, as Mr. Chambers does, that the static > vs. dynamic debate is a conceptual discussion at all. > Conceptually, static wins hands down every time. I disagree. Completely. If the language includes the empty function (one which can not be closed -- any value applied results in a "domain error" or "message not understood"), you have a very clear mechanism to express type errors. (any predicate which allows application of that function...) The main issue I see between static typing and dynamic typing is that static typing is, well.. static. The difference between static typing and dynamic typing is very analogous to the difference between evaluation to a constant, and evaluation to a function. Of course, what I call "dynamic typing" others may call "static typing" -- I'm still pondering the question of user defined types. [With sufficiently powerful primitive types, and sufficiently powerful function re-write capability, what does user defined typing buy you?] [[[ Actually, I'm struggling with some specific models for typing. Basically, I just haven't found a way of expressing user types that is as expressive as I'd like. Yet. ]]] Raul Rockwell
olson@juliet.ll.mit.edu ( Steve Olson) (05/02/91)
In article <2672@optima.cs.arizona.edu> cjeffery@optima.UUCP (Clinton Jeffery) writes: From article <566@eiffel.UUCP>, by bertrand@eiffel.UUCP (Bertrand Meyer): > If we were able to build static checkers that were totally > unobtrusive performance-wise, and did their work in - say - > ten seconds after a comparatively small change even to a very large > system, then who in the world would forsake the extra benefits of type > checking? Because static type checking mostly solves problems introduced by ... static typing. Now, if I'm forced to use static typing, there is no question that I would also want a good type checker. And I have no problem with the notion that as static type checkers go, Eiffel has a very good one. I would. I am not willing to type one keystroke (e.g. type declarations) more than I have to in order to satisfy your need for everyone to do so. What is this sweeping generalization doing here after your very nice concession to dynamically typed languages earlier in your post? Um, well, in my opinion, the extra keystrokes involved are the weakest of the arguments against static typing. I mean, the botom line isn't keystrokes, its total programmer effort. And of course, in many applications, machine effort must be considered also. I don't mind typing the declarations so much as I mind being forced to specify my data objects at the bits 'n' bytes level. ("32 or 64 bits, pal, thats all we got here, and you better not get 'em mixed up either!") -- -- Steve Olson -- MIT Lincoln Laboratory -- olson@juliet.ll.mit.edu --
guest@alfrat.uucp (Mr. Guest User) (05/03/91)
This is actually a slight detour from the main thread of this discussion but C'est la vie. In article <566@eiffel.UUCP> bertrand@eiffel.UUCP (Bertrand Meyer) writes: >covariant redefinition policy. If the mathematical models for >contravariance are simpler, then that's too bad for mathematics. >Denotational semantics 0, software engineering 1. >(By the way I love denotational semantics, even wrote a book on it, >but I believe that scientists should build theories to fit the practice, >not the other way around.) > Does this mean that there exists no formal description of Eiffel in terms of Denotational Semantics? If this is the case, what method is used to define the semantics of Eiffel (including the semantics of the type checking)? I have heard (correct me if I'm wrong) that the syntax of Eiffel is now Public Domain and assume that other vendors must be currently developing their own compilers. How can we be sure that implementations of Eiffel comply to Bertrand Meyers definition, I would hate to see Eiffel take the same road as PASCAL. For the record, I too am a fan of Denotational Semantics and also of Software Engineering, I'd like to see the score as Denotational Semantics 1, Software Engineering 1. Dave Cullen ...!unido!alfrat.uucp!dave
stephen@estragon.uchicago.edu (Stephen P Spackman) (05/03/91)
In article <51984@nigel.ee.udel.edu> new@ee.udel.edu (Darren New) writes: |Machine language is weakly and dynamically typed. C++ is (mostly) strongly I have to disagree. A good machine language (one with no Catch Fire & Burn instructions) for a machine without programmer-visible caching is both strongly and statically typed, simply by virtue of the fact that all consequences of a given machine state are defined. You are making the mistake of imagining that addresses and ints and so forth exist in object code; but they don't. Those are abstractions in your mind. Ultimately they are NOT represented in the machine model. Bits go here, bits go there, the memory holds bits and nothing else. The (only) data type is the bit.... It's kind of trivial and uninteresting, but if Smalltalk is strongly typed then so is machine language (and by the same argument: all zero possible mis-assignments are successfully trapped); and if C is statically typed then so is machine language (because bits are stored in bits and that's the whole story). |[...] Isn't "segmentation violation" a "message not understood" message? Nope, it's a perfectly sensible part of instruction execution that is used heavily in the implementation of operating systems, memory managers and so forth. |It all depends on how you look at it. [...] Therefore the phenomenon's not really there in the langauage.... I'm really not trying to be silly here. The fact that machines are strongly typed underlyingly is the thing that makes secure implementations possible. If something could happen to be in memory that wasn't a bit, no language layered above could ever have guaranteed behaviour... (which is why it's bad when the hardware fails - untrapped type violations then CAN occur.... :-). It's sensible to ask, then, how we can implement UNTYPED langauges on top of this typed substrate. My guess is it's because memory is finite.... Which is to say, it's done with smoke & mirrors. ---------------------------------------------------------------------- stephen p spackman Center for Information and Language Studies systems analyst University of Chicago ----------------------------------------------------------------------
strom@watson.ibm.com (Rob Strom) (05/03/91)
In article <OLSON.91May2145734@goneril.juliet.ll.mit.edu>, olson@juliet.ll.mit.edu ( Steve Olson) writes: |> |> Um, well, in my opinion, the extra keystrokes involved are the weakest of |> the arguments against static typing. I mean, the botom line isn't keystrokes, |> its total programmer effort. And of course, in many applications, machine |> effort must be considered also. I don't mind typing the declarations so much |> as I mind being forced to specify my data objects at the bits 'n' bytes level. |> ("32 or 64 bits, pal, thats all we got here, and you better not get 'em |> mixed up either!") |> The above isn't an argument against static typing. It's an argument against type systems which fail to be abstract and which therefore make representation visible as part of the type information. Static type systems lacking that property are immune from this criticism. (Insert subtle plug for our Hermes language here :-) A dynamic type system which gave run-time type errors when users tried to add 32 and 64 bit numbers together would be just as bad. -- Rob Strom, strom@ibm.com, (914) 784-7641 IBM Research, 30 Saw Mill River Road, P.O. Box 704, Yorktown Heights, NY 10958
ddean@rain.andrew.cmu.edu (Drew Dean) (05/04/91)
In article <OLSON.91May2145734@goneril.juliet.ll.mit.edu> olson@juliet.ll.mit.edu ( Steve Olson) writes: >In article <2672@optima.cs.arizona.edu> cjeffery@optima.UUCP (Clinton Jeffery) writes: > > I would. I am not willing to type one keystroke (e.g. type declarations) > more than I have to in order to satisfy your need for everyone to do so. > What is this sweeping generalization doing here after your very nice > concession to dynamically typed languages earlier in your post? > >Um, well, in my opinion, the extra keystrokes involved are the weakest of >the arguments against static typing. I mean, the botom line isn't keystrokes, >its total programmer effort. >-- Steve Olson >-- MIT Lincoln Laboratory >-- olson@juliet.ll.mit.edu I know that "functional language" is considered a dirty term in this group :-), but there seems to be a lot known about typing-systems in relation to them. Before following up to this message, why don't you look at, say, Ch. 7 of Field & Harrison's _Functional_Programming_, or read about the Standard ML type system (note that Standard ML has type-inference, so no extra typing is required, unless the compiler cannot infer the type itself, which is a rare event, although simple to program: fun f x y = x + y. Now + is defined for reals & integers, and the compiler needs to know the type of one operand (or both) or the result in order to type the expression). Note: I'm sure there are better references than Field & Harrison, that's just one that I happen to have on hand. A good question: how might the Standard ML type system be adopted to an OO world ? -- Drew Dean Drew_Dean@rain.andrew.cmu.edu [CMU provides my net connection; they don't necessarily agree with me.]