From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id E4AC67F0BA for ; Wed, 8 Feb 2017 12:52:37 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=bob.atkey@gmail.com; spf=Pass smtp.mailfrom=bob.atkey@gmail.com; spf=None smtp.helo=postmaster@mail-wr0-f196.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of bob.atkey@gmail.com) identity=pra; client-ip=209.85.128.196; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="bob.atkey@gmail.com"; x-sender="bob.atkey@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of bob.atkey@gmail.com designates 209.85.128.196 as permitted sender) identity=mailfrom; client-ip=209.85.128.196; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="bob.atkey@gmail.com"; x-sender="bob.atkey@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-wr0-f196.google.com) identity=helo; client-ip=209.85.128.196; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="bob.atkey@gmail.com"; x-sender="postmaster@mail-wr0-f196.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AguNGMxZO//QdPdM0GHSmE07/LSx+4OfEezUN459i?= =?us-ascii?q?sYplN5qZpsu7bnLW6fgltlLVR4KTs6sC0LuK9fC6EjdaqdbZ6TZZL8wKD0dEwe?= =?us-ascii?q?wt3CUeQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYn?= =?us-ascii?q?br+tQt2a3IyL0LW58pjXJgFJnyaVYLVoLRzwox+CmNMRhN5YLaw80AeBi2dLdv?= =?us-ascii?q?UekWlvLxSagxXx9++/+Zdi92JbvPd3pJ0IarnzY6ltFe8QNz8hKW1gvMA=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0D5BwBaBZtYf8SAVdFdHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBhDFfg1mbdx+IfI5GhiICgmJEEwEBAQEBAQEBAQEBEgEBCQsLChs?= =?us-ascii?q?xgjMZgh4BBSMEEQgBGx4DDAYFCw0CAiYCAiMRAQUBHBMIAQGJVwEDFaM/P4wCg?= =?us-ascii?q?WsYBQEcgwkFg2kKGScNVYMyAQEBAQYBAQEBHAIGCQEIeYdGCIJihFRMgjqCXwW?= =?us-ascii?q?bcJISijAPhkaRTDKBFTeBHh8THVEXhB6CDXWIfgEBAQ?= X-IPAS-Result: =?us-ascii?q?A0D5BwBaBZtYf8SAVdFdHAEBBAEBCgEBFwEBBAEBCgEBhDF?= =?us-ascii?q?fg1mbdx+IfI5GhiICgmJEEwEBAQEBAQEBAQEBEgEBCQsLChsxgjMZgh4BBSMEE?= =?us-ascii?q?QgBGx4DDAYFCw0CAiYCAiMRAQUBHBMIAQGJVwEDFaM/P4wCgWsYBQEcgwkFg2k?= =?us-ascii?q?KGScNVYMyAQEBAQYBAQEBHAIGCQEIeYdGCIJihFRMgjqCXwWbcJISijAPhkaRT?= =?us-ascii?q?DKBFTeBHh8THVEXhB6CDXWIfgEBAQ?= X-IronPort-AV: E=Sophos;i="5.33,346,1477954800"; d="scan'208";a="259383442" Received: from mail-wr0-f196.google.com ([209.85.128.196]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 08 Feb 2017 12:52:37 +0100 Received: by mail-wr0-f196.google.com with SMTP id k90so8491012wrc.3 for ; Wed, 08 Feb 2017 03:52:37 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:references:from:message-id:date:user-agent:mime-version :in-reply-to:content-transfer-encoding; bh=pcQ/2Hx8J2+BSR3Hemv81UEs1TTNl328ap3wNkBWhKE=; b=X4VGpAI8A6Ddx8aWxFMyBsD5iuQ1E4HAwXLkISyYMrmuD+FaH7P1cGpsq41hkOdS5q +JzYdHnU9TF8e4bscoLjxjrQFka8heSDqYnH/z4YnboEUvY4Mn7KBO50u6gMJq2/ggFP vnzpXjjVHp88Jg2Jf8TdjsqifGJMZKx1ERL98LDdm5Cd3ZPJN7YGgQTLTcuR69peLn1T KPJKII0Deyy0/9gJRTPFVsk3YEbTxLtK3ty6r43F5E45k8/CgsGR/MDbXg0z23G0n759 6yJJVT1aCsA547ghTJ7HSvX0HnWal/PbhUIulDdodIOKAWSZ0mJsUTEYyFVyl28Ovi3a OR3A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:subject:to:references:from:message-id:date :user-agent:mime-version:in-reply-to:content-transfer-encoding; bh=pcQ/2Hx8J2+BSR3Hemv81UEs1TTNl328ap3wNkBWhKE=; b=j0j679IKnkdIVgfZUmXeOPSrFKHZJbALb3YRNO8lVuuvzGV7Uur9HxJBxaTngqarDd L6XII0IlAGt1NuZCJ76siSF729F1rf8vN6wRZliYLnxAK1l3YyajhgCP+gHrBwHiYPay itys5J+djffXe+DLUYY0qyZnKGNLScTexPOAyjvVlFWL6Caqly/6ph/Y7fiSRjeIyoPR xVPaFA9MmSOSj5qe560XcD8mjfjp5QXESnsx6VF0tPHvOQAlJ3r3s27PK5OhJu0eSYxN VuaQNT2MGnnfhfGRpmIyxv10xLDQjGbjq926iXf/krOUj1yOS4h3I0295fO62MpiPxdL 1PMg== X-Gm-Message-State: AIkVDXK2xpN1i55qErDUPbV6IaWyEbdtMGX5qzxDm4UiemgSTYdrtMBcWCjcCpJvMEUT0Q== X-Received: by 10.223.148.2 with SMTP id 2mr20398413wrq.75.1486554756814; Wed, 08 Feb 2017 03:52:36 -0800 (PST) Received: from [129.215.111.58] ([129.215.111.58]) by smtp.gmail.com with ESMTPSA id w70sm12535189wrc.47.2017.02.08.03.52.35 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 08 Feb 2017 03:52:36 -0800 (PST) To: caml-list@inria.fr References: <87tw86rwq8.fsf@ed.ac.uk> From: Robert Atkey Message-ID: Date: Wed, 8 Feb 2017 11:52:35 +0000 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.7.0 MIME-Version: 1.0 In-Reply-To: <87tw86rwq8.fsf@ed.ac.uk> Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] Help with recursive modules and functors 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 >