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 D8AF37EF10 for ; Wed, 25 Feb 2015 10:49:36 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.213.172; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.213.172 as permitted sender) identity=mailfrom; client-ip=209.85.213.172; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; 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@mail-ig0-f172.google.com) identity=helo; client-ip=209.85.213.172; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-ig0-f172.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0C9AQAcmu1Um6zVVdFBGhaDQFoEgwSwQI1ygWQBCYVwAoEYB0MBAQEBAQEQAQEBAQEGCwsJFC6EDwEBAQIBAQECDxEdARsPAwsBAwELBgULAwoNHQICIgERAQUBChIGExIIAQeHeAEDCQgNN65LPjGLLoFrgneORQoZJwMKVIRdAQEBAQEFAQEBAQEBAQEUAQUOiwWEagQHgi07EoExBYRfCo5ShWWBVJAdEiOBDAmEET0xAQGCQQEBAQ X-IPAS-Result: A0C9AQAcmu1Um6zVVdFBGhaDQFoEgwSwQI1ygWQBCYVwAoEYB0MBAQEBAQEQAQEBAQEGCwsJFC6EDwEBAQIBAQECDxEdARsPAwsBAwELBgULAwoNHQICIgERAQUBChIGExIIAQeHeAEDCQgNN65LPjGLLoFrgneORQoZJwMKVIRdAQEBAQEFAQEBAQEBAQEUAQUOiwWEagQHgi07EoExBYRfCo5ShWWBVJAdEiOBDAmEET0xAQGCQQEBAQ X-IronPort-AV: E=Sophos;i="5.09,643,1418079600"; d="scan'208";a="123303587" Received: from mail-ig0-f172.google.com ([209.85.213.172]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 25 Feb 2015 10:49:35 +0100 Received: by mail-ig0-f172.google.com with SMTP id l13so34037131iga.5 for ; Wed, 25 Feb 2015 01:49:34 -0800 (PST) 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=Z/rTez635jI1d5+qbMk28n8OkOE3KBJ1PY4rYV8kgTk=; b=wCATzbP2oIlEcbgA7qX3lDn8Hvmt5K/odLfbVrNk1PrLBqECf7GpyOfTf1JY8Alp5s owulBOpnFQUwC7yyHO7igY/QheoaD3FGA8MnuAE0M8AOZau4NicAy0Vbs5AiQTKjLXAA 5c7mvZCAeRPX7bMbaxmN/CXlIu7T4FMrvnalwKkYVGDf8F8bftDuX85N2DuktU1EmrOO iApeRpccr9sWxwaAD3xcdU+j1qCAcIoEr5SEhQQGy0gXC+qnVHX4XSUT0m0511ymVMaA DczX9Iaix1pkKL2mNjtd/i58bKOieNedFm55zNk/a99NTPPTIbM2I3V4KLFOCr88iScR HF8w== X-Received: by 10.107.8.213 with SMTP id h82mr3139122ioi.89.1424857774703; Wed, 25 Feb 2015 01:49:34 -0800 (PST) MIME-Version: 1.0 Received: by 10.36.13.16 with HTTP; Wed, 25 Feb 2015 01:48:54 -0800 (PST) In-Reply-To: References: <000401d05056$ed605f70$c8211e50$@metastack.com> <87wq372noc.fsf@study.localdomain> <87k2z72ewr.fsf@study.localdomain> From: Gabriel Scherer Date: Wed, 25 Feb 2015 10:48:54 +0100 Message-ID: To: David Allsopp Cc: Leo White , Ben Millwood , Jeremy Yallop , OCaml List Content-Type: multipart/alternative; boundary=001a113f9934844aba050fe68d21 Subject: Re: [Caml-list] Match error with abstract types in modules --001a113f9934844aba050fe68d21 Content-Type: text/plain; charset=UTF-8 > > is there (in theory) a relatively easy kind of annotation which could be > added to type 'a t in a signature which would tell the compiler that 'a t > and 'b are equal and compatible iff 'a and 'b are equal/compatible but > still remain abstract? Yes, this is exactly the point of "injectivity" which has been discussed at length in http://caml.inria.fr/mantis/view.php?id=5985 and summarized in a (rather difficult to follow for the non-expert) talk by Jacques Garrigue at the OCaml Meeting 2013 in Boston, abstract: http://www.math.nagoya-u.ac.jp/~garrigue/papers/injectivity.pdf slides: https://ocaml.org/meetings/ocaml/2013/slides/garrigue.pdf It would not be difficult to teach the type-checker about injectivity, but there is no concrete syntax in the language to discuss it, and it is not easy to design a good one (which is why it has not been added yet). The difficult question is whether users should add an extra mark to explicitly require injectivity (like we do for covariance for example), or whether it should be assumed when using the default (type 'a t) notation, with an explicit mark to allow *non*-injectivity. On Wed, Feb 25, 2015 at 9:41 AM, David Allsopp wrote: > Leo White wrote: > > Ben Millwood writes: > > > > > I think the issue would be substantially mitigated were it not for the > > > simple fact that [type 'a t] in a signature means "abstract type", > > > whereas [type 'a t] in a structure means "empty type". The fact that > > > there is no syntactic distinction, and indeed *no way to make one* > > > caused me a great deal of confusion some time ago when I had a problem > > > similar to David's. > > The context of my original problem was the initially confusing assertion > by the compiler that two "different" BatSet.t uses were the same. I guessed > that what I was seeing was part of the "easy to shoot yourself in the foot" > comment in its documentation! > > > You can make an empty type (or at least a type for which there are no > > expressions) using: > > > > type 'a t = private T > > The obvious "solution" with sets is to use the functor version therefore > and have a module for each point (I believe that's 50% of the reason for > doing it - the other being that you don't need to store the comparison > function in the value itself), but is there (in theory) a relatively easy > kind of annotation which could be added to type 'a t in a signature which > would tell the compiler that 'a t and 'b are equal and compatible iff 'a > and 'b are equal/compatible but still remain abstract? > > > David > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > --001a113f9934844aba050fe68d21 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
is there= (in theory) a relatively easy kind of annotation which could be added to type 'a t in a signature which would tell the compiler that &= #39;a t and 'b are equal and compatible iff 'a and 'b are equal/comp= atible=20 but still remain abstract?

