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 KAA17427; Tue, 10 Apr 2001 10:22:40 +0200 (MET DST) 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 KAA17423 for ; Tue, 10 Apr 2001 10:22:39 +0200 (MET DST) Received: from psyche.kaba.or.jp (psyche.kaba.or.jp [202.249.19.1]) by concorde.inria.fr (8.11.1/8.10.0) with ESMTP id f3A8Mab15541 for ; Tue, 10 Apr 2001 10:22:36 +0200 (MET DST) Received: from vortex.kaba.or.jp (vortex.kaba.or.jp [202.249.19.21]) by psyche.kaba.or.jp (8.9.3/3.7Wpl2-psyche) with ESMTP id RAA75132; Tue, 10 Apr 2001 17:22:31 +0900 (JST) Received: from localhost (pmdhcp06.kaba.or.jp [202.249.19.118]) by vortex.kaba.or.jp (8.9.3/3.7W) with ESMTP id RAA26541; Tue, 10 Apr 2001 17:22:30 +0900 (JST) To: Judicael.Courant@lri.fr Cc: caml-list@inria.fr Subject: Re: [Caml-list] Future of labels, and ideas for library labelling In-Reply-To: <3AD2B970.BEB88A8@lri.fr> References: <4.3.2.7.2.20010409124220.00d4a810@shell16.ba.best.com> <20010410123756H.garrigue@kurims.kyoto-u.ac.jp> <3AD2B970.BEB88A8@lri.fr> X-Mailer: Mew version 1.94.2 on Emacs 20.7 / Mule 4.0 (HANANOEN) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-Id: <20010410172527K.garrigue@kurims.kyoto-u.ac.jp> Date: Tue, 10 Apr 2001 17:25:27 +0900 From: Jacques Garrigue X-Dispatcher: imput version 20000228(IM140) Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk From: Judicael Courant > > [ Disclaimer: you can safely skip this message if you are not > > interested in labels. It is about modalities of use for people who > > want them. ] > > So, is there no way out? > > Not completely, if we accept to start from strict unification: > [...] > > I can not really assess if this solution is good. However, it sounds to > me like a hack. I am rather suspicious of hack, be they clever as long > as they are not proven harmless (through a metatheoretical study). What > are the chances then that we experience bad behaviours of this hack > because of a lack of good theoretical properties? Just in case I confused anybody, this idea of allowing to omit some labels is an extension of the label mode, not the classic mode. As I explained, the classic mode itself is currently a terrible hack, and trying to extend it is bound to fail. For this idea, the reason it is more than a hack is that it can be proved unambiguous: * the application is complete, and typing would fail otherwise * ocaml's label mode does not allow unification between differently ordered function types, so that positional application is unambiguous * this is of course coherent with the unlabeled case So, you can see it as an overloading hack, but you can also build a metatheory for it. There are even ways to make this typing principal... The only weakness is that it is not compatible with unification of differently ordered function types, but this was removed from ocaml as non conform to call-by-value semantics. Jacques Garrigue ------------------- To unsubscribe, mail caml-list-request@inria.fr. Archives: http://caml.inria.fr