From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 D12597EE6A for ; Tue, 4 Jun 2013 07:47:47 +0200 (CEST) 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.214.44; 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.214.44 as permitted sender) identity=mailfrom; client-ip=209.85.214.44; 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-bk0-f44.google.com) identity=helo; client-ip=209.85.214.44; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-bk0-f44.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AsUAAHB+rVHRVdYsk2dsb2JhbABZgzmsaZIdewgWDgEBAQEHCwsJFAQkgiMBAQQBJxkBGxILAQMBCwYFCwMKDSEiAREBBQEKEgYTEodoAQMJBgyeQoxKgn2FAQoZJwMKWIguAQUMjxoHg1gDlz6BKY4yFimENzo X-IPAS-Result: AsUAAHB+rVHRVdYsk2dsb2JhbABZgzmsaZIdewgWDgEBAQEHCwsJFAQkgiMBAQQBJxkBGxILAQMBCwYFCwMKDSEiAREBBQEKEgYTEodoAQMJBgyeQoxKgn2FAQoZJwMKWIguAQUMjxoHg1gDlz6BKY4yFimENzo X-IronPort-AV: E=Sophos;i="4.87,797,1363129200"; d="scan'208";a="20174671" Received: from mail-bk0-f44.google.com ([209.85.214.44]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 04 Jun 2013 07:47:47 +0200 Received: by mail-bk0-f44.google.com with SMTP id r7so754134bkg.31 for ; Mon, 03 Jun 2013 22:47:46 -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=IC/TZmITTi6D64PjBKMpIHz3QehX/drdXUZmHKd8XFg=; b=Yi1VgDk/IOKml3ruxQOlMcCUVkqoX2xjBDBaQeqozVrHs/ZUXGdz9WeJvk9vGYntfJ uDEW1yCjyMqpnoNXl4NBzChrfg1fKGXcvWM8+8nI8prliAni3mP8R880MsU0tyjilMgR XLn2Rt8YTJfnltYRTj/60pfZQIL4o069tTkeH9qB03R8q722oQHciq4Uo14QNupT1eEd cnkY09VjQfQK/guyatDwNFb4MVOLtd6vooSlIjhM6T3Ph7V8bLOVANmH79hDJBpF11Qx K0ylhB9iarQFKgyd7kvJbk7jvMK3WIeBg6VEFWbUJFus72ih4RjBMnHokn7RCOggGC9h dyAQ== X-Received: by 10.204.227.201 with SMTP id jb9mr7354277bkb.96.1370324866769; Mon, 03 Jun 2013 22:47:46 -0700 (PDT) MIME-Version: 1.0 Received: by 10.204.35.75 with HTTP; Mon, 3 Jun 2013 22:47:06 -0700 (PDT) In-Reply-To: <87ehciseni.fsf@golf.niidar.ru> References: <87ehciseni.fsf@golf.niidar.ru> From: Gabriel Scherer Date: Tue, 4 Jun 2013 07:47:06 +0200 Message-ID: To: Ivan Gotovchits Cc: caml-list@inria.fr Content-Type: text/plain; charset=ISO-8859-1 Subject: Re: [Caml-list] GADT and locally ADT If the function knows (or infer) that the argument type is (ro), then there is only one case to handle. But there is also a function that is polymorphic over the second argument, and it must be callable with both (ro) and (rw) values : this function works "for any access mode". This is what the annotated function > let f (type t) (inp: ('a,t) access) = match inp with > | ReadWrite (ch) -> () > | Read (ch) -> ();; does. Now, when you write: > let f1 = function > | ReadWrite (ch) -> ();; the inference will deduce from the pattern that the expected type is (rw). This is the most general type if you assume that the user only writes exhaustive patterns. But because of this specialization, extending this pattern-matching with a (ro) case will not type-check without an annotation. On Tue, Jun 4, 2013 at 6:06 AM, Ivan Gotovchits wrote: > > I'm trying to get a grasp of GADT with a simple example, in which I use subj as a > phantom type. With the following, purely synthetical types: > > type ro > type rw > > type ('a,_) access = > | Read : 'a -> ('a,ro) access > | ReadWrite : 'a -> ('a,rw) access > > next I define function > > let f1 = function > | ReadWrite (ch) -> ();; > > val f : ('a, rw) access -> unit = > > That's ok, I understand, by intuition, that the argument of the function > shouldn't have both types at once: ('a,rw) access and ('a,ro) access. So > the matching is exhaustive. In accordance with it, compiler forbids the > following function: > > let f inp = match inp with > | ReadWrite (ch) -> () > | Read (ch) -> ();; > > Characters 57-66: > | Read (ch) -> ();; > ^^^^^^^^^ > Error: This pattern matches values of type ('a, ro) access > but a pattern was expected which matches values of type > ('a, rw) access > > But, if I add a type annotation I can successfully delude the compiler > and it typechecks what he has recently considered illegal: > > let f (type t) (inp: ('a,t) access) = match inp with > | ReadWrite (ch) -> () > | Read (ch) -> ();; > > val f : ('a, 'b) access -> unit = > > Are there any logical explanation to this? > > Thank in advance! > > > -- > (__) > (oo) > /------\/ > / | || > * /\---/\ > ~~ ~~ > ...."Have you mooed today?"... > > -- > 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