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.3 required=5.0 tests=AWL,DNS_FROM_RFC_POST autolearn=disabled version=3.1.3 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id AB8F2BC69 for ; Fri, 28 Dec 2007 13:46:54 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AlwPABJ/dEfUKEUHYmdsb2JhbACBV44rFQQGEBmBFJsi X-IronPort-AV: E=Sophos;i="4.24,216,1196636400"; d="scan'208";a="5576789" Received: from mail.dravanet.hu (HELO arwen.dravanet.hu) ([212.40.69.7]) by mail2-smtp-roc.national.inria.fr with ESMTP; 28 Dec 2007 13:46:54 +0100 Received: from arwen-vbmailshield (localhost.localdomain [127.0.0.1]) by arwen-vbmailshield (Postfix) with SMTP id 7600C129B for ; Fri, 28 Dec 2007 13:46:53 +0100 (CET) Received: from arwen.dravanet.hu ([127.0.0.1]) by arwen ([192.168.69.23]) with SMTP (gateway) id A0300A5D543; Fri, 28 Dec 2007 13:46:53 +0100 Received: from [127.0.0.1] (unknown [212.40.86.228]) by arwen.dravanet.hu (Postfix) with ESMTP id 098771748 for ; Fri, 28 Dec 2007 13:46:52 +0100 (CET) Message-ID: <4774F02F.4070506@dravanet.hu> Date: Fri, 28 Dec 2007 13:46:39 +0100 From: =?ISO-8859-1?Q?=22M=E1rk_S=2E_Zolt=E1n=22?= User-Agent: Thunderbird 2.0.0.9 (Windows/20071031) MIME-Version: 1.0 To: Caml Mailing List Subject: Re: [Caml-list] Type visibility limitation in recursive modules References: <476E6FB7.6040100@dravanet.hu> <476F9B82.2060103@dravanet.hu> <47743194.1080801@dravanet.hu> <20071228.190210.68534327.keiko@kurims.kyoto-u.ac.jp> In-Reply-To: <20071228.190210.68534327.keiko@kurims.kyoto-u.ac.jp> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Antivirus: avast! (VPS 071215-0, 12/15/2007), Outbound message X-Antivirus-Status: Clean X-VBMailShield: version 1.57.6 at arwen - template: default X-Spam: no; 0.00; recursive:01 bug:01 bug:01 kludge:01 ocaml:01 checker:01 structs:01 strengthened:01 doable:01 compiler:01 compiler:01 annotations:01 rewriting:01 sig:01 sig:01 Keiko Nakata wrote: > Hello. > > I have not thoroughly read your posts, > but it looks like the double vision problem. > > You may be interested in the following post to camllist: > > http://caml.inria.fr/pub/ml-archives/caml-list/2007/06/0d23465b5b04f72fedecdd3bbf2c9d72.en.html > Thanks; somehow I haven't found that particular post when I was searching for precedents. Not having managed to understand the double vision problem, I still I happen to think it is not a good explanation in this case for many reasons. Even Xavier agrees in the above linked post that this is a bug of the current implementation, i.e. not a theoretical issue. If it was due to some sort of theoretical difficulty, variant types would fail at it too, but they don't. This is a plain bug - the way type equations are stored is a kludge, as it uses the type-manifest field which already plays an only distantly related role. > By the way, I believe one can hack the OCaml type checker > to (mostly) avoid the problem by "strengthening" > the external signature of the recursively defined module > in the type environment. Something like this is actually done in the code - when typing the structs, the encountered type declarations are strengthened to point to themselves as seen from outside of the module. The problem is that this is only doable for variant and record types due to legacy design decisions in the actual implementation, namely that type abbreviations are represented in the current implementation in a way which does not allow storing the results of such strenghtening, and that the compiler silently passes over a type it cannot strenghten this way, probably in the hope of not causing hard-to-relate problems later. I really find it hard to emphasize enough that this cannot be a theoretical impossibility if it works for variant types. Unless you are talking about some other kind of hack, in which case I'd be very grateful to hear more details. > But this is not particularly beautiful > since a type constructor may escape its scope, > although the implementation is kept sound > You mean like in http://caml.inria.fr/mantis/view.php?id=3993 ? The situation is caught by the compiler, fortunately, so I don't feel worried about it. I wonder, though, if there is any other way for this escape to happen except the '_a-style delayed typing, like ref [], which IMHO should be rejected as untypeable in the absence of explicit type annotations, not courteously typed to '_a list. > I would be very happy if you could give me a practical example > which suffers from the double vision problem. > I could give you the skeleton of what I am trying to implement, which is a pattern matching & rewriting engine. I am not sure if it is a practical example of the double vision problem, since I don't know what it is. module type NumbersS : sig ... end module type AtomsS : sig ... end module type ReprS : sig module Numbers : NumbersS module Atoms : AtomsS module rec Terms : sig type t = ... end and Seq : sig type t ... end end module RepresentationF = functor(N : NumbersS) -> functor(A : AtomsS) -> (struct module Numbers = N module Atoms = A module rec Terms : sig ... end = struct ... ...end and Seq : sig type t ... end = struct type t = Terms.t list ... end end : ReprS with module Numbers = N and module Atoms = A) module type RewriterS = sig module Numbers : NumbersS module Atoms : AtomsS module Representation : ReprS with module Atoms = Atoms and module Numbers = Numbers ... end module RewriterF = functor(N : NumbersS) -> functor(A : AtomsS) -> functor(R : ReprS with module Atoms = A and module Numbers = N) -> (struct ... end : RewriterS with module Numbers = N and module Atoms = A and module Representation = R) module MyNumbers : NumbersS = struct .. end module rec MyAtoms : sig ... end = struct ... end and MyRepresentation : ReprS with module Numbers = MyNumbers and module Atoms = MyAtoms = RepresentationF(MyNumbers)(MyAtoms) and MyRewriter : RewriterS with module Numbers = MyNumbers and module Atoms = MyAtoms and module Representation = MyRepresentation = RewriterF(MyNumbers)(MyAtoms)(MyRepresentation) and Driver : sig ... end = struct ... ... end Basically, I want to - separate the numeric part (plain OCaml numeric types vs. Bignum lib vs. ocamlgmp). - postpone decisions about the actual structure of atoms (this code will be reused in many projects, and in some of them atoms may contain complex structures making use of Representation.Terms.t and Representation.Seq.t) - isolate the implementation details of Seq from Terms (Seq.t: list? array? map?) and make sure Terms does not make assumptions about the Seq.t type (the struct of Terms is a huge mess of legacy code) - keep the pattern-matching and rewriting bytecode engine isolated from the representation details - keep the actual driver separate from the rewriter too (the same Rewriter could be used with different drivers, e.g. one with memoizing, one without, one with memoizing open to explicit insertion of memoized cases; the driver might make use of builtins for certain kinds of terms, sport a typing system or not - and it would probably store lots of such information in the atoms, not in maps from atoms to information). Of course there are other, non-rec ways to get there, but I don't want to just yet. Apart from arriving to a more straightforward code using module rec, this is a hobby project, so I can afford to wait for a solution. Cheers Z-