Re: [Caml-list] GADT and locally ADT

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

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