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=1.2 required=5.0 tests=AWL,SPF_FAIL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id 80B3EBB84 for ; Wed, 14 Jan 2009 16:52:55 +0100 (CET) X-IronPort-AV: E=Sophos;i="4.37,263,1231110000"; d="scan'208";a="22469869" Received: from concorde.inria.fr ([192.93.2.39]) by mail1-smtp-roc.national.inria.fr with ESMTP; 14 Jan 2009 16:52:55 +0100 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id n0EFqsdK009791 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Wed, 14 Jan 2009 16:52:55 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AlIBAP+YbUkmachml2dsb2JhbACUFgEBAQEBCBUHuhyFbw X-IronPort-AV: E=Sophos;i="4.37,263,1231110000"; d="scan'208";a="33733405" Received: from mx2.janestcapital.com ([38.105.200.102]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 14 Jan 2009 16:52:54 +0100 Received: from nyc-qsv-mail1.delacy.com ([172.25.22.57]) by mx2.janestcapital.com with esmtp (Exim 4.69) (envelope-from ) id 1LN80M-0001JA-0W; Wed, 14 Jan 2009 10:50:06 -0500 Received: from nyc-qsv-004.delacy.com ([172.25.22.194] helo=qsmtp.delacy.com) by nyc-qsv-mail1.DELACY.com with esmtps (TLSv1:AES256-SHA:256) (Exim 4.69) (envelope-from ) id 1LN832-0000ag-P8; Wed, 14 Jan 2009 10:52:52 -0500 Received: from lon-qws-008.delacy.com ([172.30.3.108] helo=lon-qws-008) by qsmtp.delacy.com with smtp (Exim 4.63) (envelope-from ) id 1LN831-0006CI-L3; Wed, 14 Jan 2009 10:52:52 -0500 Received: by lon-qws-008 (sSMTP sendmail emulation); Wed, 14 Jan 2009 15:52:50 +0000 From: "Mark Shinwell" Date: Wed, 14 Jan 2009 15:52:50 +0000 To: Julien SIGNOLES Cc: caml-list@inria.fr Subject: Re: [Caml-list] Caml implementation of the relaxed value restriction Message-ID: <20090114155250.GJ28444@janestcapital.com> References: <1231947084.7199.34.camel@localhost> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <1231947084.7199.34.camel@localhost> User-Agent: Mutt/1.5.18 (2008-05-17) X-Miltered: at concorde with ID 496E0A56.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; shinwell:01 0100,:01 signoles:01 ocaml:01 sig:01 val:01 val:01 struct:01 ocaml:01 cvs:01 compiler:01 2009:98 wrote:01 abstract:01 typing:01 On Wed, Jan 14, 2009 at 04:31:24PM +0100, Julien SIGNOLES wrote: > In the article "Many Holes in Hindley-Milner" [1], Sam Lindley claims > that the type of x is ('a * 'a s, int) NList.t in the following ocaml > program because of Garrigue's relaxed value restriction [2]. > ========== > type 'a s > > module NList : sig > type (+'length, +'elem_type) t > val nil : ('m*'m, 'a) t > val cons: 'a * ('m*'n, 'a) t -> ('m*'n s,'a) t > end = struct > type ('i,'a) t = 'a list > let nil = [] > let cons (x, l) = x :: l > end > > let x = NList.cons (1, NList.nil) > ========== > > But, both with ocaml v3.10.2 and ocaml v3.12.0+dev1 (2008-12-03) (that > is the current cvs version), the infered type of [x] only contains a > weak type variable: ('_a * '_a s, int) NList.t. > > I quickly look at the typing rules introduced by Jacques Garrigue in [2] > and it seems to me that Sam Lindley is right: [x] is generalisable in > the above program. > > So, what's wrong here? You need to say "type +'a s", otherwise the compiler (since "s" is an abstract type) cannot know the variance of that type parameter inside a value of type 'a s. That information is needed to determine how to generalize the type of x. Mark