From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id A0E0BBC69 for ; Fri, 23 Nov 2007 09:24:58 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao8CAKIdRkfBAkMt/2dsb2JhbAA X-IronPort-AV: E=Sophos;i="4.21,455,1188770400"; d="scan'208";a="19595380" Received: from vega.fmf.uni-lj.si (HELO postar.fmf.uni-lj.si) ([193.2.67.45]) by mail4-smtp-sop.national.inria.fr with ESMTP; 23 Nov 2007 09:24:58 +0100 Received: from localhost (unknown [192.168.5.1]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id 8B14B1AC97A; Fri, 23 Nov 2007 09:24:46 +0100 (CET) X-Virus-Scanned: amavisd-new at spam.fmf.uni-lj.si Received: from postar.fmf.uni-lj.si ([192.168.5.5]) by localhost (spam.fmf.uni-lj.si [192.168.5.1]) (amavisd-new, port 10024) with ESMTP id t3aIe7eLgxHb; Fri, 23 Nov 2007 09:24:44 +0100 (CET) Received: from [193.2.67.88] (unknown [193.2.67.88]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id A38471DFF61; Fri, 23 Nov 2007 09:24:43 +0100 (CET) Message-ID: <47468EAC.1070602@fmf.uni-lj.si> Date: Fri, 23 Nov 2007 09:26:20 +0100 From: Andrej Bauer Reply-To: Andrej.Bauer@andrej.com User-Agent: Thunderbird 2.0.0.6 (X11/20071022) MIME-Version: 1.0 To: Jonathan T Bryant Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Type issue References: <2921298.1195790493072.JavaMail.jtbryant@valdosta.edu> In-Reply-To: <2921298.1195790493072.JavaMail.jtbryant@valdosta.edu> Content-Type: text/plain; charset=ISO-8859-2; format=flowed Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; andrej:01 andrej:01 bool:01 bool:01 ocaml:01 unification:01 caml-list:01 algorithm:01 guess:04 simpler:05 reasoning:07 looks:08 fun:08 fun:08 bauer:09 Here's a simpler example: # fun (g, x) -> (g true, g x) ;; - : (bool -> 'a) * bool -> 'a * 'a = Even though it looks like g could be of type 'b -> 'a, ocaml decides to go with bool only. I see this on the mailing list every once in a while, but I always forget the reasoning behind it. If I had to guess, it's just a result of unification algorithm in type reconstruction (which, incidentally I thought in class 20 minutes ago...). Starting from g : 'b -> 'a x : 'c we get these equations: 'b = bool because true must have type 'b 'c = 'b because x must have type 'b And now we get 'b = 'c = bool, hence the result. Andrej