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 D57947F7B4 for ; Fri, 14 Feb 2014 10:09:14 +0100 (CET) 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: AjwDALLc/VKFBoIFdGdsb2JhbABZgz6DWbwwgSwOAQwVCDyCJQEBBAEjBBwBNQIDCwsYAgImAgJXBogQB6V9doNnApYyh2UQB4EpjR0zB4JvNYEUiUqKfYNphkePGA X-IPAS-Result: AjwDALLc/VKFBoIFdGdsb2JhbABZgz6DWbwwgSwOAQwVCDyCJQEBBAEjBBwBNQIDCwsYAgImAgJXBogQB6V9doNnApYyh2UQB4EpjR0zB4JvNYEUiUqKfYNphkePGA X-IronPort-AV: E=Sophos;i="4.95,843,1384297200"; d="scan'208";a="49054935" 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; 14 Feb 2014 10:09:11 +0100 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 9C0A363FB; Fri, 14 Feb 2014 18:09:08 +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 0E2244126; Fri, 14 Feb 2014 18:09:08 +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 [192.168.43.31] (om126193000085.1.kyb.openmobile.ne.jp [126.193.0.85]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id A949E410B; Fri, 14 Feb 2014 18:09:02 +0900 (JST) Mime-Version: 1.0 (Mac OS X Mail 7.1 \(1827\)) Content-Type: text/plain; charset=utf-8 From: Jacques Garrigue In-Reply-To: <52FDDA89.5070303@frisch.fr> Date: Fri, 14 Feb 2014 18:08:55 +0900 Cc: Christophe Troestler , OCaml Mailing List Content-Transfer-Encoding: quoted-printable Message-Id: References: <20140214.082352.48621319473754158.Christophe.Troestler@umons.ac.be> <52FDDA89.5070303@frisch.fr> To: Alain Frisch X-Mailer: Apple Mail (2.1827) Subject: Re: [Caml-list] First class modules aliases On 2014/02/14 17:57, Alain Frisch wrote: > Hi Christophe, >=20 > On 02/14/2014 08:23 AM, Christophe Troestler wrote: >> I have encoutered several annoyances with module aliasing in the >> context of first class modules. For example, if I declare >>=20 >> module type A =3D sig type t end >> type 'a a =3D (module A with type t =3D 'a) >> module type IA =3D A with type t =3D int >> type ia =3D (module IA) >>=20 >> then I expect the types =E2=80=9Cint a=E2=80=9D and =E2=80=9Cia=E2=80=9D= to be equivalent but this is >> not the case: >>=20 >> let f (a: int a) =3D (a : ia) >>=20 >> gives the error >>=20 >> This expression has type int a =3D (module A with type t =3D int) >> but an expression was expected of type ia =3D (module IA) >=20 > Indeed, two "package types" are equal (w.r.t. unification) if they have t= he same module type path (nominally, after expanding bare module type alias= es) and the same list of constraints (modulo reordering). In this case, mo= dule type paths are different (A and IA) and so are the lists of constraint= s (of respective length 1 and 0). >=20 > One could try to use a more relaxed definition of equality, based on actu= ally comparing module type expressions. At least for closed package types = (i.e. for (module A with t =3D int) but not (module A with t =3D 'a)), this= might be doable, although introducing a dependency between the unification= algorithm and the equality check for module types might cause unexpected p= roblems. Moscow ML uses this relaxed equality, and this does not seem to be a proble= m. However, this requires some care when handling free variables. >> Another example is: >>=20 >> module X =3D struct >> module type T =3D sig type s end >> type 'a t =3D (module T with type s =3D 'a) >> let id (x: int t) =3D x >> end >>=20 >> let f (x: int X.t) =3D x >>=20 >> module Y =3D struct >> include X >> let h x =3D f(id x) >> end >>=20 >> To make it work, I basically have to perform by hand the aliasing that >> =E2=80=9Cinclude X=E2=80=9D should make: >>=20 >> module Y : sig type 'a t val h : int t -> int t end =3D struct >> type 'a t =3D 'a X.t >> let h x =3D f(X.id x) >> end >=20 > Here the problem is that "include X" copies the definition of the module = type T, as if you had written: >=20 > module T =3D sig type s end >=20 > and thus it introduces a new module type path. Since package types use a= nominal equality between module type paths, (module T) and (module X.T) ar= e incompatible. One way to fix it would be to tweak the "strengthening" a= lgorithm which adds equalities to module types in order to turn a module ty= pe declaration to an alias to the original definition instead of copying it= .=20=20 This is already done in trunk. Jacques Garrigue=