From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr 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 134CFBC57 for ; Thu, 16 Dec 2010 09:47:16 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AucAAA5hCU3RVditkGdsb2JhbACcBwGIJAgVAQECCQkMBxEEIKZUiXCCGIUyLohXAQEDBYVFBIp7iTc X-IronPort-AV: E=Sophos;i="4.59,354,1288566000"; d="scan'208";a="82865844" Received: from mail-qy0-f173.google.com ([209.85.216.173]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-MD5; 16 Dec 2010 09:47:15 +0100 Received: by qyk1 with SMTP id 1so56442qyk.18 for ; Thu, 16 Dec 2010 00:47:14 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:mime-version:sender:received :in-reply-to:references:from:date:x-google-sender-auth:message-id :subject:to:cc:content-type; bh=uh6PzpQD9+4kZzkjQaB1mlVQjy+xKshar3Q6R1Z3KIQ=; b=VZa56ciYCVzHdDceuJP6FF9gHoSnkkjKnqxMZ3jqHnfn6B5wjHAAkl+M24oSmz3Kif 7SArU9xEEoW3ZejXHNVCartgE/8UhLMJ9UvnTSWtwRmLtOt9mIrEoqSzZfs4iNjxT5Cb NXb233P/xgDY1rswcggaVDb+DgvWTI8v5cWII= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type; b=LC2XoldifcjwIIUUfjABfPErTOTwt8lfp5KZuUnZ5QbiaW95AqMcZ2/d7AQpvm+qTs 8gaoRl8oOICADOjwif9iyj9+RXpkoFKA95r7uqpBF1f4WI+RnklBZw3ru4ouBELmb7+a w67BBjXXu7RzPGZWNJPgMTMQhZLztmjt+AHQw= Received: by 10.229.222.3 with SMTP id ie3mr1372552qcb.274.1292489233568; Thu, 16 Dec 2010 00:47:13 -0800 (PST) MIME-Version: 1.0 Sender: gabriel.scherer@gmail.com Received: by 10.229.23.139 with HTTP; Thu, 16 Dec 2010 00:46:53 -0800 (PST) In-Reply-To: <20101216083217.GC29535@apus.ethz.ch> References: <20101214203043.GA9093@apus.ethz.ch> <4D087CDF.7000004@imag.fr> <20101216083217.GC29535@apus.ethz.ch> From: bluestorm Date: Thu, 16 Dec 2010 09:46:53 +0100 X-Google-Sender-Auth: CYHTuiY1rXUcn56qRFahsV4lWg8 Message-ID: Subject: Re: [Caml-list] type of high order functions To: Alexander Bernauer Cc: caml-list@yquem.inria.fr Content-Type: multipart/alternative; boundary=001636284baaa495c20497831973 X-Spam: no; 0.00; semantics:01 quantified:01 inference:01 alain's:01 syntaxes:01 ocaml:01 lexically:01 haskell:01 haskell:01 ocaml:01 semantics:01 quantified:01 inference:01 alain's:01 syntaxes:01 --001636284baaa495c20497831973 Content-Type: text/plain; charset=ISO-8859-1 On Thu, Dec 16, 2010 at 9:32 AM, Alexander Bernauer wrote: > If I don't specify a type, what's the inferred type of f? If I restrict > f to the exact same type it should do no harm. At least, that is what I > expected. As Alain explained, the annotation you wrote is *not* the exact same type. It's a different type where the scope of the 'a variable is wider, and therefore less general. If you want to have the same semantics as the inferred type (that is, a type variable quantified in the "let" declaration-side but not use-side), you must use one of the recently-introduced variable scoping constructs. You're right that the scope rules for type inference variables are muddy at best. This long underestimated issue has recently been under investigation, as you can see with Alain's proposal (both syntaxes being only available since the latest 3.12 version of OCaml), or the "Lexically scoped type variables" [1] paper in the Haskell community (which describes and compare the mutually incompatible behaviors of SML, Haskell and OCaml). [1] http://research.microsoft.com/en-us/um/people/simonpj/papers/scoped-tyvars/ --001636284baaa495c20497831973 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable On Thu, Dec 16, 2010 at 9:32 AM, Alexander Bernauer <<= a href=3D"mailto:bernauer@inf.ethz.ch">bernauer@inf.ethz.ch> = wrote:
If I don't specify a type, what's the inferred ty= pe of f? If I restrict
f to the exact same type it should do no harm. At least, that is what I
expected.

As Alain explained, the annotatio= n you wrote is *not* the exact same type. It's a different type where t= he scope of the 'a variable is wider, and therefore less general. If yo= u want to have the same semantics as the inferred type (that is, a type var= iable quantified in the "let" declaration-side but not use-side),= you must use one of the recently-introduced variable scoping constructs.

You're right that the scope rules for type inferenc= e variables are muddy at best. This long underestimated issue has recently = been under investigation, as you can see with Alain's proposal (both sy= ntaxes being only available since the latest 3.12 version of OCaml), or the= "Lexically scoped type variables" [1] paper in the Haskell commu= nity (which describes and compare the mutually incompatible behaviors of SM= L, Haskell and OCaml).

--001636284baaa495c20497831973--