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.0 required=5.0 tests=AWL,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 discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id 7B4E6BC69 for ; Thu, 22 Mar 2007 05:32:14 +0100 (CET) Received: from wx-out-0506.google.com (wx-out-0506.google.com [66.249.82.228]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l2M4WDrt019009 for ; Thu, 22 Mar 2007 05:32:14 +0100 Received: by wx-out-0506.google.com with SMTP id i26so679003wxd for ; Wed, 21 Mar 2007 21:32:13 -0700 (PDT) DKIM-Signature: a=rsa-sha1; c=relaxed/relaxed; d=gmail.com; s=beta; h=domainkey-signature:received:received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=iDi42kHy0vyeVo/gTApw6bZ7EZex/CLqsdVXD7gTyt5vCVKp9RQ4zKB4CoFSefyOILKKc6IcfOUOWX84YFUvMKHFZIStI2HeHWHcIU3qYV8o3IuJ1He2H+UgWQ6vVQB5BJ9wfLVRwTqWCLV+w+KxmDunCjP6zFNrNLrrX2rhPnk= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=kmiacDEL0iwrqXLpidzMhQQT0Y8NHhSxrnEzZ1F+TnJWGciOTjDZOXOta+GuUOj1nY1wO+WYxhStq22MU0EXENcmaD6rUyMQbfmba/hc/MOqz3jlY1kBFgvwyIO9rGrCed1paJqW0H5f8twmUWJu2PksPIebK4GQl6qv73apvfk= Received: by 10.90.25.3 with SMTP id 3mr3014673agy.1174537933151; Wed, 21 Mar 2007 21:32:13 -0700 (PDT) Received: by 10.90.115.19 with HTTP; Wed, 21 Mar 2007 21:32:13 -0700 (PDT) Message-ID: Date: Wed, 21 Mar 2007 23:32:13 -0500 From: "Derek Dreyer" To: "Stephen Weeks" Subject: Re: [Caml-list] question on type checking Cc: caml-list@yquem.inria.fr In-Reply-To: <604682010703211813j12529ba1h5f4931fe69dcd88f@mail.gmail.com> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Content-Disposition: inline References: <604682010703201120j54305a8dmf7174f434cedfa96@mail.gmail.com> <604682010703211813j12529ba1h5f4931fe69dcd88f@mail.gmail.com> X-j-chkmail-Score: MSGID : 460206CD.000 on discorde : j-chkmail score : X : 0/20 1 0.000 -> 1 X-Miltered: at discorde with ID 460206CD.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; xavier's:01 applicative:01 functors:01 applicative:01 functors:01 ocaml:01 bug:01 typechecker:01 functor:01 bug:01 markus:01 mottl:01 derek:98 derek:98 wrote:01 Very interesting. So now, looking back at Xavier's POPL'95 paper on applicative functors, I see what he means by saying it's a fundamental problem with how applicative functors work in OCaml. I.e. it's not just a bug in the typechecker, but in the type system in the original paper. In particular, the definition of signature strengthening on page 7 of that paper includes the following case: (module x_i : M; S)/p = module x_i : (M/p.x); S/p But I believe this is a mistake, and instead of S/p it should be (S{x_i <- p.x})/p In other words, first replace references to x_i (esp. in functor applications in types) inside S with references to p.x, and then proceed with selfification as usual. Is there some reason this would not work or would be difficult to implement? I believe this would eliminate the bugs we're looking at here. And I'm sort of surprised that this would be hard to do, but I'm not familiar with the implementation. Derek On 3/21/07, Stephen Weeks wrote: > Thanks for the reply Derek. I also thought it looked like a bug, and > your explanation makes sense. However, Markus Mottl pointed me to the > following issue in the bug tracker > > http://caml.inria.fr/mantis/view.php?id=3476 > > The problem there looks very similar, and would seem to indicate that > the situation is not viewed as a bug (in the sense that it won't be > fixed). >