From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 5688F7F0BA for ; Wed, 8 Feb 2017 23:28:47 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=phil.scott@ed.ac.uk; spf=None smtp.mailfrom=phil.scott@ed.ac.uk; spf=None smtp.helo=postmaster@loire.is.ed.ac.uk Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of phil.scott@ed.ac.uk) identity=pra; client-ip=129.215.16.10; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="phil.scott@ed.ac.uk"; x-sender="phil.scott@ed.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of phil.scott@ed.ac.uk) identity=mailfrom; client-ip=129.215.16.10; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="phil.scott@ed.ac.uk"; x-sender="phil.scott@ed.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@loire.is.ed.ac.uk) identity=helo; client-ip=129.215.16.10; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="phil.scott@ed.ac.uk"; x-sender="postmaster@loire.is.ed.ac.uk"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3Ay93XtR/XQ7/gDP9uRHKM819IXTAuvvDOBiVQ1KB4?= =?us-ascii?q?1e8cTK2v8tzYMVDF4r011RmSDNmdu6kP07CempujcFRI2YyGvnEGfc4EfD4+ou?= =?us-ascii?q?JSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgpp?= =?us-ascii?q?POT1HZPZg9iq2+yo9ZDeZwpFiCC+bL58Ixm6sRvdvdQKjIV/Lao81gHHqWZSde?= =?us-ascii?q?RMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZ?= =?us-ascii?q?TQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/9KpgVgPmhz?= =?us-ascii?q?kbOD446GHXi9J/jKRHoBK6uhdzx5fYbJyJOPZie6/Qe84RS2hcUcZLTyFBDI2z?= =?us-ascii?q?YYsRAeQcP+lWoYrzqFQSohalGQmgGPnixiNUinLswaE31fkqHwHc3AwnGtIDqG?= =?us-ascii?q?7arNX0NKcWTOu70bXHzTLfb/NKxDzw75DIchAgofGIR75watbeyU4zFwPZlVif?= =?us-ascii?q?t5HqMymP2esRqWSb8ulgWPuphmU6qA9xuiCiytoyhoTNnI4Z1E3I+CVjzIooJN?= =?us-ascii?q?C0UlN3bcK8HJZQqi2WLYl7TtktTmxooio21LILtJq9cSMX0poo3QTfZOaCc4WQ?= =?us-ascii?q?4hLsSuKRITBgiXJhf7K/hgyy/la6xu39Tcm4ykhFoTdfntbWqn8BzQHT6sufRv?= =?us-ascii?q?t8+EeuxyqP2hjO5u1aJU04j7TXJ4Mhz7Iqi5YesF7PEjLqlEnuia+ZbEQk+uym?= =?us-ascii?q?6+T9ZbXmo4eRN5d0igH/NqQigNe/Dvg/MggSQ2iW4vqz26D58ULjXLpGlOA2kq?= =?us-ascii?q?rBvJDAOcsbvrK5AxNS0os79xmwFTKm0NABkXkDLVJFYw6HgpPyO1DOJfD4Fe2w?= =?us-ascii?q?j06tkDdt3fDGP6fuDo/DLnjZw//deuNH7ERR0hZ75Mxc6oMcXrsGKrT6Rkz8pf?= =?us-ascii?q?TXCxY4N0q/xOOxW/tn0YZLYWKOBueiO6TOrRfc/uIuJ6+Xb4gJpB7wJ74s7Ljz?= =?us-ascii?q?jilqyhcmYaC10M5POziDFfN8LhDcOCK0jw=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DkAQBTm5tYhgoQ14FdGwEBAQMBAQEJA?= =?us-ascii?q?QEBFwEBBAEBCgEBk2ORF5dCAYYhAoJvRBMBAQEBAQEBAQEBARIBAQEKCQsKHS+?= =?us-ascii?q?CMxsBghoBAQEDASdSBQsLDgoJJQ8BLBsGiX8IA7IdOodxGoNFAQEBBwIBJSCGL?= =?us-ascii?q?IRvijkFm3CBf6EYkxM3gR4fEy5AhFWBbYlzAQEB?= X-IPAS-Result: =?us-ascii?q?A0DkAQBTm5tYhgoQ14FdGwEBAQMBAQEJAQEBFwEBBAEBCgE?= =?us-ascii?q?Bk2ORF5dCAYYhAoJvRBMBAQEBAQEBAQEBARIBAQEKCQsKHS+CMxsBghoBAQEDA?= =?us-ascii?q?SdSBQsLDgoJJQ8BLBsGiX8IA7IdOodxGoNFAQEBBwIBJSCGLIRvijkFm3CBf6E?= =?us-ascii?q?YkxM3gR4fEy5AhFWBbYlzAQEB?= X-IronPort-AV: E=Sophos;i="5.35,348,1484002800"; d="scan'208";a="212555323" Received: from loire.is.ed.ac.uk ([129.215.16.10]) by mail3-smtp-sop.national.inria.fr with ESMTP; 08 Feb 2017 23:28:42 +0100 Received: from lmtp1.ucs.ed.ac.uk (lmtp1.ucs.ed.ac.uk [129.215.149.64]) by loire.is.ed.ac.uk (8.14.7/8.14.6) with ESMTP id v18MSfFP014858; Wed, 8 Feb 2017 22:28:41 GMT Received: from hyland (249.45.7.51.dyn.plus.net [51.7.45.249]) (authenticated user=pscott7 mech=PLAIN bits=0) by lmtp1.ucs.ed.ac.uk (8.13.8/8.13.7) with ESMTP id v18MSdub008821 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NOT); Wed, 8 Feb 2017 22:28:39 GMT References: <87tw86rwq8.fsf@ed.ac.uk> User-agent: mu4e 0.9.18; emacs 25.1.1 From: Phil Scott To: Robert Atkey Cc: caml-list@inria.fr In-reply-to: Date: Wed, 08 Feb 2017 22:28:39 +0000 Message-ID: <87tw841fmw.fsf@ed.ac.uk> MIME-Version: 1.0 Content-Type: text/plain X-Scanned-By: MIMEDefang 2.78 on 129.215.16.10 X-Scanned-By: MIMEDefang 2.52 on 129.215.149.64 X-Edinburgh-Scanned: at loire.is.ed.ac.uk with MIMEDefang 2.78, Sophie, Sophos Anti-Virus, Clam AntiVirus Subject: Re: [Caml-list] Help with recursive modules and functors Cheers Bob (and Tom Ridge)! I'm through the type-checker. I'll have a play tomorrow and see if it does what I need. Robert Atkey writes: > Hi Phil, > > I'm not sure if this solves your problem, but the following seems to > work. It rewraps 'F' as 'X' in the recursive declaration, whilst > ensuring that 'X' gives the same answers as 'F' does. > > module type Foo = functor(S : sig type s val foo : s -> s end) -> > sig > type t > end > > module Bar = functor(F: Foo) -> > struct > module rec S : sig > type s = int > type baz = Baz of X(S).t > val foo : s -> s > end = > struct > type s = int > type baz = Baz of X(S).t > let foo x = x > end > and X : functor(S : sig type s val foo : s -> s end) -> > sig > type t = F(S).t > end = F > end > > I think this is the expected behaviour: > > # module B = Bar (functor (S : sig type s val foo : s -> s end) -> > struct type t = [ `X of S.s ] end);; > module B : sig > module rec S : > sig type s = int type baz = Baz of X(S).t val foo : s -> s end > and X : > functor (S : sig type s val foo : s -> s end) -> > sig type t = [ `X of S.s ] end > end > # B.S.Baz (`X 5);; > - : B.S.baz = B.S.Baz (`X 5) > > I'm not sure what the rules for typing recursive modules are, so I'm not > sure why mine type checks and yours doesn't. > > Bob > > On 07/02/17 12:50, Phil Scott wrote: >> Hi all. >> >> Suppose I have the following code: >> >> module type Foo = functor(S : sig type s val foo : s -> s end) -> >> sig >> type t >> end >> >> module Bar = >> functor(F: Foo) -> >> struct >> module rec S : >> sig >> type s = int >> type baz = Baz of F(S).t >> val foo : s -> s >> end = >> struct >> type s = int >> type baz = Baz of F(S).t >> let foo x = x >> end >> end >> >> Here, I want my Bar module to apply its supplied Foo to a recursive >> module S. However, I am being told that the functor application F(S) in >> the signature for S is ill-typed. The problems are apparently due to the >> type of baz in the signature. If I change the type so that it doesn't >> involve F(S), the type-checker is happy: >> >> module Bar = >> functor(F: Foo) -> >> struct >> module rec S : >> sig >> type s = int >> type baz = Baz >> val foo : s -> s >> end = >> struct >> type s = int >> type baz = Baz >> let foo x = x >> end >> end >> >> But this is odd to me, since baz is not even in the signature of Foo's >> argument, so I don't understand how it's type could affect the type >> correctness of the functor application. Can anyone explain to me what >> the problem is? I understand that I'm probably pushing what recursive >> modules can do, but would like some details if anyone can clear it up >> for me. >> >> Thanks! >> >> -- >> Phil Scott >> Centre for Intelligent Systems and their Applications >> University of Edinburgh >> -- Phil Scott Centre for Intelligent Systems and their Applications University of Edinburgh The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.