From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id SAA09858; Sun, 1 Dec 2002 18:31:04 +0100 (MET) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f 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 SAA10721 for ; Sun, 1 Dec 2002 18:31:03 +0100 (MET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id gB1HUuX27219; Sun, 1 Dec 2002 18:30:56 +0100 (MET) Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id SAA10480; Sun, 1 Dec 2002 18:30:55 +0100 (MET) From: Pierre Weis Message-Id: <200212011730.SAA10480@pauillac.inria.fr> Subject: Re: [Caml-list] Understanding why Ocaml doesn't support operator overloading. In-Reply-To: <20021130214138.GA19662@force.stwing.upenn.edu> from William Lovas at "Nov 30, 102 04:41:39 pm" To: wlovas@stwing.upenn.edu (William Lovas) Date: Sun, 1 Dec 2002 18:30:55 +0100 (MET) Cc: caml-list@inria.fr X-Mailer: ELM [version 2.4ME+ PL28 (25)] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk > On Fri, Nov 29, 2002 at 07:00:21PM -0500, Mike Lin wrote: > > If this is really a problem then what gets generated when you write any > > polymorphic function at all? > > I think the whole idea behind polymorphic functions is that they don't > *care* about the type that 'a is instantiated as -- generic code that works > for all instantiations can be generated. This is only really useful for > parametrized types, like 'a list, which is why it's called parametric > polymorphism. Although, you are right in that parametric polymorphism shines when used with parameterized types, this far from being the only use of it. > As an exercise, try to write a useful function that operates > on just 'a's -- you'll find it a challenge :) (in fact, i think there's a > theorem in one of Philip Wadler's papers that says the *only* function of > type 'a -> 'a in a purely functional language is the identity function). This is a theorem that was stated about $\lambda$-calculus long time ago, way before Phil Wadler's papers, back to Reynolds as I remember. The challenge you proposed is not so difficult in Caml. You can easily define functions that operates on justs'a's, or even just return plain 'a's! Objective Caml version 3.06+18 (2002-11-07) # raise;; - : exn -> 'a = # ignore;; - : 'a -> unit = Furthermore, this is even easier if you consider using true side effects that we have in Caml. > > The proposal is to allow constrained > > polymorphism; the polymorphism that is already in OCaml seems to > > supersede this with regard to the above objection. > > Overloading is also known as ad-hoc polymorphism, which as i understand it > basically means "rule-based" -- you can't generate generic code, but you > can generate all possibilites and pick the right one based on some set of > rules. This is untrue. You can generate fully generic code for ad-hoc polymorphic functions without bothering to generate ``all possibilities''. See Jun Furuse's thesis (http://pauillac.inria.fr/~furuse/thesis/). > Just because "constrained polymorphism" seems less powerful than fully > parametric polymorphism doesn't mean it's just as tractable. The analogy > that immediately came to mind for me comes from theory of computation -- a > subset of a regular language is not necessarily regular, even though it's > smaller. This is not right as well. Extensional polymorphism is MORE powerful than fully parametric polymorphism, in that it can express all parametric polymorphism types and functions, plus types and functions that you have not even dreamed of! Once more, have a look to http://pauillac.inria.fr/~furuse/thesis/ or POPL'95 initial article (ftp://ftp.inria.fr/INRIA/Projects/cristal/Pierre.Weis/generics.dvi.Z) > > I wonder if the unification algorithm can be generalized to intersect > > sets of allowable types instead of unifying "for all" type variables. > > It doesn't seem too ludicrous in principle but I could easily have > > missed some nasty corner case. > > The type inference algorithm simply assigns type variables to expressions, > generates a set of constraints based on how those expressions are put > together, and then `unifies' those constraints to make sure that they don't > lead to any contradictory equalities, like `int = float'. Trying to > generalize this would mean changing the `=' relation to something more > interesting, like maybe subset containment or something. Clearly, this > would not be a trivial undertaking.. This is correct. That's why the extensional polymorphism theory is based on the usual plain unification, for both efficiency and conservativity with respect to the Caml langauge considerations. > There has been research into "intersection types", but i don't know if they > have anything to do with your proposal... maybe someone else can shed some > light? > > cheers, > William > ------------------- > To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr > Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Pierre Weis INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://pauillac.inria.fr/~weis/ ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners