Re: [Caml-list] GADT existential escape

[Jeremy Yallop <yallop@gmail.com>]

On 19 March 2015 at 10:44, Daniel Bünzli <daniel.buenzli@erratique.ch> wrote:
> Le jeudi, 19 mars 2015 à 02:27, Milan Stanojević a écrit :
>> This is doable in OCaml.
[...]
> However are you sure your example compiles (tried to check, but Core fails on me in the toplevel) ? Trying the following [1] self-contained implementation of the idea [1] the compiler still complains about escaping types.
[...]
> let lookup : dict -> 'a key -> 'a option = fun d k ->
>   let rec find = function
>   | [] -> None
>   | B (k', v) :: bs ->
>       match eq k k' with
>       | None -> find bs
>       | Some Eq -> Some v
>   in
>   find d

This needs a locally-abstract type ("type a. ") to allow type
refinement when you match against the GADT

   let lookup : type a. dict -> a key -> a option = fun d k ->

and an additional annotation for the inner function:

  let rec find : dict -> a option = function

Jeremy.