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 BAA07483; Wed, 7 Jul 2004 01:42:05 +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 BAA06758 for ; Wed, 7 Jul 2004 01:42:04 +0200 (MET DST) Received: from moby.atcorp.com (moby.atcorp.com [204.72.172.2]) by concorde.inria.fr (8.12.10/8.12.10) with ESMTP id i66Ng2SH018558 for ; Wed, 7 Jul 2004 01:42:03 +0200 Received: from SAILFISH (conger.atcorp.com [204.72.172.102]) by moby.atcorp.com (8.11.6/8.11.2) with SMTP id i66NlJP09961; Tue, 6 Jul 2004 18:47:19 -0500 Received: by localhost with Microsoft MAPI; Tue, 6 Jul 2004 18:41:27 -0500 Message-ID: <01C46388.D8ED9F10.kmillikin@atcorp.com> From: "Kevin S. Millikin" Reply-To: "kmillikin@atcorp.com" To: "'Andy Yang'" , "caml-list@inria.fr" Subject: RE: [Caml-list] Why type infenere enter infinte loop here? Date: Tue, 6 Jul 2004 18:41:27 -0500 Organization: ATC X-Mailer: Microsoft Internet E-mail/MAPI - 8.0.0.4211 MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 40EB38CA.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; caml-list:01 2004:99 val:01 val:01 fixpoint:01 combinator:01 combinator:01 fixpoint:01 ocaml:01 ocaml:01 int:01 int:01 rec:01 rec:01 trivial:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk On Tuesday, July 06, 2004 5:25 PM, Andy Yang [SMTP:yyu08@yahoo.com] wrote: > Hi, all > > I am relatively new in Ocaml. Perhaps this problem is > trivial. With the following interactive process, ocaml > cannot give out f2's type. Could you tell me why it > cannot? > > > # let rec y f = f (fun x ->(y f) x);; > val y : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = > # let g h x = h x;; > val g : ('a -> 'b) -> 'a -> 'b = > # let f1 = y g;; > val f1 : '_a -> 'b = > # let k x = x * x + 1;; > val k : int -> int = > # let f2 = f1 k;; > For the same reason that it does not print the type of # while true do () done;; y is a fixpoint combinator. g is the application combinator (Curry's B combinator). f1 is the fixpoint of application, which does not terminating. Your definition of f1 is the same as # let f1 = y (fun h x -> h x);; which is the same as # let rec f1 = fun x -> f1 x;; An application of f1 will not terminate. The typechecker is perfectly h appy to determine that your f2 has type 'a -> 'b, but it won't print that type until it finishes computing the value. -- Kevin ------------------- 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