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&
craig@leland.Stanford.EDU (Craig Chambers) (04/22/91)
In article <3378@charon.cwi.nl> guido@cwi.nl (Guido van Rossum) writes: >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. I may not have made myself clear with the problem. I want a general type system that will handle examples like the one I posted. I am not interested in languages or type systems that have built-in data structures that solve this particular problem but do not generalize. It sounds from your reply that ABC falls into the second category, but since you didn't describe ABC's type system, I can't tell whether it is a generally useful solution to a large class of problems. What's the type (inferred, I guess) of the arguments to the min function? How does the compiler know that "<" in min will work? Does the compiler type-check each invocation of min separately (which would be sidestepping the issue) or does it really infer a type for min that's usable by all its callers? Part of the description of the problem implies to me that the type system should include some notion of subtyping and some notion of parameterized types. My (partially formed) solution also uses type variables and some notion of a type pattern (I'm not sure whether or not this is the same as a parameterized type; I'm leaning towards yes if I can overcome some annoying technical obstacles). If someone posts that some type system solves the problem, please also post enough information to give people a feel for the facilities in the type system that allow it to solve the problem. Thanks. -- Craig Chambers
dl@g.g.oswego.edu (Doug Lea) (04/22/91)
[Craig Chambers suggested I post this reply I sent him about the `min'
example for others to comment on. Here goes (in slightly edited form).]
Good example. Please bear with me while I meander toward one answer.
At first glance, you'd like to type min as something like
fn min (x: TotalOrder, y: TotalOrder) -> TotalOrder
where
type PartialOrder =
op (x: PartialOrder) <= (y: PartialOrder) -> bool
op (x: PartialOrder) == (y: PartialOrder) -> bool
axioms
forall x (x <= x);
forall x, y ((x <= y & y <= x) => x == y);
forall x, y, z ((x <= y | y <= z) => x <= z);
type TotalOrder : subtype of PartialOrder =
op (x: TotalOrder) <= (y: TotalOrder) -> bool
op (x: TotalOrder) == (y: TotalOrder) -> bool
axioms
forall x, y (x <= y | y <= x);
followed by things like
type Number : subtype of TotalOrder = ...
type Float : subtype of Number = ...
type Int : subtype of Number = ...
type NumberCollection: subtype of TotalOrder = ...
type NumberList : subtype of NumberCollection = ...
Notes:
* Most people would rename TotalOrder as `Comparable' or somesuch,
and use it via `mixin-MI'.
* I'm using op<= rather than op< throughout just to make easier
contact with well-known theory.
* The `axioms' have little to do with all of this except to clarify
the meanings of the relations involved. I mainly just wrote them
down for completeness.
But all of this is wrong. As you mention,
* It allows things like
min(3, {3, 4})
as well as
3 <= {3, 4}
to typecheck.
* The signatures for TotalOrder ops (and other unstated ops) break
contravariance.
The problem lies in how PartialOrder/TotalOrder are defined and used.
In fact, declaring the signatures of op<= as I did doesn't even match
standard interpretations of orderings, since you don't want to say
that any op<= can necessarily accept two DIFFERENT TotalOrder subtype
objects, just two from the set under consideration.
So instead, you'd like to say that any type T is ordered if it obeys
the Partial (Total) ordering PROPERTY rather than is descended from a
PartialOrder supertype. This can be stated in a parametric
polymorphic (`generic') style via something like
property PartialOrder [T] =
op (x: T) <= (y: T) -> bool
op (x: T) == (y: T) -> bool
axioms ...
property TotalOrder[T] : subproperty of PartialOrder [T] = ...
type Number : obeys TotalOrder = ...
type NumberCollection : obeys TotalOrder = ...
Here, the type Number obeys TotalOrder, even when extended to
subtypes, since you'd like to allow all possible Number subtypes to
compare, presumably via contravariance-maintaining multimethods. If
this were not so, then Int, say, might be claimed to obey TotalOrder,
but not Number. In other words, properties necessarily inherit.
The type NumberCollection should also obey TotalOrder, but the
union type Number-or-NumberCollection does not, and isn't claimed
to (unlike, implicitly, in the orginal declarations).
So it's not the case that Number ISA TotalOrder, instead Number OBEYS
TotalOrder, which means that
fn min (x: TotalOrder, y: TotalOrder) -> TotalOrder
is senseless, since ordering is a property, not a type.
Instead, you need to say something like
fn min (x: T obeys TotalOrder, y: T) -> T'
{
if (x <= y) return x; else return y;
}
where everything typechecks if x and y are both of some (perhaps
distantly removed) supertype that obeys TotalOrder (i.e., a T'),
i.e., T' is the `meet' type of ExactTypeOf(x) and ExactTypeOf(y)
obeying TotalOrder.
This is a form of MIXED universal and subtype polymorphism.
... which seems to solve the original problem.
OBJ3/FOOPS has some constructs along these lines. But they are mired
in other things that make it hard to see how to nicely apply to a more
normal OO type system or language. It's worth serious exploration to
find ways that make these things easy for programmers to state and
use.
In fact, some of this is doable even in C++, assuming PT (Templates,
as in ch. 14 of the Ellis & Stroustrup C++ ARM). One way would be to
1. Make class Number and subclasses, that implement (via double
dispatching) op<= (Number&). (Along with workarounds for
C++ contravariance-blindness, etc.)
2. Similarly for NumberCollection, etc.
3. Make min a template function
template <class T> T& min(T& x, T& y) { ... }
What you miss is
* Code sharing of different versions of min. But this is a
compiler-smarts issue. Templates don't HAVE to be macro-expanded.
* Correct dispatching and type matching. Without properties or
whatever to guide it, and because argument matching is
done statically, C++ won't necessarily invoke the expected
version of min. For example,
Int a; Float b; min(a, b)
should invoke the min(Number, Number) version, which is not
guaranteed by the rules in the ARM.
-Doug
--
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 13244rmf@cs.columbia.edu (Robert M. Fuhrer) (04/22/91)
Doug Lea (dl@g.oswego.edu) writes: > At first glance, you'd like to type min as something like > > fn min (x: TotalOrder, y: TotalOrder) -> TotalOrder > [...] > But all of this is wrong. > [...] > In fact, declaring the signatures of op<= as I did doesn't even match > standard interpretations of orderings, since you don't want to say > that any op<= can necessarily accept two DIFFERENT TotalOrder subtype > objects, just two from the set under consideration. > [...] > So instead, you'd like to say that any type T is ordered if it obeys > the Partial (Total) ordering PROPERTY rather than is descended from a > PartialOrder supertype. This can be stated in a parametric > polymorphic (`generic') style via something like Let me say that while I agree with the bulk of this posting, I think two separate things are going on. First, there is the issue that single inheritance makes harder certain kinds of sharing (like the "property" sharing mentioned above). [It's not clear to me whether the sharing of important object characteristics is made impossible or not -- I haven't thought about it much, comments are welcome!.] The second is that while we like the idea of the type hierarchy, we run into a problem with enforcing constraints among the actual parameter types. In Mr. Lea's near-solution of the example problem, a simple path to an acceptable solution would be to enforce that the 2 parameters have the *same* type (or compatible types, perhaps in the "property" sense). So, my question is, given that the type hierarchy can be properly factored such that the desired properties are represented by some class, does existential quantification (well, bounded since we have a class structure) (ala Cardelli & Wegner, ACM Surveys, 1985) solve the remaining problem? I.e., does a construct such as exists(T < TotalOrder) such that fn min(x: T, y: T) => T do the trick? If so, is this an example of the "impractical" mechanism Mr. Chambers wants to avoid? If not, what else is going on? -- -------------------------- Robert M. Fuhrer Computer Science Department Columbia University 1117B Fairchild Building Internet: rmf@cs.columbia.edu UUCP: ...!rutgers!cs.columbia.edu!rmf
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)
guido@cwi.nl (Guido van Rossum) (04/22/91)
>> [me] > [craig] craig@leland.Stanford.EDU (Craig Chambers) writes: >In article <3378@charon.cwi.nl> guido@cwi.nl (Guido van Rossum) writes: >>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. > >I may not have made myself clear with the problem. I want a general >type system that will handle examples like the one I posted. I am not >interested in languages or type systems that have built-in data >structures that solve this particular problem but do not generalize. >It sounds from your reply that ABC falls into the second category, but >since you didn't describe ABC's type system, I can't tell whether it >is a generally useful solution to a large class of problems. I still don't quite understand your gripe, so here's an explanation of ABC's type system. It solves much more than the particular problem you stated, and I believe that the type system could be extended to handle cases currently not supported by the language. Look for yourself: - basic types: numbers and strings - type constructors: - tuple containing <type1>, <type2>, ... - list of <type1> - table with keys of <type1> and values of <type2> - There are no pointers, nor function variables - There are no unions - There is no way to explicitly introduce a new type (there are infinitely many types possible through the type constructors though) - Functions may be polymorphic - The type inference system is "bootstrapped" with knowledge about the built-in operators; e.g., "+" requires two number arguments and returns a number, "^" operates on strings and returns a string, "#" (the length function) operates on strings, lists and tables, etc. >What's the type (inferred, I guess) of the arguments to the min function? It is (<alpha>, <alpha>), where <alpha> stands for any type but the two occurrences must match. This leaves the actual type unrestricted but says that the two arguments must have the same type. >How does the compiler know that "<" in min will work? From the definition of min it concludes that the arguments must be comparable to each other. The definition of the built-in "<" operator says that two types are comparable to each other if they are the same type. [As I said, ABC has no compiler since is interpreted, but that's beside the point -- there is a static type checker that must accept a program before it is ever passed to the interpreter.] >Does the >compiler type-check each invocation of min separately (which would be >sidestepping the issue) or does it really infer a type for min that's >usable by all its callers? The latter. Min's type would be "function with (<alpha>, <alpha>) argument returning <alpha>". ABC's type checker uses a unification algorithm to combine the various things it learns about variables and functions. >Part of the description of the problem implies to me that the type >system should include some notion of subtyping and some notion of >parameterized types. My (partially formed) solution also uses type >variables and some notion of a type pattern (I'm not sure whether or >not this is the same as a parameterized type; I'm leaning towards yes >if I can overcome some annoying technical obstacles). >If someone posts that some type system solves the problem, please also >post enough information to give people a feel for the facilities in >the type system that allow it to solve the problem. Thanks. I am not a type theorist, just a former member of the ABC implementation group, so it may be difficult for me to explain ABC's type system to you. Hope this has helped. If not, I'll ask its designer to take over... --Guido van Rossum, CWI, Amsterdam <guido@cwi.nl> "If this is Bolton, I shall return to the pet shop"
craig@leland.Stanford.EDU (Craig Chambers) (04/23/91)
In article <3392@charon.cwi.nl>, guido@cwi.nl (Guido van Rossum) writes: |> craig@leland.Stanford.EDU (Craig Chambers) writes: |> >How does the compiler know that "<" in min will work? |> |> From the definition of min it concludes that the arguments must be |> comparable to each other. The definition of the built-in "<" operator |> says that two types are comparable to each other if they are the same |> type. The "<" message was supposed to be a user-defined message, implemented differently by different objects/classes. But since ABC has no user-defined data types, this whole example doesn't make sense, and ABC can't express the general problem I'm trying to type-check. -- Craig Chambers
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
new@ee.udel.edu (Darren New) (04/24/91)
In article <3378@charon.cwi.nl> guido@cwi.nl (Guido van Rossum) writes: >This can be done in ABC, a statically typed interpreted language >developed at CWI [1]. From your example, it looks like ABC is dynamically typed (altho strongly typed) to me. Why do you say it is statically typed? What are the types of "x" and "y" in your declaration of "min"? -- 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 +=+
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
craig@elaine35.Stanford.EDU (Craig Chambers) (04/24/91)
In article <DUCHIER.91Apr23205041@albania.cs.yale.edu> duchier-denys@cs.yale.edu writes: >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...'. Several people have pointed at Haskell as a language including a type system that solves the problem (a lot of people have sent e-mail to me directly; I was actually hoping to spur group discussion rather than request information). And Haskell's system might be a reasonable answer. I've read the Haskell report, but since I've never programmed in Haskell, I can't really tell. I wonder e.g. whether the type variables in the Ord class allow subtypes or whether all "instances" of a type variable must be the same type. I also wonder whether type classes are a compile-time macro expansion type of thing for overloading or whether they support run-time dynamic dispatching like a full-fledged OO language. I'd appreciate answers from people more knowledgable about Haskell than me (I?). In any case, I'll take this opportunity to post my thoughts on a type system that attempts to solve the problem. The type of the arguments to the min function must be things that understand "<". The straightforward (and broken) approach would be to define a supertype called Ordered that is the type of these arguments: type Ordered Ordered "<" Ordered: bool ... end Ordered min(x:Ordered, y:Ordered):Ordered { return x < y ? x : y; } Numbers and collections of Ordered things are then made subtypes of Ordered: type Number <= Ordered Number "<" Number: bool ... end Number type Integer <= Number Integer "<" Integer: bool { ... } Integer "<" Float: bool { ... } ... end Integer type Float <= Number Float "<" Integer: bool { ... } Float "<" Float: bool { ... } ... end Float type Collection[S] ... end Collection type Collection[T <= Ordered] <= Ordered Collection[T] "<" Collection[T]: bool { ... } ... end Collection Unfortunately, this doesn't work since it allows calls of the form min(3, {3,4}) which are not implemented anywhere. In other words, Number and Collection are not legal subtypes of Ordered since they violate contravariance. What we need is some "type pattern" which describes types that support "<" on their elements, or more precisely, a pattern of two types that can be compared (the type of the first argument to < doesn't have to be the same as the second type). I'm thinking that parameterized types are such pattern types. I'm looking at solutions like the following: type Ordered[T] T "<" T: bool ... end Ordered type Number <= Ordered[Number] ... end Number ... type Collection[T <= Ordered[T]] <= Ordered[Collection[T]] ... end Collection min(x:Ordered[T], y:Ordered[T]):T { ... } Now Number is a legal subtype of the Ordered[Number] instance of the Ordered parameterized type (check the signatures), and similarly for the Collection type (although this case begins to look a little hairy). The interface to min states that both arguments should be subtypes of some common instance of the Ordered parameterized type, and that the result of min is (a subtype of) this instantiating type. However, I don't completely understand this type system. Are type patterns really the same as parameterized types? Sometimes I get confused whether I should say Ordered[T] somewhere or just T. For instance, I wonder whether the type of y in the min function above could just as easily be T. How would such a change affect what kinds of objects can be passed to min? I'm also trying to get this type system to work out in a multiply-dispatched OO language that I've been working on, and that's making the problem (for me) even harder. -- Craig Chambers
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
boehm@parc.xerox.com (Hans Boehm) (04/25/91)
It seems to me that this problem fundamentally has very little to do with object
oriented programming. Expressing things in terms of a subtype hierarchy
confuses the issue and contributes nothing. In Russell, the min function
has signature:
func [x,y: val T; T: type { < }] val T
It's a function of two values of type T, and of the type T itself. T is
expected to include a < operation. (I get to cheat slightly, in that
operations like < have the "right" type by default.) The third (type)
parameter will be inferred for each call, and is not explicitly needed,
except in the declaration of min.
It would be nice if I could annotate "<" with some properties (e.g. the fact
that it should be transitive). Languages like IBM's Scratchpad have
mechanisms for doing that.
Cardelli's Quest language combines this kind of mechanism with inheritance.
(Quest and Russell differ in other profound respects. But those have nothing
to do with this discussion.)
Hans
(boehm@xerox.com)
Usual disclaimers ...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!gudemannew@ee.udel.edu (Darren New) (04/25/91)
In article <2392@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes: >OK, I give up. What is the difference between dynamic typing and >dynamic binding? How about an example? Hermes gives a declaration (polymorph) and two operations (wrap and unwrap) for dealing with it. You can take a typed value and wrap it into a polymorph. Later, you can take that polymorph and unwrap it into a typed value (with appropriate runtime checks). However, there is nothing else you can do with the polymorph (except ask its type and such) while it is wrapped: specifically, you cannot operate on the wrapped typed value. This feature allows building of hetrogeneous lists, resource managers, dictionaries, and so on. However, it seems to be a pain to build `objects' in Hermes because each capability for sending a message must be unwrapped before use if it is passed in a polymorph and must be predeclared of the right type if it is not a polymorph. Either each "object" will have a dictionary of polymorphs which must be unwrapped or will have a separate declaration for all possible combinations of messages handled (clearly unfeasible). C++ has static typing (in that it is illegal to perform an operation on something that the declared type does not support), but it is possible that the same call will invoke different methods for different values of arguments. This I call dynamic binding. Smalltalk mixes this up because the type of a value *always* determines what method a message will be bound to, and thus people tend to confuse these two properties. -- --- 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 +=+
wg@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
craig@leland.Stanford.EDU (Craig Chambers) (04/25/91)
In article <boehm.672515148@siria>, boehm@parc.xerox.com (Hans Boehm) writes: |> It seems to me that this problem fundamentally has very little to do with object |> oriented programming. Expressing things in terms of a subtype hierarchy |> confuses the issue and contributes nothing. In Russell, the min function |> has signature: |> |> func [x,y: val T; T: type { < }] val T |> |> It's a function of two values of type T, and of the type T itself. T is |> expected to include a < operation. (I get to cheat slightly, in that |> operations like < have the "right" type by default.) The third (type) |> parameter will be inferred for each call, and is not explicitly needed, |> except in the declaration of min. Part of the subtype interaction is that I'd like to instantiate the type T above to "Number", and then allow subtypes of Number as the actuals passed to x and y. So I don't think that subtyping is completely spurious. But I believe that subtyping might be able to be "grafted on" to an existing non-object-oriented language that handles these sorts of things. For example, I think that you could take CLU's form of the parameterized min function with where clauses: min = proc[T:type](x:T, y:T) returns(T) where T has <:proctype(T, T) returns bool ... end min ...and then allow subtyping of arguments. Then I could write: min[number](3,4.5) I could also write: min[collection[number]]({3,4.5}, {2,6.2,-5}) The where clause above is similar to the type pattern idea I talked about earlier and to properties in the Haskell type class system. But I'd like to find a solution that didn't have both a notion of type that has subtypes and a notion of type property that has instances; having both seems non-orthogonal in some way. It seems to me that languages based (at least in spirit) on some form of polymorphic lambda calculus, e.g. Russell, ML, and Haskell, can do the part of the problem that involves type variables (i.e. handling Num * Num and Collection * Collection), but none of them really handle the part dealing with subtyping of various kinds of numbers. And most existing statically-typed object-oriented languages handle the subtyping of numbers fine but fall down when faced with a need for some form of type variables. -- Craig Chambers P.S. People might find it interesting that A. K. Wright sent me e-mail saying that he felt that the min problem and similar problems cannot be solved to my satisfaction, and references his SIGPLAN PLDI'90 paper with G. V. Cormack on "Type-Dependent Parameter Inference" as containing a number of linear algebra examples that pose similar problems for static type checkers.
boehm@parc.xerox.com (Hans Boehm) (04/26/91)
It's not entirely clear to me what you're trying to achieve by viewing integer and float as subtypes of number. They presumably share no code, hence code reuse is not the issue. There is no real possibility of adding further subtypes without modifying the existing ones. (You would have to add definitions of < for all newly introduced combinations.) Thus it seems that in this case subtyping is equivalent to viewing number as the union of integer and float, with < suitably defined on the union. Essentially all of the languages under discussion can deal with that. There are problems with this, but they are essentially syntactic. I may not want to write convert_to_number(3.5). (If I care about "performance transparency", I may want to write it, since convert_to_number(x) may cost a lot more to evaluate than x. I may have to convert a floating point value in a register to a pointer to a tagged value in the heap.) Thus there are sticky issues about inferring injections into a union. In this case it doesn't seem hard. But a general elegant solution probably is hard, at least if it's also capable of inferring the type argument to min. Hans (boehm@xerox.com)
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
eliot@cs.qmw.ac.uk (Eliot Miranda) (04/29/91)
In article <boehm.672608274@siria> you write: >It's not entirely clear to me what you're trying to achieve by viewing >integer and float as subtypes of number. They presumably share no code, >hence code reuse is not the issue. They most certainly can. In Smalltalk-80's arithmetic implementation class Number provides a number(sorry) of arithmetic operators defined in terms of other (presumed more primitve operators). e.g. Number abs ^self < 0 ifTrue: [self negated] ifFalse: [self] e.g. quo: (rounding division towards zero), // (rounding division towards -ve infinity) are implemented in Number in terms of / (exact division) floor & ceiling. Number provides the specification & implementation of the coercion system which allows mixed arithmetic. Number provides generic implementations of many functions implemented by float, e.g. Number cos ^self asFloat cos Number provides enumeration & interval creation: to: to:by: to:by:do: etc At least in Smalltalk, using a class hierarchy that requires subclasses to implement a certain subset of operators & then implementing other operators implemented upon them higher in the hierarchy is a common & powerful technique. The canonical example is the implementation of the relational operators > >= <= ~= min: max: between:and: etc in Magnitude in terms of = < and not. -- Eliot Miranda email: eliot@dcs.qmw.ac.uk Dept of Computer Science ARPA: eliot%dcs.qmw.ac.uk@nsf.ac.uk Queen Mary Westfield College UUCP: eliot@qmw-dcs.uucp Mile End Road Fax: 081 980 6533 (+44 81 980 6533) LONDON E1 4NS Tel: 071 975 5229 (+44 71 975 5229)
boehm@parc.xerox.com (Hans Boehm) (04/30/91)
eliot@cs.qmw.ac.uk (Eliot Miranda) writes: >In article <boehm.672608274@siria> you write: >>It's not entirely clear to me what you're trying to achieve by viewing >>integer and float as subtypes of number. They presumably share no code, >>hence code reuse is not the issue. >They most certainly can. In Smalltalk-80's arithmetic implementation >class Number provides a number(sorry) of arithmetic operators defined in terms >of other (presumed more primitve operators). >e.g. >Number abs > ^self < 0 ifTrue: [self negated] ifFalse: [self] > ... Certainly it is possible for them to share code using inheritance, once you augment the example with other functions. However the original < and min example also point out why you might not want to do this. Implementing min as a method of number means that ir only applies to numbers, and not to other objects understanding <. This argument is perhaps less convincing for abs, since there are fewer kinds of objects that understand 0, <, and negation. Other operations like integer exponentiation again have much wider applicability. The point is that inheritance is sometimes the right tool, but it often is not. For the original problem, I believe it is not. For some expansions of the original problem, it probably is. But even then there are static type systems (e.g. Cardelli's Quest) that deal with both parametrization and subtyping. Hans boehm@xerox.com Standard disclaimers ...
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 +=+
rockwell@socrates.umd.edu (Raul Rockwell) (04/30/91)
Darren New: > Besides, I still haven't seen a good example of how to do > hetrogeneous lists in a statically-typed language. Sorry, I can't resist (-: struct dumb { char c; int i; double* d; }; Raul
rick@tetrauk.UUCP (Rick Jones) (04/30/91)
new@ee.udel.edu (Darren New) writes: > Doesn't look like you've answered the question here. What's the > type of `min'? I feel this does deserve a bit of expansion. To explain the implication of "Current" in Eiffel, it is first necessary to point out that routines in Eiffel can only exist as features of classes. A class is the only form of code module in Eiffel, and everything is written within the boundaries of some class. Thus there is no such thing as "the" min function - many classes may provide a "min" function. A function can only be invoked via a non-void reference to an object of that class. A function such as "min" would in fact be written as a function of say a number class, and would return either the object on which it is called or its argument, whichever is the smaller. I.e. (fragment code of class NUMBER) class NUMBER export min feature min (other: like Current): like Current is do if other < Current then Result := other else Result := Current end end end "Current" is the current object, and "like Current" is the same type as the current object. So in this example "like Current" is the same as NUMBER. In use: num1, num2, num3: NUMBER ; -- ... values assigned to num1 & num2 ... num3 := num1.min (num2) Now if a class INTEGER is a descendant of NUMBER, it inherits "min", but the types of the argument and return value automatically change without explicit redefinition. So: class INTEGER inherit NUMBER end will give INTEGER a "min" function whose type is INTEGER, and whose argument must also be (or conform to) an INTEGER. So if I have: num1, num2, num3: NUMBER ; int1, int2, int3: NUMBER ; The following are legal: int3 := int1.min (int2) -- all types the same num3 := int1.min (int2) -- conforming result type num3 := num1.min (int2) -- conforming argument type but the following aren't: int3 := num1.min (num2) -- wrong result type int3 := int1.min (num2) -- wrong argument type I hope this helps. -- Rick Jones, Tetra Ltd. Maidenhead, Berks, UK rick@tetrauk.uucp Any fool can provide a solution - the problem is to understand the problem
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
anw@maths.nott.ac.uk (Dr A. N. Walker) (05/01/91)
In article <52166@nigel.ee.udel.edu> new@ee.udel.edu (Darren New) writes: >Besides, I still haven't seen a good example of how to do hetrogeneous >lists in a statically-typed language. Perhaps I might have a go if I understood the question better. (a) There is no difficulty [in the right language!] in writing a generic list constructor, so that given a type T you could instantiate lists of T. This could be a library routine, that needn't know in advance what T might be. This would give a homogeneous list, but different calls of the same routine would deliver lists of different types. (b) Given a set of types, say "student", "room", "teacher", "course", there is no difficulty [in languages that don't necessarily have generics but do have unions and pointers] in writing routines for lists of "union (student, room, teacher, course)". This would give a homogeneous list, but the base contents could be as heterogeneous as you [statically] liked. (c) Given a collection of ways of constructing types, say "array of", "pointer to", "procedure with parameters ... returning ...", etc., there is no difficulty [in suitable languages!] in constructing an ADT (perhaps some tree structure) which represents arbitrary types and building lists of this ADT (and/or of instantiated objects of such types). Compilers do this all the time. (d) Given a generic pointer, in languages that assume rightly or wrongly that all pointers are the same "shape", there is no difficulty in building a list of pointers to arbitrary objects. Storage allocators do this all the time. Are you thinking of something else? Or is one of (a-d) what you are after? [I have no axe to grind on the general static/dynamic debate. Dynamic typing is often more convenient, but it is, I still maintain, *necessary* only when you, the programmer, don't know what types of objects your program is going to have to deal with or what operations are going to be effected on them. That situation might be acceptable for a quick prototype, but not for a finished system. That is why it is easy to describe *situations* in which dynamic typing is desirable, but we have not seen a completely specified *problem* for which it is needed.] -- Andy Walker, Maths Dept., Nott'm Univ., UK. anw@maths.nott.ac.uk
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
new@ee.udel.edu (Darren New) (05/02/91)
In article <1991May1.143831.2065@maths.nott.ac.uk> anw@maths.nott.ac.uk (Dr A. N. Walker) writes: >In article <52166@nigel.ee.udel.edu> new@ee.udel.edu (Darren New) writes: >>Besides, I still haven't seen a good example of how to do hetrogeneous >>lists in a statically-typed language. (a) gives you a bunch of homogenous lists. (b) gives you a list of unions (which can only contain types you consider when you write the program). >(c) Given a collection of ways of constructing types, say "array of", > "pointer to", "procedure with parameters ... returning ...", etc., > there is no difficulty [in suitable languages!] in constructing an > ADT (perhaps some tree structure) which represents arbitrary types > and building lists of this ADT (and/or of instantiated objects of > such types). Compilers do this all the time. Getting closer. However, you have to then run this through the compiler. (Hermes can let you do this.) Or are you talking about something like XDR or a routine to do ASN.1/BER encoding or something? Then you are implementing dynamic typing in order to obtain hetro lists. >(d) Given a generic pointer, in languages that assume rightly or > wrongly that all pointers are the same "shape", there is no > difficulty in building a list of pointers to arbitrary objects. > Storage allocators do this all the time. But doing this makes it difficult to actually *do* something with the values you are pointing to. > Are you thinking of something else? Or is one of (a-d) what >you are after? I think the canonical example (for me) is something like a resource manager. I want to be able to write a routine (once) and compile it (once) at the beginning of my work. This routine should accept pairs of <name, value> where the value may be anything the language can handle. It should be able to add and find and remove tuples, and it should be able to iterate through the list, handing me each tuple (for example, to find out the total number of bytes used by values). In case (c), you have to write code for each type to break it into the values you are looking for, interpret the tags, etc. In case (d), you have to already know the type of the object associated with each name before you can do anything with it (such as find it's size) or else it turns into case (c). > [I have no axe to grind on the general static/dynamic debate. >Dynamic typing is often more convenient, but it is, I still maintain, >*necessary* only when you, the programmer, don't know what types of >objects your program is going to have to deal with or what operations >are going to be effected on them. Right. >That situation might be acceptable >for a quick prototype, but not for a finished system. Here I must disagree. Building libraries for other people to use, and building these libraries such that the library can evolve without invalidating programs built with previous versions of the library and vica versa, is an important use for dynamically-typed systems. I don't think that your (d) is as safe as a dynamic type system. I'm starting to think that "dynamic typing" might be somewhat akin to "object oriented programming" in the sense that it is more a organization/management technique than an actual programming language issue. Just like you can do object-oriented programming in COBOL (but it isn't very pretty), you can "do" dynamic typing in a static language (but it isn't very pretty). If you knew at the start exactly how the program would work, knew all the programs it would ever have to interface to, and knew the complete requirements, then you could do it with static typing. However, few projects I've ever worked on (and none I didn't spec by myself for myself) have ever met these requirements. -- Darren (Followups via email -- It'll expire before I have a chance to read news again.) -- --- 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) (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.143831.2065@maths.nott.ac.uk> anw@maths.nott.ac.uk (Dr A. N. Walker) writes:
] [ ... ]
] Dynamic typing is often more convenient, but it is, I still maintain,
] *necessary* only when you, the programmer, don't know what types of
] objects your program is going to have to deal with or what operations
] are going to be effected on them. That situation might be acceptable
] for a quick prototype, but not for a finished system. That is why it
] is easy to describe *situations* in which dynamic typing is desirable,
] but we have not seen a completely specified *problem* for which it is
] needed.
This has to be the most succinct description of the relative advantages of
static and dynamic typing that I have seen - thank you, I agree entirely.
--
Rick Jones, Tetra Ltd. Maidenhead, Berks, UK
rick@tetrauk.uucp
Any fool can provide a solution - the problem is to understand the problemrick@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
rick@tetrauk.UUCP (Rick Jones) (05/03/91)
In article <2479@m1.cs.man.ac.uk> mario@cs.man.ac.uk (Mario Wolczko) writes: >In article <1146@tetrauk.UUCP>, rick@tetrauk.UUCP (Rick Jones) writes: >> [ ... ] 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. This is true, and static analysis will always be pessimistic. What GTA does do is to establish whether there are any assigments of objects in the whole program, which could (directly or indirectly) result in an object which does not support some feature being attached to a variable which calls the feature. This ignores run-time branches, so there is an implicit assumption that every possible branch combination may at some time be executed. Thus your example: > 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; will be rejected. However, for normal, well-designed programs, this is not a problem. A program such as this example is inherently unreliable, even though thorough testing and use may never have produced the conditions required for failure. A safer version would be: > 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 > if predicate1 > then X.F; > fi but this is not good object oriented design. The program is making branch decisions based (indirectly) on the object's actual type. Good OO design uses abstraction and polymorphism to produce code which is independent of the object's actual type. A checkably safe version is: > var X, Y; > if predicate1 > then Y := L1; /* L1 is an object that has feature F */ > Y.F; > X := Y; > else X := L2; /* L2 is an object that does not have feature F */ > fi Feature F has been safely applied to object L1 via Y, subsequently feature F may not be applied via X, since X may or may not refer to object L1. Although this appears to make a simple program more complex, the example is artificial. It is more likely that the equivalent assignments are across different modules, where there would have to be separate declarations of X and Y anyway. If the situation of the first example existed, but distributed across different source modules, the unreliability would go unnoticed. If the second existed in the same way, it would be very clumsy code. GTA would pick up both these, suggesting a more robust or cleaner design should be used. I maintain that a well designed program which avoids branch decisions based on type will check correctly under the rules of GTA. I do not believe even the pessimistic checking of GTA is possible in a dynamically typed language - it requires explicit type declarations, and a conventional (e.g. inheritance based) mechanism for defining basic type conformance as a starting point. I cannot produce a rigorous justification of this viewpoint, though. The theory of this type-checking system was discussed quite thoroughly by Bertrand Meyer in the article he posted last year. If you don't have it and would like a copy (it's about 1500 lines), I can email it to you. -- Rick Jones, Tetra Ltd. Maidenhead, Berks, UK rick@tetrauk.uucp Any fool can provide a solution - the problem is to understand the problem
adam@visix.com (05/04/91)
In article <1991May1.143831.2065@maths.nott.ac.uk>, anw@maths.nott.ac.uk (Dr A. N. Walker) writes: |> [I have no axe to grind on the general static/dynamic debate. |> Dynamic typing is often more convenient, but it is, I still maintain, |> *necessary* only when you, the programmer, don't know what types of |> objects your program is going to have to deal with or what operations |> are going to be effected on them. That situation might be acceptable |> for a quick prototype, but not for a finished system. That is why it |> is easy to describe *situations* in which dynamic typing is desirable, |> but we have not seen a completely specified *problem* for which it is ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ |> needed.] Yes, a completely specified problem is, by definition, one in which you know all the objects and operations, ergo there is no way to completely specify a problem that requires dynamic typing. However, I think you overemphasize the importance of completely specified problems. In my view, underspecified problems are not just quick prototypes. System browsers are underspecified. AI programs are underspecified. Learning starts with an underspecified state. A system that learns, or helps you learn, must be underspecified. You learn how to completely specify a problem by attempting various underspecified solutions. I see this as the fundamental difference between computer science and software engineering. |> -- |> Andy Walker, Maths Dept., Nott'm Univ., UK. |> anw@maths.nott.ac.uk Adam
amanda@visix.com (Amanda Walker) (05/04/91)
In article <1991May3.184332.28319@visix.com> adam@visix.com writes:
However, I think you overemphasize the importance of completely
specified problems. In my view, underspecified problems are not
just quick prototypes. System browsers are underspecified.
AI programs are underspecified.
Indeed. In fact, one of the advantages I have found in OO design and
implementation is that it makes it possible to attack problems over
incompletely specified domains. In particular, dynamic type systems
allow existing code to work over domains which were not originally
specified, as long as those domains have the necessary
characteristics. A trivial example of this idea is that a heapsort
should operate on any set of objects for which I can provide
comparison and exchange operations.
One all too common example of this situation is using a precompiled
module with a new data type (i.e., code reuse at the binary level),
which we can expect to happen more and more often as OO concepts
become more "mainstream."
--
Amanda Walker amanda@visix.com
Visix Software Inc. ...!uunet!visix!amanda
--
"It's not the tragedies that kill us, it's the messes." --Dorothy Parkermario@cs.man.ac.uk (Mario Wolczko) (05/04/91)
In article <1991May3.184332.28319@visix.com>, adam@visix.com writes: > |> That is why it > |> is easy to describe *situations* in which dynamic typing is desirable, > |> but we have not seen a completely specified *problem* for which it is > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ > |> needed.] > > Yes, a completely specified problem is, by definition, one in which > you know all the objects and operations, ergo there is no way to > completely specify a problem that requires dynamic typing. Indeed. One of the main ideas behind inheritance is that you leave some things open so that classes may be reused in unanticipated ways, ie you are building components to assist in the solution of problems you do not even know about yet! 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___________________________________
davidm@uunet.UU.NET (David S. Masterson) (05/06/91)
>>>>> On 4 May 91 15:39:18 GMT, mario@cs.man.ac.uk (Mario Wolczko) said:
Mario> Indeed. One of the main ideas behind inheritance is that you leave
Mario> some things open so that classes may be reused in unanticipated ways,
Mario> ie you are building components to assist in the solution of problems
Mario> you do not even know about yet!
Hmmm. Interesting way of looking at inheritance and nothing wrong with it.
Just curious, though (and this may be very related to the question at hand),
do most people use inheritance to build down from some underspecified level to
something more specific to the problem at hand or do most people build up from
some highly specific to something that can be more easily generalized to later
problems? If you say either-or (depending on the circumstances), what are the
circumstances that make you choose one over the other?
I think people will find that the answers to this will show the differences in
how people attack problems and that these differences have led to static
versus dynamic specification of problems.
--
====================================================================
David Masterson Consilium, Inc.
(415) 691-6311 640 Clyde Ct.
uunet!cimshop!davidm Mtn. View, CA 94043
====================================================================
"If someone thinks they know what I said, then I didn't say it!"rick@tetrauk.UUCP (Rick Jones) (05/07/91)
In article <1513@fang.dsto.oz> dch@aeg.dsto.oz.au (Dave Hanslip) writes: | rick@tetrauk.UUCP (Rick Jones) writes: | | >anw@maths.nott.ac.uk (Dr A. N. Walker) writes: | >] [ ... ] | >] That is why it | >] is easy to describe *situations* in which dynamic typing is desirable, | >] but we have not seen a completely specified *problem* for which it is | >] needed. | | >This has to be the most succinct description of the relative advantages of | >static and dynamic typing that I have seen - thank you, I agree entirely. | | | Agree you may, but very few real-world, complex problems are ever completely | specified. Even if the specification process is rigorous, the customer never | knows completely what he/she wants and over the life of software the | requirements will inevitably change. That is why it's not only acceptable in | a finished system, but desirable. Note that I didn't say that static typing is always better, but that this is a very good definition of the strengths of each approach. I know I have been arguing the case for Eiffel's static type checking mechanisms - that's because I am an Eiffel user, and some of the type checking concepts were clearly mis-understood by some contributors to this newsgroup. The system I am developing is in fact a two-tier model. In simple terms, there is a statically typed, hard-coded lower level written by application programmers (in Eiffel), which supports a higher level, dynamic model which will be configurable by users. The high level model is in effect dynamically typed (although it isn't a "programming language" in the conventional sense). This enables the dynamic model to be configured very freely, but without any danger of breaking the static model. In the context of Dr. Walker's statement, the low level model has a behaviour which IS completely specified - the system would not be reliable if it wasn't. The high level model is not completely specified, and so is open to change and is dynamic. -- 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/08/91)
In article <CIMSHOP!DAVIDM.91May5120037@uunet.UU.NET>, cimshop!davidm@uunet.UU.NET (David S. Masterson) writes:
do most people use inheritance to build down from some
underspecified level to something more specific to the problem at
hand or do most people build up from some highly specific to
something that can be more easily generalized to later problems?
If you say either-or (depending on the circumstances), what are
the circumstances that make you choose one over the other?
I can only speak for myself. When trying to solve a specific problem
I will try to identify aspects of that problem which are of a general
nature, and which could be reused. (Example: in writing a compiler, I
have developed classes to support directed acyclic graphs in a general
way). In some cases, there will be parts of a class that are very
specific to the problem at hand, and then I will try to factor the
class into two classes -- an "abstract", reusable superclass, and a
"concrete" subclass. Sometimes this factoring can be repeated,
leading to a hierarchy of abstract classes, with concrete classes at
the leaves.
Sometimes the abstract class will already be there, and I just have to
provide a concrete subclass, which is usually easy. (I do all my
serious OO programming in Smalltalk, which has lots of abstract
classes.) Occasionally I find a concrete class which does part of
what I want, but perhaps something else which I don't, and then I try
to split that class into abstract and concrete pieces, such that I can
inherit from the abstract part to get what I want. (Splitting an
existing class while remaining compatible can be very hard.) In any
case I try to avoid having one concrete class inherit from another
concrete class.
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___________________________________mario@cs.man.ac.uk (Mario Wolczko) (05/08/91)
In article <1158@tetrauk.UUCP>, rick@tetrauk.UUCP (Rick Jones) writes:
[long defence of global type analysis, followed by critique of my 6
line program fragment]
But now you're moving the goalposts. Your original posting stated
quite unequivocally that global type analysis only rejected programs
that were not type-safe, and my example showed that this was false.
(The example was not meant to be particularly meaningful, only to make
the point.)
Describing such a program as "inherently unreliable" is similarly
bogus --- by appropriate substitution I could make it into a program
that was provably correct.
Having retreated from the earlier claim, you now claim that only
well-designed programs will be amenable to global type analysis, a
much more subjective claim.
I feel sure that we could argue until blue in the face as to what
constitutes a well-designed program. My guess is that your bottom
line will be that any program which is not amenable to global type
analysis is not well-designed!
I will make only two further observations:
1. Eiffel's "reverse assignment attempt" is a run-time type test
anyway, and
2. The most common "type error" in Smalltalk is sending a message to
nil, ie forgetting to initialize a variable. Static typing doesn't
help here at all.
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___________________________________sakkinen@jyu.fi (Markku Sakkinen) (05/09/91)
In article <2500@m1.cs.man.ac.uk> mario@cs.man.ac.uk (Mario Wolczko) writes: > ... >I will make only two further observations: > ... >2. The most common "type error" in Smalltalk is sending a message to > nil, ie forgetting to initialize a variable. Static typing doesn't > help here at all. Right, with type systems defined as they usually are, trying to access 'nil' cannot be caught as a type error even in statically typed languages. The story becomes different if pointer types as such are defined as "strict", i.e. 'nil' not allowed, and conventional (possibly 'nil') pointers are then regarded as union types. Of course, one could not very well build typical dynamic, recursive data structures using only strict pointers. 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)
rick@tetrauk.UUCP (Rick Jones) (05/10/91)
In article <2500@m1.cs.man.ac.uk> mario@cs.man.ac.uk (Mario Wolczko) writes: >In article <1158@tetrauk.UUCP>, rick@tetrauk.UUCP (Rick Jones) writes: >[long defence of global type analysis, followed by critique of my 6 >line program fragment] > >But now you're moving the goalposts. Your original posting stated >quite unequivocally that global type analysis only rejected programs >that were not type-safe, and my example showed that this was false. Well, I didn't think I was moving them - but I accept that I probably didn't make clear enough where I was planting them to start with. >I feel sure that we could argue until blue in the face as to what >constitutes a well-designed program. My guess is that your bottom >line will be that any program which is not amenable to global type >analysis is not well-designed! You could be right - how one approaches design is to some degree a subjective matter. The constraints of Eiffel's type system, including GTA (which Bertrand Meyer commented has always been present as implicit rules anyway), do not present themselves to me as impediments to program design - if anything, I find them to be aids. I say this from practical experience, not just ideology. I have not used Smalltalk for any serious work, only played with it, but my feeling is that if I were to tackle a project with it, I would design things in a different way. I can't say exactly how it would be different, I would need some experience to say any more. I tend to get the feeling that a lot of the "static v. dynamic" debate is in fact a debate between programmers of the procedural-based school (typified by Eiffel and C++), and those of the Smalltalk school. The underlying styles are so different that the typing issue is really only one part of the distinction. A design which works well in Eiffel may not transfer directly to Smalltalk, nor vice-versa. However, the same _problem_ can be solved equally well in either environment, if given to designers/programmers with equivalent familiarity in the respective systems; they will just build it differently. Since everyone works best in the environment in which they feel most familiar, they naturally tend also to feel it is the best environment. There is in fact no absolute criteria of "best" - it is in the end all subjective. >I will make only two further observations: >1. Eiffel's "reverse assignment attempt" is a run-time type test > anyway, and True, but being an assignment between types it operates within the type system rather than against it, which I find works very cleanly. >2. The most common "type error" in Smalltalk is sending a message to > nil, ie forgetting to initialize a variable. Static typing doesn't > help here at all. And also, of course, in Eiffel (trappable by an implicit assertion). Unless there are no void references permitted - which introduces other problems - there seems to be no practical way around this. Now if this could be deduced statically ...! but I guess that takes us into formal proofs, at which point I exit stage left and leave it to others. -- Rick Jones, Tetra Ltd. Maidenhead, Berks, UK rick@tetrauk.uucp Any fool can provide a solution - the problem is to understand the problem
preece@urbana.mcd.mot.com (Scott E. Preece) (05/16/91)
In article <1991May3.212005.29453@visix.com> amanda@visix.com (Amanda Walker) writes: | | ... A trivial example of this idea is that a heapsort | should operate on any set of objects for which I can provide | comparison and exchange operations. --- OK, let me expose my ignorance[1]. I'd like to see how object-oriented design works. Would you care to sketch the design for this? My naive model would be that a heap is an object and that it has add and remove methods to take objects of unspecified type and stick them into the heap in the right place. So where do the comparison and exchange procedures go? I see two alternatives[2]: (1) the heap object has compare and exchange methods that "know about" all of the types, figure out what's involved, and operate on the member objects or (2) the objects have methods that report their "comparable value" and size in canonical forms that a generic routine in the heap object can operate on. Neither of these makes me awfully happy. In case (1) the heap has to know much too much about the objects, making it hard to believe that the desired level of reusability can be reached. In case (2) we have removed the heap's ability to choose what attribute of the object is used for sorting, since the object owns production of the sort key. So where is "the right place" to put the comparison and exchange knowledge, in the heap, in the objects living in the heap, or somewhere else that I missed entirely? NOTES: [1] I first used SIMULA in 1973, but the way I used it didn't look much like what people seem to be saying about o-o today. I have a little trouble with the notion that process should go away and design should be strictly composition of objects (I've seen several statements along those lines). At any rate, I'm being quite honest here in asking for examples of how an experienced O-O designer would think about the problem. [2] Well, actually, of course, I see a lot of other alternatives, but they mostly could be characterized as one of these, with embroidery. -- scott preece motorola/mcg urbana design center 1101 e. university, urbana, il 61801 uucp: uunet!uiucuxc!udc!preece, arpa: preece@urbana.mcd.mot.com phone: 217-384-8589 fax: 217-384-8550