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 0A1AB81799 for ; Sat, 27 Jul 2013 22:08:24 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of philippe.veber@gmail.com) identity=pra; client-ip=74.125.82.49; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="philippe.veber@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of philippe.veber@gmail.com designates 74.125.82.49 as permitted sender) identity=mailfrom; client-ip=74.125.82.49; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="philippe.veber@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-wg0-f49.google.com) identity=helo; client-ip=74.125.82.49; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="postmaster@mail-wg0-f49.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AukBAHAo9FFKfVIxjWdsb2JhbABbDoN9vVaBEggWDgEBAQEHCwsJEgYkgiQBAQQBQAEbHQEDAQsGBQQHDS4hAQERAQUBHAYTh30BAwkGmxSMT4J/g3YKGScNZId0AQUMjQmCaAeEBQOVdoFpjCaDQRYpg3xAOg X-IPAS-Result: AukBAHAo9FFKfVIxjWdsb2JhbABbDoN9vVaBEggWDgEBAQEHCwsJEgYkgiQBAQQBQAEbHQEDAQsGBQQHDS4hAQERAQUBHAYTh30BAwkGmxSMT4J/g3YKGScNZId0AQUMjQmCaAeEBQOVdoFpjCaDQRYpg3xAOg X-IronPort-AV: E=Sophos;i="4.89,758,1367964000"; d="scan'208";a="22477336" Received: from mail-wg0-f49.google.com ([74.125.82.49]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 27 Jul 2013 22:08:13 +0200 Received: by mail-wg0-f49.google.com with SMTP id y10so3213644wgg.16 for ; Sat, 27 Jul 2013 13:08:13 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=WbPJ5pRz9MJWZTDWpMmVpz/MxkJyY6FIXrHw//oPMso=; b=uoMHUNkrDz5DBhNKyeiA3m04huhdhKbw+LGyUFuI6EsvwNeybc+4RUWZp6xqXBj/eB tMvYEh6kVh17DrggKtYozdoQkm2pG6O6p+gBiIPQiMWZMqUAH+zCuiMskESvHor9XDSE yQLc12SG4Mz9RUp/frV/wBDwEifzTSNAT1o8HI60j/KRix8rUet4Ov40RLaE+hk5WhKV IANmoruqFKV4HjlBrqW9zxVXh0KnxndP4abowQjHCQAIaqNmDf0cIXsBEZl9nqTXs8jh SKcsRN0c9dVPmGWIjS+tY3mUPGQ++qfN6cmqZqNbK9ggIXkds68qpK4vUalbLc7CC2FE H/lw== X-Received: by 10.194.8.99 with SMTP id q3mr1995158wja.91.1374955693280; Sat, 27 Jul 2013 13:08:13 -0700 (PDT) MIME-Version: 1.0 Received: by 10.194.41.138 with HTTP; Sat, 27 Jul 2013 13:07:53 -0700 (PDT) In-Reply-To: <059C2901-8AFE-4E28-B1D2-BC1D660CCA3A@math.nagoya-u.ac.jp> References: <059C2901-8AFE-4E28-B1D2-BC1D660CCA3A@math.nagoya-u.ac.jp> From: Philippe Veber Date: Sat, 27 Jul 2013 22:07:53 +0200 Message-ID: To: Jacques Garrigue Cc: caml users Content-Type: multipart/alternative; boundary=047d7b5d6592ae156e04e283d1e0 X-Validation-by: philippe.veber@gmail.com Subject: Re: [Caml-list] Narrowing a signature with a constrained type --047d7b5d6592ae156e04e283d1e0 Content-Type: text/plain; charset=ISO-8859-1 Thanks for the explanation Jacques! To be honest I was expecting the difficulty to lie in comparing two constrained definitions (in my example, that would mean that type 'a format would already be constrained and I'd be trying to narrow it further with another constrained type). I thought the particular case where the original type is unconstrained would be easier, but yeah, this is certainly more difficult than it looks! ph. 2013/7/27 Jacques Garrigue > On 2013/07/26, at 22:32, Philippe Veber wrote: > > > Dear camlers, > > > > Out of curiosity, I'd be happy to understand why the following > definition is rejected: > > > > # module type T = sig type 'a format end;; > > module type T = sig type 'a format end > > # module F(X : T with type 'a format = 'a list constraint 'a = < .. >) = > struct end;; > > File "", line 1, characters 13-67: > Error: In this `with' > constraint, the new definition of format does not match its original > definition in the constrained signature: > > Type declarations do not match: type 'a format = 'a0 list is not > included in type 'a format > > Their constraints differ. > > > > Would it be unsound to allow it? > > Well, to ensure the coherence of the with constraints, we require that > the new signature be a subtype of the original one (as a module, not as an > object). > This is where your code gets rejected. > > Now why is it deemed unsafe to allow a constrained type definition to be a > subtype of > an unconstrained one? > Actually, I don't know. > The unconstrained type does not enforce the invariants of the constrained > one, > but they will be checked as soon as you try to unify the two. > So it may be possible to lift this restriction. > > However, there are technical difficulties in comparing a constrained > definition > with an unconstrained one, so this might just be the main reason. > This would also have an impact on the invariants of types through > abstraction. > > Jacques --047d7b5d6592ae156e04e283d1e0 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
Thanks for the explanation Jacques!

To be honest I = was expecting the difficulty to lie in comparing two constrained definition= s (in my example, that would mean that type 'a format would already be = constrained and I'd be trying to narrow it further with another constra= ined type). I thought the particular case where the original type is uncons= trained would be easier, but yeah, this is certainly more difficult than it= looks!

ph.


2013/7/27 Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
On 2= 013/07/26, at 22:32, Philippe Veber <philippe.veber@gmail.com> wrote:

> Dear camlers,
>
> Out of curiosity, I'd be happy to understand why the following def= inition is rejected:
>
> # module type T =3D sig type 'a format end;;
> module type T =3D sig type 'a format end
> # module F(X : T with type 'a format =3D 'a list constraint &#= 39;a =3D < .. >) =3D struct end;;
> File "", line 1, characters 13-67: =A0 =A0 =A0 =A0 =A0 =A0 = =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0= =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 = =A0 =A0 Error: In this `with' constraint, the new definition of format = does not match its original definition in the constrained signature:
> Type declarations do not match: type 'a format =3D 'a0 list is= not included in type 'a format
> =A0 =A0 =A0 =A0Their constraints differ.
>
> Would it be unsound to allow it?

Well, to ensure the coherence of the with constraints, we requi= re that
the new signature be a subtype of the original one (as a module, not as an = object).
This is where your code gets rejected.

Now why is it deemed unsafe to allow a constrained type definition to be a = subtype of
an unconstrained one?
Actually, I don't know.
The unconstrained type does not enforce the invariants of the constrained o= ne,
but they will be checked as soon as you try to unify the two.
So it may be possible to lift this restriction.

However, there are technical difficulties in comparing a constrained defini= tion
with an unconstrained one, so this might just be the main reason.
This would also have an impact on the invariants of types through abstracti= on.

Jacques

--047d7b5d6592ae156e04e283d1e0--