From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 6883BBBAF for ; Thu, 10 Sep 2009 21:19:21 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AnoBAIvtqEpV2gB4mWdsb2JhbACbQAEBAQEJCwoHE8NOhBgFils X-IronPort-AV: E=Sophos;i="4.44,366,1249250400"; d="scan'208";a="34041446" Received: from emailfrontal1.citycable.ch ([85.218.0.120]) by mail3-smtp-sop.national.inria.fr with SMTP; 10 Sep 2009 21:19:20 +0200 Received: from [192.168.0.10] (unknown [85.218.92.99]) (Authenticated sender: guillaume.yziquel@citycable.ch) by emailfrontal1.citycable.ch (Postfix) with ESMTPA id 9756312C2B5; Thu, 10 Sep 2009 21:19:14 +0200 (CEST) Message-ID: <4AA95027.5050308@citycable.ch> Date: Thu, 10 Sep 2009 21:14:47 +0200 From: Guillaume Yziquel Reply-To: guillaume.yziquel@citycable.ch User-Agent: Mozilla-Thunderbird 2.0.0.19 (X11/20090103) MIME-Version: 1.0 To: Jacques Garrigue Cc: caml-list@inria.fr Subject: Re: [Caml-list] polymorphic method. References: <4AA8F16F.1040009@citycable.ch> <20090910.214827.104047449.garrigue@math.nagoya-u.ac.jp> <4AA8F986.1060206@citycable.ch> <20090910.232102.112610940.garrigue@math.nagoya-u.ac.jp> In-Reply-To: <20090910.232102.112610940.garrigue@math.nagoya-u.ac.jp> Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: quoted-printable X-Spam: no; 0.00; guillaume:01 guillaume:01 recursion:01 doable:01 principality:01 'self:01 'self:01 typable:01 typable:01 val:01 val:01 annotations:01 polymorphism:01 compiler:01 inference:01 Jacques Garrigue a =C3=A9crit : > From: Guillaume Yziquel > >> By the way, I do not exactly understand the "you might end up with >> types more polymorphic than you expected" part. >=20 > This is actually the main problem. > At some point, I actually considered generating automatically > polymorphic method types where possible. > The idea would be simply to first give all the methods in a class > monomorphic types (to avoid the undecidability of polymorphic recursion= ),=20 > and then generalize all type variables that do not "escape": i.e. do > not appear in class parameters, value fields, or global references. > Technically this is perfectly doable. Yes, I figured that out. > Theoretically, there are problems with principality, as there is no > most generic type for a polymorphic method (all types are incompatible > with each other). > It is easier to see that on a practical example. > Say that I defined lists: >=20 > class ['a] cons x l =3D object (_ : 'self) > method hd : 'a =3D x > method tl : 'self =3D l > end >=20 > class nil =3D object > method hd =3D raise Empty > method tl =3D raise Empty > end Cute way of defining lists. > Now, both cons and nil would be typable (cons is already typable), and > the inferred types would be: > class ['a] cons : 'a -> 'b -> > object ('b) method hd : 'a method tl : 'b end >=20 > class nil : object > method hd : 'a > method tl : 'b > end >=20 > At first glance, it seems that the type of nil being completely > polymorphic, we could pass it as second argument to cons. > However, it is not the case. cons has two monomorphic methods, while > nil has two polymorhic methods, and their types are incomparable. > If we look at object types, >=20 > type 'a cons =3D < hd : 'a; tl : 'b > as 'b > type nil =3D < hd : 'a.'a ; tl : 'b.'b > >=20 > Of course, you could argue that what is wrong is the definition of > nil. But basically there is no way to decide what is the right type > for nil as soon as we allow inferring polymorphic methods. To continue on the example of nil: the current definition of nil (i.e.=20 the one with type ) would be written as > class nil : object > polymorphic method hd =3D raise Empty > polymorphic method tl =3D raise Empty > end and the definition > class nil : object > method hd =3D raise Empty > method tl =3D raise Empty > end would not compile since the 'a and the 'b would not be bound in the=20 definition of class nil. Just to be sure we are talking about the same thing. > Interestingly, currently you can define nil as an immediate object > and have immediately the right type without any annotation: >=20 > exception Empty > let nil =3D object > method hd =3D raise Empty > method tl =3D raise Empty > end ;; > val nil : < hd : 'a; tl : 'b > =3D So you're saying that what I proposed up there, saying that it would not=20 compile properly, indeed works out fine in the current setting? Isn't that inconsistent to allow 'a coming from exceptions to get bound,=20 while not doing so for some other 'a? (Sorry if I'm being unclear and=20 using approximative terminology). > let l =3D new cons 3 nil ;; > val l : int cons =3D >=20 > So, the current approach is to privilege the monomorphic case, > requiring type annotations for the polymorphic case. Your suggestion > of allowing to give a hint that you want a polymorphic type makes > sense, but it does not say which polymorphic type: there might be > several, with different levels of polymorphism, with no way to choose > between them. Probably it would be ok to choose the most polymorphic > one, but one can always find counter-examples. Humm... I still do not see why there would be ambiguity in choosing 'the=20 most general' polymorphic type... Can't 'the most polymorphic one' be=20 properly defined? > So the meaning of your > "polymorphic" keyword would be: "give me the most polymorphic type for > this method, I hope I understand what it will be, but if I'm wrong and > it breaks my program I won't complain". This may be practically ok, Yes. For me, it would be OK. Even more if 'the most polymorphic one' is=20 properly defined. I wouldn't worry too much about the 'I hope I=20 understand what it will be' in this case. > but this is a hard sell as a language feature. Particularly when you > think that future versions of the compiler may be able to infer more > polymorphic types, thanks to improvements in type inference, and > suddenly break your program. I'd like to suggest something na=C3=AFve: for each 'a type, try to bind i= t to=20 the class definition (what you call monomorphic I think), and if you=20 can't, then bind it to the method definition (what you call=20 polymorphic). (This, of course, in the presence of the 'polymorphic'=20 keyword). This seems, at least na=C3=AFvely, properly defined behaviour. And from a= =20 practical point of view, this is what I'd be looking for. Of course, that doesn't deal with improvements in the type inference=20 system, but I think it would be neat. I'm not really familiar with syntax extensions. Can this 'polymorphic'=20 keyword be implemented with a syntax extension? All the best, --=20 Guillaume Yziquel http://yziquel.homelinux.org/