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.6 required=5.0 tests=AWL autolearn=disabled version=3.1.3 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 2C663BBAF for ; Thu, 21 Aug 2008 13:00:39 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AvgCAMvnrEjAXQIniGdsb2JhbACRXj4BAQEPIJxDhk4BAoNr X-IronPort-AV: E=Sophos;i="4.32,245,1217800800"; d="scan'208";a="28393119" Received: from concorde.inria.fr ([192.93.2.39]) by mail4-smtp-sop.national.inria.fr with ESMTP; 21 Aug 2008 13:00:38 +0200 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m7LB0bU1003621 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 21 Aug 2008 13:00:38 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AnsBAJDnrEjRVcirlGdsb2JhbACRXj4BAQEBCQMKBxEDnD+GTgECg2s X-IronPort-AV: E=Sophos;i="4.32,245,1217800800"; d="scan'208";a="14157180" Received: from wf-out-1314.google.com ([209.85.200.171]) by mail2-smtp-roc.national.inria.fr with ESMTP; 21 Aug 2008 13:00:37 +0200 Received: by wf-out-1314.google.com with SMTP id 25so1007234wfa.0 for ; Thu, 21 Aug 2008 04:00:36 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:message-id:date:from:sender :to:subject:cc:in-reply-to:mime-version:content-type :content-transfer-encoding:content-disposition:references :x-google-sender-auth; bh=5UqmxFSUVS7PN0m60eZVpeDijSzTOqa/hbtcrUSF6RY=; b=fDwW7tify5fCapEMpf/LmgCNfEnKY7aMnc5OSUnbvuL3MmWIHqLEVGKVIww/FvPRnf oNlcAnbDYVH2bTIuqgRlhm5NnFYSCJeofiJwbpf8qTReLP09yVJKqQvLXXvcpvDSgOpg 2p5oEWXHXelLsK33JBsQnGWCJ7Tv7cCefyQ3I= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:sender:to:subject:cc:in-reply-to:mime-version :content-type:content-transfer-encoding:content-disposition :references:x-google-sender-auth; b=tom3sVmPyefabEjAZgFmsYHWVpEWQ2VkSNVXGl2e+FLotOdkV5q43eUYWOZFkf5TN3 yQj4kK2dP0lsMs6d7ZmMJ8TnaHmQnZIoipqK2uipLULxw29MCpY90jBnFw/dc1p5fYPP 1D6XP+FdAJh3bjg0uut7JjyVj1OnFhlPDsRsA= Received: by 10.142.217.17 with SMTP id p17mr443937wfg.23.1219316436113; Thu, 21 Aug 2008 04:00:36 -0700 (PDT) Received: by 10.142.105.11 with HTTP; Thu, 21 Aug 2008 04:00:36 -0700 (PDT) Message-ID: <2b7b425b0808210400j618e461fre54f73612b920e4a@mail.gmail.com> Date: Thu, 21 Aug 2008 13:00:36 +0200 From: "=?ISO-8859-1?Q?J=E9r=E9mie_Lumbroso?=" Sender: jeremie.lumbroso@gmail.com To: "Keiko Nakata" Subject: Re: [Caml-list] Separating two mutually recursive modules Cc: caml-list@inria.fr In-Reply-To: <20080821.182901.68534700.keiko@kurims.kyoto-u.ac.jp> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Content-Disposition: inline References: <2b7b425b0808201654i61d3f878gbed5c27ca9114438@mail.gmail.com> <20080821.182901.68534700.keiko@kurims.kyoto-u.ac.jp> X-Google-Sender-Auth: 8eedd4064510edf6 X-Miltered: at concorde with ID 48AD4AD6.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; recursive:01 checker:01 recursive:01 contrarily:01 sig:01 sig:01 node:01 val:01 struct:01 anil:01 val:01 bool:01 bool:01 struct:01 anil:01 Hello, > Can I look at the code which does not type check without Obj.magic? > Ideally something like if I comment out Obj.magic then I get a type > error, and if I comment it in then the code type checks, so that I can > identify the point of the issue? (In the context of this simplified > example of Boxes & Validator) Yes, and thank you for taking an interest! I do have a warning though: this code is not correct, in the sense that, it doesn't type and it *shouldn't* type (because while in this case Validator.Boxes.t *is* equivalent to B.t, there is nothing but my "good will" that guarantees in the specs of the modules that this is so). Attempts to make this correct (for the type checker) with "with type" conditions have failed. The mutually recursive version I posted in the previous message is an "evolution" from this (and that mutually recursive version, contrarily to this one is "correct"). module type BOXES_PROVIDER =3D sig type t end module type VALIDATOR =3D sig module Boxes : BOXES_PROVIDER type t =3D Me of int | Node of t * t | B of Boxes.t val fold_on_B : (Boxes.t -> 'a) -> ('a -> 'a -> 'a) -> 'a -> t -> 'a end module BoxesProvider(Validator : VALIDATOR) : BOXES_PROVIDER =3D struct module rec A : sig type t =3D | Anil =09 | Aout of Validator.t val o_f : ('a -> bool) -> ('a -> bool) -> t -> bool end =3D struct type t =3D | Anil =09 | Aout of Validator.t (* There is no equality between Validator.Boxes.t and B.t, i.e.: failing to see this is not a problem with the typechecker. To get the type error, replace with "let crosstype x =3D x". *) let crosstype (x : Validator.Boxes.t) =3D ((Obj.magic x) : B.t) let o_f p1 p2 =3D let rec aux =3D function =09| Anil -> false =09| Aout tv -> =09 Validator.fold_on_B (fun x -> B.o_f p1 p2 (crosstype x)) (||) fals= e tv in aux end and B : sig type t =3D | Bnil =09 | Bout of A.t * t =09=09 val o_f : ('a -> bool) -> ('a -> bool) -> t -> bool end =3D struct type t =3D | Bnil =09 | Bout of A.t * t =09=09 let o_f p1 p2 =3D let rec aux =3D function =09| Bnil -> false =09| Bout(a, tv) -> (A.o_f p1 p2 a) || (aux tv) in aux end type t =3D B.t end module rec Validator : VALIDATOR (* with type Boxes.t =3D Validator.Boxes.t ?? *) =3D struct module Boxes =3D BoxesProvider(Validator) type t =3D Me of int | Node of t * t | B of Boxes.t let fold_on_B f combinator default =3D let rec aux =3D function | Node(b1, b2) -> combinator (aux b1) (aux b2) | B r=09 -> f r | _ =09 -> default in aux end > > (********************) > > (* MODULE Validator *) > > (********************) > > > > and Validator : sig > > > > (* This type has been simplified for explanatory purposes. *) > > (* IDEALLY, Boxes.B.t would simply be B.t. *) > > type t =3D Me of int | Node of t * t | B of Boxes.B.t > > > > val fold_on_B : (Boxes.B.t -> 'a) -> ('a -> 'a -> 'a) -> 'a -> t ->= 'a > > > > end =3D > > But B is not in the scope, isn't it? Indeed. What I meant to say is, "IDEALLY, Boxes.B.t would simply be Boxes.t" (and Validator would not need to know about submodules A and/or B). Please, of course, don't hesitate to ask for any other details you might need (and don't hesitate to tell me if this Obj.magic code is not what you needed!). All the best, J=E9r=E9mie