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 4B3087F784 for ; Wed, 25 Feb 2015 09:41:42 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of dra-news@metastack.com) identity=pra; client-ip=62.13.148.101; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="dra-news@metastack.com"; x-sender="dra-news@metastack.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of dra-news@metastack.com designates 62.13.148.101 as permitted sender) identity=mailfrom; client-ip=62.13.148.101; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="dra-news@metastack.com"; x-sender="dra-news@metastack.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@outmail148101.authsmtp.com) identity=helo; client-ip=62.13.148.101; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="dra-news@metastack.com"; x-sender="postmaster@outmail148101.authsmtp.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0BnAQBliu1UnGWUDT5bDoJUdFoEsEkGkkyFeAKBI0MBAQEBAQEQAQEBAQEIFAlChA8BAQEDAQMkEz8FCwIBCA4KChQQMiUCBA4NiB8JA9RTAQEBAQYBAQEBAQEBG4YHhQyEPTEHgxeBFAWTO4VlAYEajmKDPoNTPW+BRH8BAQE X-IPAS-Result: A0BnAQBliu1UnGWUDT5bDoJUdFoEsEkGkkyFeAKBI0MBAQEBAQEQAQEBAQEIFAlChA8BAQEDAQMkEz8FCwIBCA4KChQQMiUCBA4NiB8JA9RTAQEBAQYBAQEBAQEBG4YHhQyEPTEHgxeBFAWTO4VlAYEajmKDPoNTPW+BRH8BAQE X-IronPort-AV: E=Sophos;i="5.09,643,1418079600"; d="scan'208";a="101240382" Received: from outmail148101.authsmtp.com ([62.13.148.101]) by mail3-smtp-sop.national.inria.fr with ESMTP; 25 Feb 2015 09:41:41 +0100 Received: from mail-c235.authsmtp.com (mail-c235.authsmtp.com [62.13.128.235]) by punt18.authsmtp.com (8.14.2/8.14.2/) with ESMTP id t1P8feYY076690; Wed, 25 Feb 2015 08:41:40 GMT Received: from romulus.metastack.com (cpc1-cmbg5-0-0-cust241.5-4.cable.virginm.net [81.98.252.242]) (authenticated bits=0) by mail.authsmtp.com (8.14.2/8.14.2/) with ESMTP id t1P8faS6057055; Wed, 25 Feb 2015 08:41:36 GMT Received: from remus.metastack.local (remus.metastack.com [172.16.0.1]) by romulus.metastack.com (8.14.2/8.14.2) with ESMTP id t1P8fYpl027493 (version=TLSv1/SSLv3 cipher=AES128-SHA bits=128 verify=FAIL); Wed, 25 Feb 2015 08:41:35 GMT Received: from Remus.metastack.local ([fe80::547c:3c42:e1da:eda2]) by Remus.metastack.local ([fe80::547c:3c42:e1da:eda2%10]) with mapi id 14.03.0224.002; Wed, 25 Feb 2015 08:41:35 +0000 From: David Allsopp To: Leo White CC: OCaml List Thread-Topic: [Caml-list] Match error with abstract types in modules Thread-Index: AQHQUGW3HoJ7Sr46RUmuhYPLJuzpG50BB1qw Date: Wed, 25 Feb 2015 08:41:34 +0000 Message-ID: References: <000401d05056$ed605f70$c8211e50$@metastack.com> <87wq372noc.fsf@study.localdomain> <87sidv2kgj.fsf@study.localdomain> In-Reply-To: <87sidv2kgj.fsf@study.localdomain> Accept-Language: en-GB, en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [172.16.0.18] Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 Organization: MetaStack Solutions Ltd. X-Scanned-By: MIMEDefang 2.65 on 172.16.0.20 X-Server-Quench: 1c01a3e5-bcca-11e4-b396-002590a15da7 X-AuthReport-Spam: If SPAM / abuse - report it at: http://www.authsmtp.com/abuse X-AuthRoute: OCd1ZAARAlZZVg1f DC4bFwdFRBksPQFF ChxFJgxfNl8UURhQ KkJXbgASJgdBAn9U UXkJW1VRQF15U2d0 YQlXIw1cfENGQQdv UlZLRlBNFgB3AVJF B34WBEgRcQVDf351 YAhjXnBcXAp7JkZ8 E00BEHBUNjQxdWEe BURFJQBddh5Kfh1A Y1AuVXZZMGJJBA9q VzwYNjU1eDFeMzhg CiQEMVkSCUsRBDkm Dw8DATVnFEceWz86 JABuNk8EEV1ZM0N6 NFwtRFYVKHc8 X-Authentic-SMTP: 61633634383431.1023:706 X-AuthFastPath: 0 (Was 255) X-AuthSMTP-Origin: 81.98.252.242/25 X-AuthVirus-Status: No virus detected - but ensure you scan with your own anti-virus system. Subject: RE: [Caml-list] Match error with abstract types in modules Leo White wrote: > >> so that `int foo` is equal to `float foo`, then your match isn't > >> really exhaustive. > > > > How so? >=20 > Both constructors would then have the same type. Since it is possible they > both have the same type, you need to match on both of them. >=20 > > What's (very) confusing to me is that it seems to permit nonsensical > > matches without warning. In both the unconstrained and constrained > > versions of Foo, the resulting type of the function [foo] is [int > > Foo.foo t -> unit] so [foo B] is always rejected. But you get no > > warning about an unusable match case with: > > > > let foo =3D function A -> () | B -> () > > >=20 > This is because `foo B` may not always be rejected. Consider the following > code: >=20 > module F (Foo : sig type 'a foo end) =3D struct >=20 > type _ t =3D A : int Foo.foo t > | B : float Foo.foo t >=20 > let foo =3D function > | A -> () > | B -> () >=20 > (* [foo B] would be an error here *) >=20 > end >=20 > module M =3D F(struct type 'a foo =3D unit end) >=20 > (* But out here it is fine *) > let () =3D M.foo M.B >=20 > > although > > > > let foo =3D function A | B -> () > > > > unsurprisingly does not type. >=20 > That's due to GADTs not currently being compatible with or-patterns, it is > not related to the injectivity issues you are having. >=20 > >> In the second version, the compiler cheats. Since `bar` is definied > >> in the same module, it knows that the abstract `bar` type it can see > >> is actually the definition, not just an abstraction of a type defined > >> elsewhere, so it knows that `int bar` cannot equal `float bar`. > >> > >> Personally, I dislike this behaviour and would prefer both cases to > >> give an error. > > > > What's to dislike? >=20 > Giving different behviour based on whether something is defined in the > same module is anti-modular, and confuses people when they try to split > their code across different modules. >=20 > > It's rather useful - the constructors of a GADT are partionable by > > type. >=20 > That is indeed useful, but only really works in OCaml if you expose the > definitions of these types, so that OCaml can see that they are definitely > not the same type. This is why you see people use: >=20 > type z =3D Z >=20 > type 'a s =3D S It turns out that this very helpful explanation has inadvertently answered = an issue I had a while ago where I'd ended up leaving a comment in my code = that I didn't fully understand why I needed type t =3D T, type s =3D S for = doing this! > when doing type-level arithmetic. By giving types with incompatible > definitions, rather than abstract types, OCaml can safely conclude they > are not the same type. >=20 > > What caught me out was that two constructors with distinct types (in > > my actual use with different instantiations of 'a > > BatSet.t) were being regarded as equal in terms of pattern matching. > > I'd be quite happy if a type annotation were necessary to make it > > explicit that I meant to do it: > > > > let foo (key : int Foo.foo t) =3D > > match key with A -> () > > > > Especially with that explicit type, I find it very odd to get a > > warning about a constructor whose type is not permitted in this > > context and so cannot be matched. >=20 > The problem is that OCaml has no way to know that `int Foo.foo` is not > equal to `float Foo.foo` so it must insist that you include a case for it. > OCaml also doesn't know that `int Foo.foo` does equal `float Foo.foo` so > it can't let you call `foo Foo.B` either. Ah, I see - thanks! David