OO need not be ugly, if done right: "Objects to Unify Type Classes and GADTs", http://lambda-the-ultimate.org/node/3837
Sandro On 11/03/2010 12:38 PM, Jonathan S. Shapiro wrote: > As part of thinking about interop, I've been reviewing the BitC stance > on object-oriented programming. Object-oriented programming in the style > of C++/Java/C# remains, in my opinion, the wrong model. That said, it's > a popular model, and certainly one that is not going away anytime soon. > > While I would be very reluctant to twist the BitC type system to > accomodate OO, I see no reason to stand on a pedastle and exclude OO if > the type system can actually handle it. Actually, I'ld be willing to add > minor enhancements to make it work. If nothing else, we need to think > about this for the sake of code conversion. > > BACKGROUND: > > I don't think it is fully implemented in the current implementation, > but BitC already provides a mechanism for ad-hoc polymorphism over > structures through the built-in "has-field" constraint. This takes the form: > > (has-field 'a FieldName 'b) > > with the intended meaning that the type 'a has some field FieldName of > type 'b. So given: > > (define (f x) x.fld) > > we would infer: > > (forall ((has-field 'a FieldName 'b)) (fn 'a -> 'b)) > > HAS-FIELD can be viewed as a realization of row sub-typing expressed in > ad-hoc form through the constraint system. If we ignore issues arising > from inheritance, this is sufficient to support full polymorphism over > structures, and it apparently works just fine for structures containing > methods. If the type of x is known, then the constraints solve in the > obvious way. From: > > (define (f x:S) x.fld) > > we would infer: > > (forall ((has-field S FieldName 'b)) (fn S -> 'b)) > > We can then determine syntactically that S has such a field, and we can > immediately resolve the type of 'b. > > This got me to wondering: is this good enough to get us to single > inheritance for programmers who want it? The answer seems to be > "almost". Let me walk through my thinking and let's see if we can show > where it breaks: > > First, note that the structure declaration and the equivalent has-field > constraints can be viewed as interchangeable. That is, given the > structure definition: > > (defstruct S i:int f:loat) > > the following two typings seem to be entirely equivalent and > interchangeable (please excuse the missing quantification): > > S ((has-field S i int), (has-field S f float)) > > Indeed, the left typing implies the right typing, which is why we can > remove the constraint in the previous example. > > So what strikes me here is that the main problem in getting from here to > single inheritance is virtual methods where the type of the override > differs in some way from the type of the base. Looking over the work in > F-Bounded polymorphism > <http://www.cs.utexas.edu/~wcook/papers/FBound89/CookFBound89.pdf>, it > seems to me that the root problem comes from two goals that may not be > important: > > * The desire to preserve subtyping across methods involving > recursive type, and > * The desire not to /lose/ type information when an operation like > Move is invoked. > > It seems to me that the first goal is unnecessary, and the second goal > is more than we require in order to deal with CTS. I am wondering if an > ad-hoc solution will not suffice in practice to give us what /current/ > OO languages with single inheritance provide in practice. > > What I am imagining is that we think of virtual functions as consisting > of an "ordered union type". That is: a sequence of types of > progressively decreasing desirability. When resolving a method call site > with a call, we proceed down this list right to left, where the > rightmost type is the most derived virtual overload that is visible > given the type information at hand, and the leftmost type is the /least/ > derived virtual declaration. If we find any legal match under the usual > rules, then the call is permitted. > > Union types of this form are not union types in the general sense. > First, there is a resolution order yielding a particular, concrete > resolution. Second, they arise only in constrained syntactic contexts. > Third, the ordering relationship is syntactically derivable from the > class declarations, and therefore need not be inferred. A type > inference implementation for this may require back-tracking in the type > checker, but that is already required for constraints in general, so I > see no major new issue here in that respect. > > Given the amount of effort that has gone into subtyping and subclassing > over the years, this seem FAR too obvious to actually work, or surely > somebody would have noticed by now. > > Can anybody explain why this won't work? I grant from the outset that > it's just plain ugly, but then, that seems somehow appropriate in the > context of a discussion of OO code... :-) > > > shap > > > > _______________________________________________ > bitc-dev mailing list > [email protected] > http://www.coyotos.org/mailman/listinfo/bitc-dev _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
