From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: weis Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id LAA11452 for caml-redistribution; Wed, 27 May 1998 11:25:55 +0200 (MET DST) Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id LAA31863 for ; Tue, 26 May 1998 11:22:54 +0200 (MET DST) Received: from morgon.inria.fr (morgon.inria.fr [128.93.8.33]) by concorde.inria.fr (8.8.7/8.8.7) with ESMTP id LAA28761; Tue, 26 May 1998 11:22:47 +0200 (MET DST) Received: (from remy@localhost) by morgon.inria.fr (8.8.7/8.8.7) id LAA19825; Tue, 26 May 1998 11:24:35 +0200 Message-ID: <19980526112435.51973@morgon.inria.fr> Date: Tue, 26 May 1998 11:24:35 +0200 From: Didier Remy To: Hendrik Tews Cc: caml-list@inria.fr Subject: Re: co(ntra)-variant subtyping Reply-To: Didier.Remy@inria.fr References: <199805201500.RAA19129@ithif18.inf.tu-dresden.de> <19980522112157L.garrigue@kurims.kyoto-u.ac.jp> <199805251146.NAA21664@ithif18.inf.tu-dresden.de> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Mailer: Mutt 0.85e In-Reply-To: <199805251146.NAA21664@ithif18.inf.tu-dresden.de>; from Hendrik Tews on Mon, May 25, 1998 at 01:46:19PM +0200 Organization: INRIA, BP 105, F-78153 Le Chesnay Cedex Phone: (33) 1 3963 5317 -- Sec: (33) 1 3963 5570 -- Fax: (33) 1 3963 5684 Web: http://pauillac.inria.fr/~remy Sender: weis > Objective Caml's subtyping algorithm does not subtype under type > constructors (but it does it under abbreviations), for the sake of > efficiency. That is, eventhough colored_point :> point, you don't have > colored_point option :> point option. This equation would be needed to > check the subtyping in method move of example 2. > > I must say I am really surprised. > > How about object types? Do they support co(ntra)-variant > subtype rules? As Jacques said, subtyping sees through abbreviations. Object types are abbreviations. They are covariant except when self-type occurs negatively, in which case they are non-variant. > I would suggest to include a section about the subtype relation > in the ocaml documentation. We are aware that the documentation is too succinct. We will keep improving it. > Because IMHO anybody how knows > something about formal models for oo languages would expect > co(ntra)-variant subtype rules. I leave you this opinion. Traditionally, people have heavily relied on subtyping polymorphism; they run into serious difficulties because of the bad interaction between recursion, late-binding and contra-variance. This lead to some mistakes (some languages got it wrong). Moreover they still have difficulties with binary methods. For instance, even though Java is explicitly typed, it fails to type binary methods: the type of self is weakened to the current type of the class, which forces later useless and unsafe coercions (they may fail, dynamically). Instead, Objective Caml relies on parametric polymorphism. This is easier to explain, often more powerful (here, binary methods are not a problem) and allows simple type inference. This is really what makes Objective Caml work. Actually, Objective Caml does work with no subtyping at all, i.e. polymorphic message invocation, inheritance, binary methods, etc. all work without subtyping. Indeed, many examples do not use subtyping at all. Still, Objective Caml allows subtyping because they are a few situations when it is convenient. Typically, when storing a collection of objects of different subclasses of a common parent class into a bag. Then, only the operations of the parent class can be directly invoked on the objects of the collection. (Actually, subtyping is independent from the class hierarchy and objects do not need to be in an inheritance relation to be put in the same collection.) > In summary I think the lack of these subtype rules are a major > restriction of the ocaml language. I am not convinced that the current restriction is such a burden. You are one of the first person to complain... > Now it is not possible to mix > class types and (algebraic) data types in an application. Instead > a user has to decide beforehand what is more important for him: > algebraic data types and parametric polymorphism or object types > with code reuse and stepwise refinement. Maybe you could detail your examples. > Are there any plans to add the missing subtype rules to the type > system of ocaml? In fact, there is no real difficulty to allow subtyping through user-declared type constructors. However, when types are abstract (e.g. in module interfaces) the user would need to declare the variances of the constructors in their arguments. We did not want to add yet another notion in the language, and therefore we prefered to make all non-primitive type constructors non variant. Didier