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)
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
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
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
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
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 <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
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