Re: [Caml-list] GADT and locally ADT

[Gabriel Scherer <gabriel.scherer@gmail.com>]

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