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=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 9978ABC69 for ; Mon, 26 Mar 2007 16:24:52 +0200 (CEST) Received: from [128.93.11.95] (estephe.inria.fr [128.93.11.95]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l2QEOJsq015453; Mon, 26 Mar 2007 16:24:19 +0200 Message-ID: <4607D791.30202@inria.fr> Date: Mon, 26 Mar 2007 16:24:17 +0200 From: Xavier Leroy User-Agent: Thunderbird 1.5.0.7 (X11/20060915) MIME-Version: 1.0 To: Derek Dreyer Cc: Stephen Weeks , caml-list@yquem.inria.fr Subject: Re: [Caml-list] question on type checking References: <604682010703201120j54305a8dmf7174f434cedfa96@mail.gmail.com> <604682010703211813j12529ba1h5f4931fe69dcd88f@mail.gmail.com> In-Reply-To: X-Enigmail-Version: 0.94.0.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 4607D793.001 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 ocaml:01 generative:01 functor:01 derek:98 equality:01 equality:01 abstract: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 Thanks for this very interesting suggestion. As Derek knows, there are two deep limitations in the syntactic type system for modules used in OCaml, namely 1) at most one type equality can be recorded per type declaration, and 2) structure equality is not tracked, therefore the types F(M).t and F(N).t (assuming t is abstract in F's result signature) are distinct even if N is an alias for M. I managed to convince myself that the problems with applicative functors discussed e.g. in PR#3476 cannot be solved without lifting one of these limitations, which is something I don't know how to do (neither theoretically nor implementation-wise). Derek's suggestion seems to prove me wrong. The two definitions of signature strengthening (the one in my papers, used in OCaml, and Derek's proposal) appear to have the same expressive power in a system with generative functors, but Derek's definition is definitely stronger in conjunction with applicative functors. > 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? Difficult to implement: I don't think so. Would not work: some formal soundness argument would be nice of course :-), but there is a strong intuition that at the point of the ";" in the equation above, the two paths "x_i" and "p.x" carry the same amount of typing information, so replacing the latter by the former appears sound. Best wishes, - Xavier