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 4DA4880161 for ; Tue, 20 Jun 2017 12:05:47 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=yallop@gmail.com; spf=Pass smtp.mailfrom=yallop@gmail.com; spf=None smtp.helo=postmaster@mail-io0-f177.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of yallop@gmail.com) identity=pra; client-ip=209.85.223.177; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="yallop@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of yallop@gmail.com designates 209.85.223.177 as permitted sender) identity=mailfrom; client-ip=209.85.223.177; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="yallop@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-io0-f177.google.com) identity=helo; client-ip=209.85.223.177; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="postmaster@mail-io0-f177.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3At6uP9BeEC1r0BCLRIHLHMyuNlGMj4u6mDksu8pMi?= =?us-ascii?q?zoh2WeGdxcu/ZB7h7PlgxGXEQZ/co6odzbGH7Oa4ASQp2tWoiDg6aptCVhsI24?= =?us-ascii?q?09vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7?= =?us-ascii?q?Ovr6GpLIj8Swyuu+54Dfbx9GiTe5Y75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYe?= =?us-ascii?q?RWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZ?= =?us-ascii?q?TAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v9LlgRgP2hy?= =?us-ascii?q?gbNj456GDXhdJ2jKJHuxKquhhzz5fJbI2JKPZye6XQds4YS2VcRMZcTy5OAo28?= =?us-ascii?q?YYUBDOQPIPhWoJXmqlsSsRezHxWgCP/zxjJKgHL9wK000/4mEQHDxAEuG8wBsG?= =?us-ascii?q?7Ko9XwNKYZTOK6w7PMzTXHaPNWwSr25Y/Icx87pfGMWbVwcdLKxEkgEgPKlFSQ?= =?us-ascii?q?qYj/MzyJ0eQNtnGW4ux9Xuysk24qsx99riSry8s2iYTEhpgZxk7a+Sh32oo5ON?= =?us-ascii?q?+1RUx9bNW5CpVfrTuaOJFzQs46Q2FnpiI6yroetJ6+ZicKyZAnywfea/yAb4SE?= =?us-ascii?q?+xzjWPuTLDp6nn5ld7W/hxG98Uik1OLwTNW70FFPriZdk9nMsG4C1wDL58SZVv?= =?us-ascii?q?dw+l2t1DWP2gzJ9O1IP045mbDGJ5MjwLM8jp8Tvl7CHi/ylkX2lqiWdkA89+mo?= =?us-ascii?q?8evnZrHmppiEN4JvhQH+N74hms27AegiLgcOWG2b9fym1LL/5U35XKlKjvoun6?= =?us-ascii?q?bFqp/aIMAbqre9Aw9UyYYj9w2yDyym0dQdhXkINkhJeBOBj4jzOlHBOur0Dfml?= =?us-ascii?q?gwfkrDA+7PDcP6b9BY3NIzD5mbnvdLJ56gYIwwopzMtD4IpUB5kbKfz9U0v1tZ?= =?us-ascii?q?rVE0lqHRazxrPFBc9w05JWaGuLBqiBePfDuFuM4foHLOyFZYtTszH4fat2r8Xy?= =?us-ascii?q?hGM0zAdONZKi2oEaPTXhRqxr?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CBAgB08khZhrHfVdFcHQEFAQsBGAEFA?= =?us-ascii?q?QsBhRwHg2ScF4kbjm6GJAKCVQdCFQEBAQEBAQEBAQEBEgEBAQgLCwgoL4IzJAG?= =?us-ascii?q?CQAEBAQECASMEGQEbHQEDAQsGBQsNAgImAgIiAREBBQEcBhMIigsBAw0IoE0/j?= =?us-ascii?q?AiBbBgFARyDCQWDYQoZJw1Wg0ABAQEBAQUBAQEBARsCBhJ5imWHe4JhBYlkiDq?= =?us-ascii?q?MQ5Nhkg6TQhQfgRU1gSwwIQgbFUkZhGUfgXM/NolZAQEB?= X-IPAS-Result: =?us-ascii?q?A0CBAgB08khZhrHfVdFcHQEFAQsBGAEFAQsBhRwHg2ScF4k?= =?us-ascii?q?bjm6GJAKCVQdCFQEBAQEBAQEBAQEBEgEBAQgLCwgoL4IzJAGCQAEBAQECASMEG?= =?us-ascii?q?QEbHQEDAQsGBQsNAgImAgIiAREBBQEcBhMIigsBAw0IoE0/jAiBbBgFARyDCQW?= =?us-ascii?q?DYQoZJw1Wg0ABAQEBAQUBAQEBARsCBhJ5imWHe4JhBYlkiDqMQ5Nhkg6TQhQfg?= =?us-ascii?q?RU1gSwwIQgbFUkZhGUfgXM/NolZAQEB?= X-IronPort-AV: E=Sophos;i="5.39,364,1493676000"; d="scan'208";a="228993211" Received: from mail-io0-f177.google.com ([209.85.223.177]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 20 Jun 2017 12:05:46 +0200 Received: by mail-io0-f177.google.com with SMTP id t87so81253175ioe.0 for ; Tue, 20 Jun 2017 03:05:46 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=MlWY7hG+8ga2uiEI+UzgtYcIIG3lK8QCBMgCQJNwvu4=; b=kEN9URa567XCuNWnOMwPfJQ9zU/SxzJ1NrLQhExm+AzLiER3aiEg5UfxltaJJcUUeM SYAWbCM5/8oFmjktkLV5++R0yR00BTBme67qeerXSZPoNdBQ/jDZekn7kiVTf99VlyS7 yYpaI/3gzCeQL0/PZlvxDxsGPWpZhWzUt+XmITJr2zCX4czuGR23D+1uSyRz/O64Ddqj 8MwLJT/7HuK8q2VPRqztcEHdcl2uL7+KT3JTAaQkVYCx72UM6BlwOT7qlITfC97Mx1/D UO11l+NFRm96Pl8vDGgVxhlXbWJsdw2wMC19hCtbZbcnk9EYNRbJ4nQBwlYsrk/RTAML 6TKQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=MlWY7hG+8ga2uiEI+UzgtYcIIG3lK8QCBMgCQJNwvu4=; b=du5XIcXProZsgVzEHw6FYG3w0ZF0457rVKENyhRCr9QC7K49pH05Q6uTbdr6gwTIOT MX23/Elc68ZlTgzcShPumDtNpLMS2DW/suPV+3TDKVrHBC+gWCH7U1IluFBtEkEPNex8 xk3DSi+KsW3QcUPchwooy2hRSBeLEpHEmZD+rd8TXtjgTCthc7NlN/S+5xrJr7+U4VBn 5dlvzWJGkDN3p4v7FYN4hVnPI7tcb8dEcfDN5dTLLCWFJp5fx+e28bpl+a3iAx2f1W7b CMpLVAO9ztSs0O5eXuVBKESgodquanlEafiIEJbIkJJcMYYdQUqHR/YopVhAkEp7CH/s Cytw== X-Gm-Message-State: AKS2vOzLaq4IbzKMVlRhJdhQxWHMJAwZJahUVrQqODrxvORL9NgY+PUd x6+h6PdZ5317WKHOmpCEtRQ/ghccjZ2K X-Received: by 10.107.6.7 with SMTP id 7mr28816477iog.122.1497953144821; Tue, 20 Jun 2017 03:05:44 -0700 (PDT) MIME-Version: 1.0 Received: by 10.79.124.84 with HTTP; Tue, 20 Jun 2017 03:05:44 -0700 (PDT) In-Reply-To: <20170620093641.ovz6dnsghtdj6tv6@delli7.univ-savoie.fr> References: <20170620093641.ovz6dnsghtdj6tv6@delli7.univ-savoie.fr> From: Jeremy Yallop Date: Tue, 20 Jun 2017 11:05:44 +0100 Message-ID: To: Christophe Raffalli Cc: "caml-list@inria.fr" Content-Type: text/plain; charset="UTF-8" Subject: Re: [Caml-list] module equality Dear Christophe, On 20 June 2017 at 10:36, Christophe Raffalli wrote: > 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 Right: in OCaml, two applications of a functor to the same module path have signatures with equal type components. This type of functor is called "applicative", as opposed to the "generative" functors found in Standard ML. Generative functors have the behaviour you were expecting, with each application generating fresh type components. However, applicative functors allow many programs to be given types that are rejected when functors are generative. (There are a few examples nowadays of programs that can be given types with generative, but not applicative, functors, but they're fairly obscure.) In your example: > module F(O:Set.OrderedType) : S with type elt = O.t = struct [...] > module M1 = F(Int) > module M2 = F(Int) the two applications of F both have the signature sig ... type t = F(Int).t ... end i.e. both M1.t and M2.t are equal to the type F(Int).t, and so values of those types can be mixed freely. However, although the types resulting from the functor applications are shared, the values resulting from the application (i.e. M1 and M2) are not equivalent. People occasionally find this combination -- sharing of types without sharing of values -- surprising, since types are often used to determine whether values are compatible in terms of both representation and behaviour. There are a couple of ways to ensure that applications of F to the same module build modules with incompatible types. First, the applicative behaviour only holds for paths, so you can force incompatibility at the call site by passing a module expression that is not a path as an argument: module M1 = F(struct include Int end) module M2 = F(struct include Int end) # fun (x : M1.t) -> (x : M2.t);; Characters 19-20: fun (x : M1.t) -> (x : M2.t);; ^ Error: This expression has type M1.t but an expression was expected of type M2.t Alternatively, you can mark the functor as generative at the definition site by adding an additional parameter '()': module F(O:Set.OrderedType) () : S with type elt = O.t = struct ... which requires each caller of F to provide a corresponding argument module M1 = F(Int) () module M2 = F(Int) () and once again generates modules whose signatures have distinct type components. Since the surprising behaviour only arises when functor applications have effects, Andreas Rossberg has advocated connecting the applicative/generative distinction with the purity/effectful distinction, making pure functors applicative and effectful functors generative. OCaml doesn't enforce this behaviour, but it's a reasonably pattern to follow when writing programs. Kind regards, Jeremy