From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <garrigue@math.nagoya-u.ac.jp>
X-Original-To: caml-list@sympa.inria.fr
Delivered-To: caml-list@sympa.inria.fr
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 777D67EE51
	for <caml-list@sympa.inria.fr>; Sat,  4 May 2013 14:47:06 +0200 (CEST)
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  garrigue@math.nagoya-u.ac.jp) identity=pra;
  client-ip=133.6.130.5;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="garrigue@math.nagoya-u.ac.jp";
  x-sender="garrigue@math.nagoya-u.ac.jp";
  x-conformance=sidf_compatible
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  garrigue@math.nagoya-u.ac.jp) identity=mailfrom;
  client-ip=133.6.130.5;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="garrigue@math.nagoya-u.ac.jp";
  x-sender="garrigue@math.nagoya-u.ac.jp";
  x-conformance=sidf_compatible
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo;
  client-ip=133.6.130.5;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="garrigue@math.nagoya-u.ac.jp";
  x-sender="postmaster@mailhost.math.nagoya-u.ac.jp";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: Aj8EAI0ChVGFBoIFdGdsb2JhbABQwwGBEg4BDBUIPIIfAQEEASccATUCAwsLNBJXBhOIBgWve4RFAoU/hzYHjn4zB4JyYYkbjhSUTg
X-IPAS-Result: Aj8EAI0ChVGFBoIFdGdsb2JhbABQwwGBEg4BDBUIPIIfAQEEASccATUCAwsLNBJXBhOIBgWve4RFAoU/hzYHjn4zB4JyYYkbjhSUTg
X-IronPort-AV: E=Sophos;i="4.87,611,1363129200"; 
   d="scan'208";a="13194337"
Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5])
  by mail3-smtp-sop.national.inria.fr with ESMTP; 04 May 2013 14:47:03 +0200
Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1])
	by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 4F2C1638C;
	Sat,  4 May 2013 21:47:01 +0900 (JST)
Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1])
	by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 0D845252A;
	Sat,  4 May 2013 21:47:01 +0900 (JST)
DomainKey-Signature: h=Received:Subject:Mime-Version:Content-Type:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=; c=nofws; d=math.nagoya-u.ac.jp; q=; s=alpha
Received: from tanpopo.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157])
	by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id BF0DA2503;
	Sat,  4 May 2013 21:47:00 +0900 (JST)
Mime-Version: 1.0 (Mac OS X Mail 6.3 \(1503\))
Content-Type: text/plain; charset=iso-8859-1
From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
In-Reply-To: <5184FDB0.30406@inria.fr>
Date: Sat, 4 May 2013 21:47:17 +0900
Cc: caml-list@inria.fr
Content-Transfer-Encoding: quoted-printable
Message-Id: <492B4A0C-06A9-4B72-83E7-5DC585690EC3@math.nagoya-u.ac.jp>
References: <5184FDB0.30406@inria.fr>
To: =?iso-8859-1?Q?Micha=EBl_Lienhardt?= <michael.lienhardt@inria.fr>
X-Mailer: Apple Mail (2.1503)
Subject: Re: [Caml-list] recursive module type


On 2013/05/04, at 21:23, Micha=EBl Lienhardt <michael.lienhardt@inria.fr> w=
rote:

> Hello,
>=20
> I would like to define some recursive module type in caml, like
> module type S =3D sig
> ...
> module Toto(M : S) : sig
>  ...
> end
> end
>=20
> More precisely, I'd like to extend the Set module available in the ocaml =
distribution with a function that convert a set into another set.
> Intuitively, I came up with the following signature S, which is not accep=
ted by ocaml (Error: Unbound module type S):
>=20
>  module type S =3D sig
>=20
>    include Set.S
>=20
>    module Convert : functor(SetTarget : S) -> sig
>      val convert : (elt -> SetTarget.elt) -> t -> SetTarget.t
>    end
>  end

You first problem is syntactic.
You cannot define recursive signatures, just recursive modules.
But the signature may refer recursively to the module.
So you can attempt to write the following:

module rec M : sig
  module type S =3D sig=20=20
     include Set.S
     module Convert : functor(SetTarget :M.S) -> sig=20=20=20=20=20=20=20=
=20=20=20
       val convert : (elt -> SetTarget.elt) -> t -> SetTarget.t
     end
   end
end =3D M;;

unfortunately, this does not work:
Fatal error: exception Env.Recmodule

And this is not surprising, because this would let you indeed define
a recursive signature (i.e. a signature that unfolds infinitely).

Jacques Garrigue=