Re: [Caml-list] GADT and locally ADT

[Ivan Gotovchits <ivg@ieee.org>]

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