Yes, this is exa= ctly the point of "injectivity" which has been discussed at lengt= h in
=C2=A0 = http://caml.inria.fr/mantis/view.php?id=3D5985
and summar= ized in a (rather difficult to follow for the non-expert) talk by Jacques G= arrigue at the OCaml Meeting 2013 in Boston,
=C2=A0 abstract: http://ww= w.math.nagoya-u.ac.jp/~garrigue/papers/injectivity.pdf
=C2=A0 slides= : htt= ps://ocaml.org/meetings/ocaml/2013/slides/garrigue.pdf

It would not be difficult to teach the type-checker about injectivity, bu= t there is no concrete syntax in the language to discuss it, and it is not = easy to design a good one (which is why it has not been added yet). The dif= ficult question is whether users should add an extra mark to explicitly req= uire injectivity (like we do for covariance for example), or whether it sho= uld be assumed when using the default (type 'a t) notation, with an exp= licit mark to allow *non*-injectivity.

On Wed, Feb 25, 2015 at 9:41 AM, David= Allsopp <dra-news@metastack.com> wrote:
Leo White wrote:
> Ben Millwood <bmillwood= @janestreet.com> writes:
>
> > I think the issue would be substantially mitigated were it not fo= r the
> > simple fact that [type 'a t] in a signature means "abstr= act type",
> > whereas [type 'a t] in a structure means "empty type&quo= t;. The fact that
> > there is no syntactic distinction, and indeed *no way to make one= *
> > caused me a great deal of confusion some time ago when I had a pr= oblem
> > similar to David's.

The context of my original problem was the initially confusing asser= tion by the compiler that two "different" BatSet.t uses were the = same. I guessed that what I was seeing was part of the "easy to shoot = yourself in the foot" comment in its documentation!

> You can make an empty type (or at least a type for which there are no<= br> > expressions) using:
>
> type 'a t =3D private T

The obvious "solution" with sets is to use the functor ver= sion therefore and have a module for each point (I believe that's 50% o= f the reason for doing it - the other being that you don't need to stor= e the comparison function in the value itself), but is there (in theory) a = relatively easy kind of annotation which could be added to type 'a t in= a signature which would tell the compiler that 'a t and 'b are equ= al and compatible iff 'a and 'b are equal/compatible but still rema= in abstract?


David

--
Caml-list mailing list.=C2=A0 Subscription management and archives:
ht= tps://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
--001a113f9934844aba050fe68d21--