Re: [Caml-list] GADT and locally ADT

Article View: fa.caml

Article #51

#51

From: Gabriel Scherer
Date: Tue, 04 Jun 2013 05:47

92 lines
6211 bytes

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 <ivg@ieee.org> 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 = <fun>
>
> 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 = <fun>
>
> 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

-- 
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

Technical Details

Message-ID: <fa.+5gzXTlVscJHgiTcnUiWBvFqC9g@ifi.uio.no>

Path:

arc1-ca.pugleaf.net!d5ni687pbl.0!nntp.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!goblin2!goblin1!goblin.stu.neva.ru!uio.no!nntp.uio.no!.POSTED!not-for-mail

References: <fa.5uFIA2a5E/43K8sy3BbYsXbUjtk@ifi.uio.no>

Show Full Headers

Complete Article Headers

X-Google-Thread: c0fe4b917e,e559dbf6f40dc76e,start
X-Google-Attributes: gidc0fe4b917e,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
X-Received: by 10.66.193.131 with SMTP id ho3mr4279151pac.24.1370324879008;
        Mon, 03 Jun 2013 22:47:59 -0700 (PDT)
Path: arc1-ca.pugleaf.net!d5ni687pbl.0!nntp.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!goblin2!goblin1!goblin.stu.neva.ru!uio.no!nntp.uio.no!.POSTED!not-for-mail
From: Gabriel Scherer <gabriel.scherer@gmail.com>
Newsgroups: fa.caml
Subject: Re: [Caml-list] GADT and locally ADT
Date: Tue, 04 Jun 2013 05:47:58 UTC
Organization: Internet mailing list
Lines: 92
Sender: caml-list-request@inria.fr
Message-ID: <fa.+5gzXTlVscJHgiTcnUiWBvFqC9g@ifi.uio.no>
References: <fa.5uFIA2a5E/43K8sy3BbYsXbUjtk@ifi.uio.no>
NNTP-Posting-Host: mail-jess.uio.no
Mime-Version: 1.0
X-Trace: readme.uio.no 1370324878 24932 129.240.7.9 (4 Jun 2013 05:47:58 GMT)
X-Complaints-To: abuse@uio.no
NNTP-Posting-Date: Tue, 4 Jun 2013 05:47:58 +0000 (UTC)
Cc: caml-list@inria.fr
To: Ivan Gotovchits <ivg@ieee.org>
X-IronPort-AV: E=Sophos;i="4.87,797,1363129200"; 
   d="scan'208";a="20174711"
X-Original-To: caml-list@sympa.inria.fr
Delivered-To: caml-list@sympa.inria.fr
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"
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)
In-Reply-To: <87ehciseni.fsf@golf.niidar.ru>
X-Sequence: 6880
X-no-archive: yes
List-Id: <caml-list.inria.fr>
List-Archive: <http://sympa.inria.fr/sympa/arc/caml-list>
List-Help: <mailto:sympa_inria@inria.fr?subject=help>
List-Owner: <mailto:caml-list-request@inria.fr>
List-Post: <mailto:caml-list@inria.fr>
List-Subscribe: <mailto:sympa_inria@inria.fr?subject=subscribe%20caml-list>
List-Unsubscribe: <mailto:sympa_inria@inria.fr?subject=unsubscribe%20caml-list>
Original-Date: Tue, 4 Jun 2013 07:47:06 +0200
Original-Message-Id: <CAPFanBEau9FFNJAVF+9RyhfnbuLi+smcW3Hc6bk2BMxM3ysnnA@mail.gmail.com>
Original-References: <87ehciseni.fsf@golf.niidar.ru>
Bytes: 5904
Content-Type: text/plain; charset=ISO-8859-1

Reply to Parent Message