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 TAA01774; Fri, 2 Jul 2004 19:36:54 +0200 (MET DST)
X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f
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 TAA01752 for <caml-list@pauillac.inria.fr>; Fri, 2 Jul 2004 19:36:53 +0200 (MET DST)
Received: from mail.dcs.qmul.ac.uk (vicar.dcs.qmul.ac.uk [138.37.95.146])
	by nez-perce.inria.fr (8.12.10/8.12.10) with ESMTP id i62HaqEV024504
	for <caml-list@inria.fr>; Fri, 2 Jul 2004 19:36:52 +0200
Received: from xenografia.plus.com ([212.159.85.26] helo=dcs.qmul.ac.uk)
	by mail.dcs.qmul.ac.uk with asmtp (TLSv1:DHE-RSA-AES256-SHA:256)
	(Exim 4.34)
	id 1BgRxz-0007xy-Le
	for caml-list@inria.fr; Fri, 02 Jul 2004 18:36:52 +0100
Message-ID: <40E59D30.1080202@dcs.qmul.ac.uk>
Date: Fri, 02 Jul 2004 18:36:48 +0100
From: Martin Berger <martinb@dcs.qmul.ac.uk>
User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.6) Gecko/20040124
X-Accept-Language: en, en-us, de-de, ru, pt-br
MIME-Version: 1.0
To: The Caml Trade <caml-list@inria.fr>
Subject: [Caml-list] Y combinator and type-checking
Content-Type: text/plain; charset=us-ascii; format=flowed
Content-Transfer-Encoding: 7bit
X-DCS-Auth-User: martinb
X-DCS-clamav-result: clean (1BgRxz-0007xy-Le)
X-DCS-uvscan-result: clean (1BgRxz-0007xy-Le)
X-Miltered: at nez-perce with ID 40E59D34.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)!
X-Loop: caml-list@inria.fr
X-Spam: no; 0.00; combinator:01 combinator:01 val:01 annotate:01 inferred:01 annotating:01 -rectypes:01 val:01 inferred:01 annotated:01 beginners:01 ocaml:01 ocaml:01 rec:01 rec:01 
Sender: owner-caml-list@pauillac.inria.fr
Precedence: bulk

i just noticed something confusing: consider an implementation of the
Y combinator (for a CBV language):

     let rec y f = f (fun x -> (y f) x );;

let's see what ocaml says about this definition.

     # let rec y f = f (fun x -> (y f) x );;
     val y : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>

now i annotate the definition above with the types just
inferred:

     let rec y  ( f : ( 'a -> 'b ) -> 'a -> 'b )
            : ( ( 'a -> 'b ) -> 'a -> 'b ) -> 'a -> 'b
       = f (fun x -> (y f) x );;

suddenly, ocaml complains:

     #let rec y  ( f : ( 'a -> 'b ) -> 'a -> 'b )
              : ( ( 'a -> 'b ) -> 'a -> 'b ) -> 'a -> 'b
         = f (fun x -> (y f) x );;

     This expression has type 'a -> 'b -> 'c but is here used with
     type (('a -> 'b -> 'c) -> 'a -> 'b -> 'c) -> 'a -> 'b -> 'c


why would annotating a program with seemingly correct types render
a program untypable? this is my main question.

here's a related observation: if we run the last program under "ocaml
-rectypes" instead of just "ocaml" we get

     # let rec y  ( f : ( 'a -> 'b ) -> 'a -> 'b )
              : ( ( 'a -> 'b ) -> 'a -> 'b ) -> 'a -> 'b
         = f (fun x -> (y f) x );;
     val y :
     (((('a -> ('a -> 'b as 'b)) -> 'a -> 'b as 'a) -> 'b) -> 'a
     -> 'b) -> 'a -> 'b = <fun>

so now the typechecker gives a thumbs-up, but the inferred and annotated
types differ. why?

I hope this is not a well-known beginners issue!

martin

-------------------
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