[Caml-list] GADT and locally ADT

[Caml-list] GADT and locally ADT

[Ivan Gotovchits]

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?"...

Re: [Caml-list] GADT and locally ADT

[Gabriel Scherer]

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

Re: [Caml-list] GADT and locally ADT

[Ivan Gotovchits]

Gabriel Scherer <gabriel.scherer@gmail.com> writes:

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

Looks reasonable, but can you, please, explain the difference between
function:

    let f (type t)  (inp: ('a,t) access)  = match inp with
      | ReadWrite ch -> ()
      | Read ch -> ()

that have type 

    val f : ('a, 'b) access -> unit

and

    let f (inp: ('a,'b) access)  = match inp with
      | ReadWrite ch -> ()
      | Read ch -> ()

that fails to type check:

Error: This pattern matches values of type ('a, ro) access
       but a pattern was expected which matches values of type
         ('a, rw) access

Re: [Caml-list] GADT and locally ADT

[Gabriel Scherer]

In expressions, type variables 'a 'b do not enforce polymorphism, they
are merely name for types that will be inferred.
  let f : 'a -> 'a = fun x -> x + 1
is accepted. So your second example with ('a, 'b) does not enforce polymorphism.

This is not in general a problem as if the inferred type is indeed a
type variable, it will be generalized by the inference algorithm and
therefore "turned into polymorphism" after type inference. It is
problematic however for polymorphic recursive functions (this form of
polymorphism would have to be "guessed" before the recursive
definition is type-checked, and therefore requires an annotation), and
for GADTs.

There are two *distinct* notions used to enforce polymorphism:
- polymorphic type variables as in
    val f : 'a -> 'a
  or
    let f : 'a . 'a -> 'a = ...
  (useful for polymorphic recursion)
- local abstract types
   let f (type t) : t -> t = ...
   fun (type t) -> ...
  (useful for GADTs)

Local abstract types are documented in
http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#toc80 . They
are not type variable (they cannot be unified with anything, hence
enforce polymorphism), but type "constructors" syntactically (like
'list' in ('a list), but without a parameter). We say that GADTs
introduce equations and refine types; they can only refine local
abstract types, not type variables. The refinement of GADT types is
similar to what happen when you traverse a module abstraction, outside
you know the abstract type M.t, and inside you know (type M.t = int).

Due to this "implementation detail" of GADTs, the following code (that
enforces polymorphism) would still fail to type-check:

    let f : 'b . ('a, 'b) access -> unit = function
      | ReadWrite ch -> ()
      | Read ch -> ()

while the following work

    let f (type t) : ('a, t) access -> unit = function
      | ReadWrite ch -> ()
      | Read ch -> ()

Finally, the syntax

   let f : type t . ('a, t) acc -> unit = function ...

is a merge of both ('a 'b . ...) and ((type t) ...): it provides a
local type constructor, and enables polymorphic recursion. This is
what you should use when you write recursive functions using GADTs.




On Tue, Jun 4, 2013 at 9:23 AM, Ivan Gotovchits <ivg@ieee.org> wrote:
> Gabriel Scherer <gabriel.scherer@gmail.com> writes:
>
>> 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.
>
> Looks reasonable, but can you, please, explain the difference between
> function:
>
>     let f (type t)  (inp: ('a,t) access)  = match inp with
>       | ReadWrite ch -> ()
>       | Read ch -> ()
>
> that have type
>
>     val f : ('a, 'b) access -> unit
>
> and
>
>     let f (inp: ('a,'b) access)  = match inp with
>       | ReadWrite ch -> ()
>       | Read ch -> ()
>
> that fails to type check:
>
> Error: This pattern matches values of type ('a, ro) access
>        but a pattern was expected which matches values of type
>          ('a, rw) access

Re: [Caml-list] GADT and locally ADT

[Ivan Gotovchits]

Gabriel Scherer <gabriel.scherer@gmail.com> writes:

> In expressions, type variables 'a 'b do not enforce polymorphism, they
> are merely name for types that will be inferred.
>   let f : 'a -> 'a = fun x -> x + 1
> is accepted. So your second example with ('a, 'b) does not enforce polymorphism.
>
> This is not in general a problem as if the inferred type is indeed a
> type variable, it will be generalized by the inference algorithm and
> therefore "turned into polymorphism" after type inference. It is
> problematic however for polymorphic recursive functions (this form of
> polymorphism would have to be "guessed" before the recursive
> definition is type-checked, and therefore requires an annotation), and
> for GADTs.
>
> There are two *distinct* notions used to enforce polymorphism:
> - polymorphic type variables as in
>     val f : 'a -> 'a
>   or
>     let f : 'a . 'a -> 'a = ...
>   (useful for polymorphic recursion)
> - local abstract types
>    let f (type t) : t -> t = ...
>    fun (type t) -> ...
>   (useful for GADTs)
>
> Local abstract types are documented in
> http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#toc80 . They
> are not type variable (they cannot be unified with anything, hence
> enforce polymorphism), but type "constructors" syntactically (like
> 'list' in ('a list), but without a parameter). We say that GADTs
> introduce equations and refine types; they can only refine local
> abstract types, not type variables. The refinement of GADT types is
> similar to what happen when you traverse a module abstraction, outside
> you know the abstract type M.t, and inside you know (type M.t = int).
>
> Due to this "implementation detail" of GADTs, the following code (that
> enforces polymorphism) would still fail to type-check:
>
>     let f : 'b . ('a, 'b) access -> unit = function
>       | ReadWrite ch -> ()
>       | Read ch -> ()
>
> while the following work
>
>     let f (type t) : ('a, t) access -> unit = function
>       | ReadWrite ch -> ()
>       | Read ch -> ()
>
> Finally, the syntax
>
>    let f : type t . ('a, t) acc -> unit = function ...
>
> is a merge of both ('a 'b . ...) and ((type t) ...): it provides a
> local type constructor, and enables polymorphic recursion. This is
> what you should use when you write recursive functions using GADTs.
>

Thanks for a very informative answer! I hope that I do understand this,
though practice will show.

Thanks again!


-- 
         (__) 
         (oo) 
   /------\/ 
  / |    ||   
 *  /\---/\ 
    ~~   ~~   
...."Have you mooed today?"...