From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id NAA13920 for caml-red; Fri, 15 Dec 2000 13:56:52 +0100 (MET) 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 DAA30655 for ; Fri, 15 Dec 2000 03:25:40 +0100 (MET) Received: from kurims.kurims.kyoto-u.ac.jp (kurims.kurims.kyoto-u.ac.jp [130.54.16.1]) by concorde.inria.fr (8.11.1/8.10.0) with ESMTP id eBF2PYL02198 for ; Fri, 15 Dec 2000 03:25:35 +0100 (MET) Received: from localhost (mikan.kurims.kyoto-u.ac.jp [130.54.16.202]) by kurims.kurims.kyoto-u.ac.jp (8.9.3/3.7W) with ESMTP id LAA09096; Fri, 15 Dec 2000 11:25:23 +0900 (JST) To: orodeh@cs.huji.ac.il Cc: caml-list@inria.fr Subject: Re: Type annotations In-Reply-To: References: 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: <20001215112523T.garrigue@kurims.kyoto-u.ac.jp> Date: Fri, 15 Dec 2000 11:25:23 +0900 From: Jacques Garrigue X-Dispatcher: imput version 20000228(IM140) Sender: weis@pauillac.inria.fr > > There has been already various proposals for allowing types to be taken > > into account when typing record labels. The difficulty is that as soon > > as you make it into something useful, you loose the principal type > > property, and that some theoreticians working on ocaml wouldn't like > > it. > > The loss of the pricipal type theorem has also recently been discussed in > comp.lang.ml and comp.lang.functional. Using type-annotation by the > compiler prior (call this the PRIOR approach) to unification can help > typing expression that cannot be typed otherwise. For example, cases of > polymoriphic recursion. In fact, this is the way this is handled in > Haskell (this topic has also appeared in this list previously). > Although I wouldn't go running to implement all my code in Haskell :-), I > do think that using PRIOR could be an improvement. > > Is there a problem with PRIOR? There are a few things that work well with this approach, polymorphic recursion being one. But it is not as general as it seems. A simple scheme is to assume that you can give explicitely a type to an identifier, use this type to resolve ambiguities, and check afterwards that this type is correct. With such a scheme, let w : t = {x=1;y=2} in w.x will indeed be correctly handled. However, this breaks as soon as an annotation is lacking: let w : t = {x=1;y=2} in let v = w in w.x Similarly, pairs won't work let w : t * int = ({x=1;y=2}, 3) in (fst w).x Indeed, while w was given a special "assumed" type, propagating such assumed types through definitions and function calls is much more subtle. In a paper by Didier Remy and myself [1], we designed a system that could do a fair amount of "assumed" type propagation. This was intended for providing first class polymorphism and polymorphic methods, and was implemented in Objective Label. This could also be used for typing records, while some might see it as an overkill. But this is much more complex than what you are calling PRIOR. And this is not principal in the strict meaning (due to a mischevious side-effect of the value only prolymorphism rule). I am currently working on reintegrating this feature in ocaml. However it is not yet clear whether it can be made cheap enough to make it into the main stream version (type inference becomes slower). And then some might discuss the fact it would require people to learn yet another set of rules about how assumed types are propagated. Cheers, Jacques [1] Extending ML with semi-explicit higher order polymorphism, Information and Computation 155, december 1999, pages 134-171. --------------------------------------------------------------------------- Jacques Garrigue Kyoto University garrigue at kurims.kyoto-u.ac.jp JG