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 8FCEA7EF10 for ; Mon, 9 Mar 2015 09:50:11 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of leo@lpw25.net) identity=pra; client-ip=66.111.4.224; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="leo@lpw25.net"; x-sender="leo@lpw25.net"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of leo@lpw25.net) identity=mailfrom; client-ip=66.111.4.224; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="leo@lpw25.net"; x-sender="leo@lpw25.net"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@new2-smtp.messagingengine.com) identity=helo; client-ip=66.111.4.224; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="leo@lpw25.net"; x-sender="postmaster@new2-smtp.messagingengine.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0B/AADcXf1UnOAEb0JahDKDCsU6AoEoTQEBAQEBARABAQEBAQYNCQkULoQQAQQBIwQZOgQLCwQWAiYCAiwriEAIpm1whGiWNgEBAQEGAQEBAQEXBoEhiXaEdRaCFwwvEh2BFopugySfSYQxHjGCQwEBAQ X-IPAS-Result: A0B/AADcXf1UnOAEb0JahDKDCsU6AoEoTQEBAQEBARABAQEBAQYNCQkULoQQAQQBIwQZOgQLCwQWAiYCAiwriEAIpm1whGiWNgEBAQEGAQEBAQEXBoEhiXaEdRaCFwwvEh2BFopugySfSYQxHjGCQwEBAQ X-IronPort-AV: E=Sophos;i="5.11,366,1422918000"; d="scan'208,217";a="102568289" Received: from new2-smtp.messagingengine.com ([66.111.4.224]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 09 Mar 2015 09:50:10 +0100 Received: from compute2.internal (compute2.nyi.internal [10.202.2.42]) by mailnew.nyi.internal (Postfix) with ESMTP id 106AE1860 for ; Mon, 9 Mar 2015 04:50:07 -0400 (EDT) Received: from web3 ([10.202.2.213]) by compute2.internal (MEProxy); Mon, 09 Mar 2015 04:50:08 -0400 DKIM-Signature: v=1; a=rsa-sha1; c=relaxed/relaxed; d=lpw25.net; h= message-id:x-sasl-enc:from:to:mime-version :content-transfer-encoding:content-type:in-reply-to:references :subject:date; s=mesmtp; bh=ZCbSiSk9GJnozMOTLwG9Ph8A1E0=; b=Cgm+ sFtxpTXNTFehgutyI5EDre11o5BpxJv+CaMnRBDqR8SyXJWR6smUcXWQVuU3oJSt sJyK0IZ57+UXn/wJdvq/qr+UcZK958QgssleJxLWCImG1LbQPu7RJYRPhK0HtUtj BhNHy3ftbwXtpWkkl+KXhrTwWwD/T4v9Y9HNvkM= DKIM-Signature: v=1; a=rsa-sha1; c=relaxed/relaxed; d= messagingengine.com; h=message-id:x-sasl-enc:from:to :mime-version:content-transfer-encoding:content-type:in-reply-to :references:subject:date; s=smtpout; bh=ZCbSiSk9GJnozMOTLwG9Ph8A 1E0=; b=E2c92lMZieUuzlqyBc7UZksLAVkjtDXYYiYQComlPhK4zqfFKRSpRg67 krnsieDwyzRxfpQy/cmBRQ+XIJwGn9hcwXUqrquoQs5ajhdiW3c0sYYypOtJcnWX OxWQDLEFM3enCz9yNBOC0cgKKgd0w4SB3tLLtPp+M5FK03NgPTE= Received: by web3.nyi.internal (Postfix, from userid 99) id 24009116DDA; Mon, 9 Mar 2015 04:50:08 -0400 (EDT) Message-Id: <1425891008.3125906.237731925.21BB0F13@webmail.messagingengine.com> X-Sasl-Enc: PJ8R/EW/KR8dQMJmEy5LtVNR68LNUEJoEhvjwKN7N+7S 1425891008 From: Leo White To: caml-list@inria.fr MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: multipart/alternative; boundary="_----------=_142589100831259061"; charset="utf-8" X-Mailer: MessagingEngine.com Webmail Interface - ajax-07699171 In-Reply-To: References: Date: Mon, 09 Mar 2015 01:50:08 -0700 Subject: Re: [Caml-list] Signature substitution deleting an exposed type alias This is a multi-part message in MIME format. --_----------=_142589100831259061 Content-Transfer-Encoding: 7bit Content-Type: text/plain > 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 --_----------=_142589100831259061 Content-Transfer-Encoding: 7bit Content-Type: text/html
> 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
--_----------=_142589100831259061--