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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 0510F80161 for ; Tue, 20 Jun 2017 11:36:45 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=christophe@raffalli.eu; spf=Pass smtp.mailfrom=christophe@raffalli.eu; spf=None smtp.helo=postmaster@mailler06.lws-hosting.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of christophe@raffalli.eu) identity=pra; client-ip=31.207.32.247; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="christophe@raffalli.eu"; x-sender="christophe@raffalli.eu"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of christophe@raffalli.eu designates 31.207.32.247 as permitted sender) identity=mailfrom; client-ip=31.207.32.247; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="christophe@raffalli.eu"; x-sender="christophe@raffalli.eu"; 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@mailler06.lws-hosting.com) identity=helo; client-ip=31.207.32.247; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="christophe@raffalli.eu"; x-sender="postmaster@mailler06.lws-hosting.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3A4h8adBbwi0Yqlwdj3h4i3uj/LSx+4OfEezUN459i?= =?us-ascii?q?sYplN5qZoMS4bnLW6fgltlLVR4KTs6sC0LuJ9fi4EUU7or+5+EgYd5JNUxJXwe?= =?us-ascii?q?43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRp?= =?us-ascii?q?OOv1BpTSj8Oq3Oyu5pHfeQtFiT6/bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+?= =?us-ascii?q?RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPC?= =?us-ascii?q?TQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD?= =?us-ascii?q?0fOjA38G/ZlNF+gqFUrx29uhNwzZXZYI6JOPdkZK7RYckXSGhHU81MVyJBGIS8?= =?us-ascii?q?b44XAucfPeZYtYj9p0ASrRu5HQmsBP3gwSJUiHDs06063f4uEQXC3AwhAtkDt2?= =?us-ascii?q?jbrNXvNKcTSuC10K7IzS3Db/xIwjr98pLHch4vof6WWbJwdcvRxVMxGAPYl1id?= =?us-ascii?q?r5HuMTCN1ukVvWWX8vBsWfyzh2MlsQ18rCajyt0yhoTGhI8Z0k3I+CF3zYovKt?= =?us-ascii?q?C1S1R3bcO6HJZerS2WKoR7T8U/SG9yoik60KcJuZujcSgK1psnwxnfZuSCc4eS?= =?us-ascii?q?4xLjUOKRLilihH55eb+znRKy8Ea7yuHlVsm0101KrjZEktnKuXABzQDc6s+CSv?= =?us-ascii?q?dl/0eh3yiA1xzL5+xKPEw4j7TXJ4Ijz7IqmJcfr17PEjH5lUj0lKOWc18r+ums?= =?us-ascii?q?6+TpeLXmoZqcOpdohQH+KKQum9e/Afg/MggWX2iU5/+x1Kf58k33TrVFlPk2kq?= =?us-ascii?q?3YsJzAO8sbu7a1AxVJ3YY79xa/EzCm3cwEknYdKVJFfAuLj4zoO1HVPPD1Fuy/?= =?us-ascii?q?glSpkDdz3f/KJLzhApPXLnjCirjtZ7h961QPgDY0mJpU7pdQT7UAO+7bW0nrtd?= =?us-ascii?q?WeAAVze1i/yuPjTdF8zZ82WGSVA6bfPrmE4nGS4ed6COmWZZQJvy79JrAf7vDg?= =?us-ascii?q?hHs9mBdJdqmz3IALb2i4E9x8KkuXaH7og5EMDDFZ7UIFUOX2hQjaAnZobHGoUv?= =?us-ascii?q?dk6w=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0ClAQB060hZZPcgzx9chAhigQ2Da4sMn?= =?us-ascii?q?kGKUwcdiF5DFAEBAQEBAQEBAQEBAxwLCgUqJAuCMyKCbQSBDiECEUIMij8ErRO?= =?us-ascii?q?BbDqLfw+Ta4JhBYlSEog6jEOHMowiDWyBco8wlQo2gStRJluEPQEKAQEBQR2Ba?= =?us-ascii?q?HSJWQEBAQ?= X-IPAS-Result: =?us-ascii?q?A0ClAQB060hZZPcgzx9chAhigQ2Da4sMnkGKUwcdiF5DFAE?= =?us-ascii?q?BAQEBAQEBAQEBAxwLCgUqJAuCMyKCbQSBDiECEUIMij8ErROBbDqLfw+Ta4JhB?= =?us-ascii?q?YlSEog6jEOHMowiDWyBco8wlQo2gStRJluEPQEKAQEBQR2BaHSJWQEBAQ?= X-IronPort-AV: E=Sophos;i="5.39,364,1493676000"; d="asc'?scan'208";a="279769022" Received: from mailler06.lws-hosting.com ([31.207.32.247]) by mail2-smtp-roc.national.inria.fr with ESMTP; 20 Jun 2017 11:36:44 +0200 Received: from mailler06.lws-hosting.com (localhost.localdomain [127.0.0.1]) by filter3.lws (Postfix) with ESMTP id DF4CD3AE2B35 for ; Tue, 20 Jun 2017 11:36:42 +0200 (CEST) Received: from mailler06.lws-hosting.com (localhost.localdomain [127.0.0.1]) by filter2.lws (Postfix) with ESMTP id C9BA53AE2A46 for ; Tue, 20 Jun 2017 11:36:42 +0200 (CEST) Received: from mailler06.lws-hosting.com (localhost.localdomain [127.0.0.1]) by filter1.lws (Postfix) with ESMTP id BE6A53AE58E8 for ; Tue, 20 Jun 2017 11:36:41 +0200 (CEST) X-Spam-Checker-Version: SpamAssassin 3.3.1 (2010-03-16) on mailler06.lws-hosting.com X-Spam-Level: **** X-Spam-Virus: No Received: from raffalli.eu (vps29067.lws-hosting.com [192.162.68.177]) by mailler06.lws-hosting.com (Postfix) with ESMTP id BBB713AE33AC for ; Tue, 20 Jun 2017 11:36:41 +0200 (CEST) Received: from localhost (nat-maths.univ-savoie.fr [193.48.123.14]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by raffalli.eu (Postfix) with ESMTPSA id 8A7FE3520759 for ; Tue, 20 Jun 2017 11:36:41 +0200 (CEST) Date: Tue, 20 Jun 2017 11:36:41 +0200 From: Christophe Raffalli To: "caml-list@inria.fr" Message-ID: <20170620093641.ovz6dnsghtdj6tv6@delli7.univ-savoie.fr> MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha256; protocol="application/pgp-signature"; boundary="lntqewxulkn3a4cx" Content-Disposition: inline User-Agent: NeoMutt/20170306 (1.8.0) X-Validation-by: christophe@raffalli.eu Subject: [Caml-list] module equality --lntqewxulkn3a4cx Content-Type: text/plain; charset=utf-8 Content-Disposition: inline Dear camelers, I thought that two applications of Set.Make to the same module would result in two distinct modules with two distinct types 't'. This is not the case, and I am no sure it is a good choice as it allows to write the following, where you can break the invariant of a functor: ------------------------------------------------------------------------- let is_prime n = let rec fn d = if d * d > n then true else if n mod d = 0 then false else fn (d+1) in fn 2 let rec random_prime n = let p = 2 + Random.int (n-2) in if is_prime p then p else random_prime n module type S = sig type elt type t val create : elt list -> t end module F(O:Set.OrderedType) : S with type elt = O.t = struct type elt = O.t type t = O.t list let salt = random_prime 1_000_000 let _ = Printf.printf "salf: %d\n%!" salt let f x = Hashtbl.hash (Hashtbl.hash x * salt) let cmp x y = match compare (f x) (f y) with | 0 -> compare x y | c -> c let create l = List.sort cmp l end module Int = struct type t = int let compare = compare end module M1 = F(Int) module M2 = F(Int) let _ = Printf.printf "test: %b\n%!" (M1.create [1;2;3;4;5] = M2.create [1;2;3;4;5]) ---------------------------------------------------------------------------- OK, I know how to rewrite this functor so that M1.t and M2.t are distinct. But still the above code should be rejected, shouldn't it ? Cheers, Christophe --lntqewxulkn3a4cx Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQEzBAABCAAdFiEEJ369adg37nCCF0BCVXIaPfvmsfAFAllI7KYACgkQVXIaPfvm sfBKuwgAtwFjTb/zzX1uusud7Dgl2ehWSMrU6UXcaIv9A7XE3ltv1r0z7AqshmRb BWTTK4hNVwMsPCzT0w/a2tH7bBlkKw3ZllLBRWk9iVWIFLBr2eUwwk5QhPsIEjlo 5+zBsUqmMVN27Kpxaq7xx4Qh7OVqx3r6uAN3c/Bksl9PIDQL5iZ5FwO+wYOUDmc3 eCpphMQzQy8+cCIvwKR0jUPriyQATVaAXRUW4dSPeJs4lX7lZYMF2/uexkfhKkBI JUQ7kIdKw3bAcXKO9YQsQ0/Q/uRpWYIsjLdN3Ouhw4Fd9TCRH4D0m0ElRY0xjclx Er3RURhWUx7ASYuWMp8FwkwzVrLyag== =P//M -----END PGP SIGNATURE----- --lntqewxulkn3a4cx--