From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 67B2A7EEE0 for ; Wed, 18 Mar 2015 03:00:41 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of mathieu.barbin@gmail.com) identity=pra; client-ip=209.85.192.53; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mathieu.barbin@gmail.com"; x-sender="mathieu.barbin@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of mathieu.barbin@gmail.com designates 209.85.192.53 as permitted sender) identity=mailfrom; client-ip=209.85.192.53; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mathieu.barbin@gmail.com"; x-sender="mathieu.barbin@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-qg0-f53.google.com) identity=helo; client-ip=209.85.192.53; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mathieu.barbin@gmail.com"; x-sender="postmaster@mail-qg0-f53.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0CWAADx2whVlDXAVdFbhDIEy3wCgTgHTAEBAQEBAREBAQEBBwsLCRIwhBABAQMBEhUZARsdAQMBCwYFBAc7IgERAQUBHAYTIod4AQMJCKNOPjGNHIJ3kDMKGScNVIRnAQEBAQEFAQEBAQEBFgEFDosJhHEHhC0FjjaLdJJTEiOBFYQtIjGCQwEBAQ X-IPAS-Result: A0CWAADx2whVlDXAVdFbhDIEy3wCgTgHTAEBAQEBAREBAQEBBwsLCRIwhBABAQMBEhUZARsdAQMBCwYFBAc7IgERAQUBHAYTIod4AQMJCKNOPjGNHIJ3kDMKGScNVIRnAQEBAQEFAQEBAQEBFgEFDosJhHEHhC0FjjaLdJJTEiOBFYQtIjGCQwEBAQ X-IronPort-AV: E=Sophos;i="5.11,419,1422918000"; d="scan'208";a="103762789" Received: from mail-qg0-f53.google.com ([209.85.192.53]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 18 Mar 2015 03:00:40 +0100 Received: by qgfa8 with SMTP id a8so25858176qgf.0 for ; Tue, 17 Mar 2015 19:00:39 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=FuGyDBdreiYBDxgcm4uQIj6zQKDEU0YQ8IrDltTfv+k=; b=Pdj5FbMOHgV31vPNf4IV85jNnRnq6tRlepR1lDroIYCl3SoQk+/rjdYoIXwOVUhzAy 1ErNvsmaQl1ogsyFmQ+6UAK1skgkJm4kJBbU87B03jnTj3xqXdBWcY0t++DCFikxCPpD 2QRCXHVa+ZoDp0q2EiWRCVd9wPhrFKOhBhehkxFNwJFuWv/dpMcMfNy2XmFH5PrD+NkR SAE3Q9FL/8baGDzWVR/X4Xb4nF5xM8oxd6CZPiFwTo9S9x4/OCfTbnBnuOifI6xFjTPV f8vqQnoW3mSwtJMCiqfg+qXALMuERjchEtdC2Tj0SO//caX3HbI3qMvFTqgu1FRpuWLf C1Bw== MIME-Version: 1.0 X-Received: by 10.140.83.202 with SMTP id j68mr83010746qgd.18.1426644039041; Tue, 17 Mar 2015 19:00:39 -0700 (PDT) Received: by 10.229.211.2 with HTTP; Tue, 17 Mar 2015 19:00:38 -0700 (PDT) In-Reply-To: <1425891008.3125906.237731925.21BB0F13@webmail.messagingengine.com> References: <1425891008.3125906.237731925.21BB0F13@webmail.messagingengine.com> Date: Tue, 17 Mar 2015 22:00:38 -0400 Message-ID: From: Mathieu Barbin To: Leo White Cc: caml-list@inria.fr Content-Type: multipart/alternative; boundary=001a11c1379c2b0cb605118673b8 Subject: Re: [Caml-list] Signature substitution deleting an exposed type alias --001a11c1379c2b0cb605118673b8 Content-Type: text/plain; charset=ISO-8859-1 Dear Leo, Thank you for the explanation and the illustrating example. On Mon, Mar 9, 2015 at 4:50 AM, Leo White wrote: > > module type A = sig > > type t = int > > val of_int : int -> t > > end > > > > module type B = sig > > type t > > include A with type t := t > > end > > > > [...] > > > > In the example, I am not sure what exactly are the signatures involved > in the comparison, since the included signature > > does not contain the definition of the type t ( removed by the use of := > ), and without the type [t] the signature are > > virtually identical. > > The two signatures being compared are the signatures before the > definition of t is removed, so essentially: > > sig > type t = int > val of_int : int -> t > end > > is being compared with: > > sig > type t = t' > val of_int : int -> t > end > > where t' refers to the type defined by the `type t` definition in the B > signature. > > This prevents inconsistent signatures being created. For example, > > type t = T of int > > module type C = sig > type s = int > type r = t = T of s > end > > module type D = C with type s := float > > would result in: > > module type D = sig type r = t = T of float end > > which is inconsistent, since the definition does not match the equation. > > Regards, > > Leo > --001a11c1379c2b0cb605118673b8 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
Dear Leo, Thank you for the explanation and the=A0illustra= ting=A0example. =A0


On Mon, Mar 9, 2015 at 4:50 AM, Leo White <leo@lpw25.n= et> wrote:
> module type A =3D sig
> =A0 type t =3D int
> =A0 val of_int : int -> t
> end
>
> module type B =3D sig
> =A0 type t
> =A0 include A with type t :=3D t
> end
>
> [...]
>
> In the example, I am not sure what exactly are the signatures inv= olved in the comparison, since the included signature
> does not contain the definition of the type t ( removed by the us= e of :=3D ), and without the type [t] the signature are
> virtually identical.
=A0
The two signatures being compared are the signatures before the=
definition of t is removed, so essentially:
=A0
=A0 =A0 sig
=A0 =A0 =A0 type t =3D int
=A0 =A0 =A0 val of_int : int -> t
=A0 =A0 end
=A0
is being compared with:
=A0
=A0 =A0 sig
=A0 =A0 =A0 type t =3D t'
=A0 =A0 =A0 val of_int : int -> t
=A0 =A0 end
=A0
where t' refers to the type defined by the `type t` definit= ion in the B
signature.
=A0
This prevents inconsistent signatures being created. For example,
<= /div>
=A0
=A0 =A0 type t =3D T of int
=A0
=A0 =A0 module type C =3D sig
=A0 =A0 =A0 type s =3D int
=A0 =A0 =A0 type r =3D t =3D T of s
=A0 =A0 end
=A0
=A0 =A0 module type D =3D C with type s :=3D float
=A0
would result in:
=A0
=A0 =A0 module type D =3D sig type r =3D t =3D T of float end
=A0
which is inconsistent, since the definition does not match the equatio= n.
=A0
Regards,
=A0
Leo

--001a11c1379c2b0cb605118673b8--