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=2.8 required=5.0 tests=DNS_FROM_RFC_POST,SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 700D0BC37 for ; Wed, 29 Jul 2009 07:37:46 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgYCAFJ9b0pKfU4aimdsb2JhbACZSz8BAQEKCQwHEQWoT4EfkBcBAwIEhAwF X-IronPort-AV: E=Sophos;i="4.43,287,1246831200"; d="scan'208";a="31827634" Received: from ey-out-2122.google.com ([74.125.78.26]) by mail3-smtp-sop.national.inria.fr with ESMTP; 29 Jul 2009 07:37:46 +0200 Received: by ey-out-2122.google.com with SMTP id 4so124553eyf.15 for ; Tue, 28 Jul 2009 22:37:45 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:message-id:date:from :user-agent:mime-version:to:cc:subject:references:in-reply-to :content-type:content-transfer-encoding; bh=/7Kw+UNAyk4k696n91kzPH1Fht697N5zU3y9eVpQx8o=; b=tbg4dN04KpcZ6BniGH5O/fFCF4M4sQQrxxfw24dYbfLB0k5C1x2w1ucIR2M1N728/J zrRagCV3LlhxPw0HEqupBuZoKGvpIp2YfKCvlyDHu4V0dyl5CVVvCyM7SbRY+7ISEb/S +menOpeDklNZBy6PKURki6eI/EiI0r/UqTPI0= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:user-agent:mime-version:to:cc:subject :references:in-reply-to:content-type:content-transfer-encoding; b=avUML7hHZqTOVRgegMOfX1UKNOVGezqFXBaic12DeVyBydYrdt3lUxn1/NZGZUngcd 7+gsvBC/NoWWl8qNObQJKQLIZM/Fb5K3ZJKkQzPFAaLk0oiMPbN4KIJabdWXVo+Wx65O HKepcfyrtVKFhmOSc+ooBPbUEHg2QGkHGPsxg= Received: by 10.210.13.12 with SMTP id 12mr10945524ebm.98.1248845865556; Tue, 28 Jul 2009 22:37:45 -0700 (PDT) Received: from ?192.168.1.22? (227.88.196-77.rev.gaoland.net [77.196.88.227]) by mx.google.com with ESMTPS id 10sm1596419eyd.10.2009.07.28.22.37.44 (version=TLSv1/SSLv3 cipher=RC4-MD5); Tue, 28 Jul 2009 22:37:44 -0700 (PDT) Message-ID: <4A6FE050.2040803@gmail.com> Date: Wed, 29 Jul 2009 07:38:24 +0200 From: Johannes Kanig User-Agent: Thunderbird 2.0.0.22 (X11/20090608) MIME-Version: 1.0 To: Philippe Cc: Jon Harrop , "caml-list@yquem.inria.fr" Subject: Re: [Caml-list] annotations and type-checking References: <200907290028.29488.jon@ffconsultancy.com> In-Reply-To: Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit X-Spam: no; 0.00; annotations:01 quantifiers:01 quantified:01 transforming:01 val:01 bool:01 annotations:01 bool:01 28,:98 harmless:98 wrote:01 caml-list:01 int:01 int:01 expression:02 Philippe wrote: > Le 29 juil. 09 à 01:28, Jon Harrop a écrit : >> I'm guessing the scope of the 'a is not what you'd expect but I have >> no idea >> why. I'd have thought the latter would be a harmless type annotation... > > My guess is that the problem here is not about scope but about > quantifiers : the type of f is quantified universally by default but the > annotation constrains the type of f to a fixed (yet unknown) type in the > subsequent expression (in that sense, yes, the scope of f plays a > crucial role). I think John Harrop is right and the scope of 'a is really the issue here. First of all, transforming "let ... in" into a top-level let makes the code work again: # let f (x : 'a) : 'a = x;; val f : 'a -> 'a = # f true;; - : bool = true # f 3;; - : int = 3 which suggests that the scope of type variables in annotations is a top-level let-binding. I think I have read about this somewhere, but I can't find the right page of the manual ... Also, the following code fails: # let f (x : 'a) : 'a = x in (f true, (3 : 'a));; Error: This expression has type int but an expression was expected of type bool Here it is clear that all annotations are talking about the same variable 'a. If 'a was existentially bound twice (once for the function definition, once for the constant 3), a type error would not occur. Johannes