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 LAA23292; Sun, 14 Sep 2003 11:48:18 +0200 (MET DST) Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id LAA29485 for ; Sun, 14 Sep 2003 11:48:17 +0200 (MET DST) Received: from nef.ens.fr (nef.ens.fr [129.199.96.32]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id h8E9mHT00510 for ; Sun, 14 Sep 2003 11:48:17 +0200 (MET DST) Received: from clipper.ens.fr (clipper-gw.ens.fr [129.199.1.22]) by nef.ens.fr (8.12.9/1.01.28121999) with ESMTP id h8E9mHlL082369 ; Sun, 14 Sep 2003 11:48:17 +0200 (CEST) Received: from localhost (frisch@localhost) by clipper.ens.fr (8.12.3/jb-1.1) id h8E9mFmw011294 ; Sun, 14 Sep 2003 11:48:15 +0200 (MET DST) X-Authentication-Warning: clipper.ens.fr: frisch owned process doing -bs Date: Sun, 14 Sep 2003 11:48:15 +0200 (MET DST) From: Alain.Frisch@ens.fr X-X-Sender: frisch@clipper.ens.fr Reply-To: Alain.Frisch@ens.fr To: skaller cc: Caml list Subject: Re: [Caml-list] inference engine In-Reply-To: <1063512749.23073.28.camel@pelican> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Virus-Scanned: by amavisd-milter (http://amavis.org/) X-Loop: caml-list@inria.fr X-Spam: no; 0.00; alain:01 frisch:01 caml-list:01 inference:01 inference:01 troll:01 checker:01 checker:01 unification:01 int':01 unification:01 recursion:01 alain:01 ocaml:01 ocaml:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk On 14 Sep 2003, skaller wrote: > I'll try. At present, with > > let f (x:int) = x +. 1.0 > > the inference engine goes: I keep wondering if you're trying some kind of troll here, or if you're serious. When you're saying "At present the inference engine goes..", what do you mean? Have you tried your examples with the actual OCaml type checker? As a matter of fact, the type checker performs unification with the constraints on arguments of functions as soon as possible. You don't need any extra notion like 'mandatory typing' to do this. > > let f (x:int) * = x .+ 1.0 --> x is 'a > let f (x:int) = x .+ * 1.0 --> 'a is restricted to float > let f (x:int*) = x +. 1.0 --> float is restricted to int ERROR > > where the * marks the position in the analysis: the constraint of > x to int is applied *after* the type is already deduced. No, that's not how it works. Try the example with OCaml. > To do that I'm suggesting to give x the type 'at least an int', > meaning any subsequent typing of x in the function body > must be constrainable to int -- and that is checked every time > additional information is obtained by the inference engine > to refine the type. Do you know about unification? > For another example: OCaml does report the error where you expect. Try the example with OCaml. > in particular, in the case like: > > let rec f1 (x1:t1):r1 = .. > and f2 (x2:t2):r2 = ... > and f3 (x2:t3):r3 = .. > ... > and f999 (x999:t999):r999 = ... > > the fact the the constraints t1, r1, t2, t2, .. > are not applied until after the whole recursion > is typed Again, this is wrong. -- Alain ------------------- 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