Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!ub!oswego!oswego.oswego.edu!dl From: dl@g.g.oswego.edu (Doug Lea) Newsgroups: comp.object Subject: Re: A Hard Problem for Static Type Systems Message-ID: Date: 22 Apr 91 09:56:07 GMT References: <1991Apr20.010347.28984@leland.Stanford.EDU> <3378@charon.cwi.nl> <1991Apr22.015415.28303@leland.Stanford.EDU> Sender: news@oswego.oswego.edu (Network News) Reply-To: dl@g.oswego.edu Organization: SUNY Oswego Lines: 141 In-Reply-To: craig@leland.Stanford.EDU's message of 22 Apr 91 01:54:15 GMT [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 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 13244