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 090257EF10 for ; Tue, 24 Feb 2015 20:11:42 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=pra; client-ip=131.111.8.150; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=mailfrom; client-ip=131.111.8.150; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of postmaster@ppsw-50.csi.cam.ac.uk designates 131.111.8.150 as permitted sender) identity=helo; client-ip=131.111.8.150; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="postmaster@ppsw-50.csi.cam.ac.uk"; x-conformance=sidf_compatible; x-record-type="v=spf1" X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0BcAQDny+xUnJYIb4Nbg1hasEYGkkyFeAKBLEMBAQEBAQEQAQEBAQEGDQkJFC6EEAEEASdSBQsLDhMlDwEESYg6CATQCYRqAQEIAQEBAQEdhgeFDIRuB4QrBZM2hWWBG45egz6EEG+CQwEBAQ X-IPAS-Result: A0BcAQDny+xUnJYIb4Nbg1hasEYGkkyFeAKBLEMBAQEBAQEQAQEBAQEGDQkJFC6EEAEEASdSBQsLDhMlDwEESYg6CATQCYRqAQEIAQEBAQEdhgeFDIRuB4QrBZM2hWWBG45egz6EEG+CQwEBAQ X-IronPort-AV: E=Sophos;i="5.09,640,1418079600"; d="scan'208";a="101193278" Received: from ppsw-50.csi.cam.ac.uk ([131.111.8.150]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 24 Feb 2015 20:11:41 +0100 X-Cam-AntiVirus: no malware found X-Cam-ScannerInfo: http://www.cam.ac.uk/cs/email/scanner/ Received: from host86-159-4-23.range86-159.btcentralplus.com ([86.159.4.23]:33952 helo=study.localdomain) by ppsw-50.csi.cam.ac.uk (smtp.hermes.cam.ac.uk [131.111.8.158]:587) with esmtpsa (PLAIN:lpw25) (TLSv1.2:AES128-GCM-SHA256:128) id 1YQKtQ-0001Pk-rZ (Exim 4.82_3-c0e5623) (return-path ); Tue, 24 Feb 2015 19:11:40 +0000 From: Leo White To: David Allsopp Cc: OCaml List References: <000401d05056$ed605f70$c8211e50$@metastack.com> <87wq372noc.fsf@study.localdomain> X-Face: "XWxb[u_Z\PA_Y?9@|IA!!+jTb(/290-*ea/Un$I0B98.$n%eL.;2w*,z]WR#T:,p[ NBd++M7l]#7zj7!{~iw $W-"/=|dVjhT[D{4~gE}gK<2`.6fs!;uqqud]vs2N/3^m7{aS1V, Date: Tue, 24 Feb 2015 19:11:40 +0000 In-Reply-To: (David Allsopp's message of "Tue, 24 Feb 2015 18:26:41 +0000") Message-ID: <87sidv2kgj.fsf@study.localdomain> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain Subject: Re: [Caml-list] Match error with abstract types in modules >> so that `int foo` is equal to `float foo`, then your match isn't really >> exhaustive. > > How so? 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. > 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 = function A -> () | B -> () > This is because `foo B` may not always be rejected. Consider the following code: module F (Foo : sig type 'a foo end) = struct type _ t = A : int Foo.foo t | B : float Foo.foo t let foo = function | A -> () | B -> () (* [foo B] would be an error here *) end module M = F(struct type 'a foo = unit end) (* But out here it is fine *) let () = M.foo M.B > although > > let foo = function A | B -> () > > unsurprisingly does not type. That's due to GADTs not currently being compatible with or-patterns, it is not related to the injectivity issues you are having. >> 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? 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. > It's rather useful - the constructors of a GADT are > partionable by type. 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: type z = Z type 'a s = S 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. > 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) = > 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. 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. Regards, Leo