Re: [Caml-list] GADT existential escape

["Daniel Bünzli" <daniel.buenzli@erratique.ch>]

Le jeudi, 19 mars 2015 à 02:27, Milan Stanojević a écrit :
> This is doable in OCaml.

Cool, a new trick. My understanding of this is basically to apply to types the same idea as Univ by representing them as a first class module.  

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.  

> Note that Univ was possible in OCaml even before first-class
> modules, GADTs and extensible types (which are all used in Type_equal)

Yes, see http://alan.petitepomme.net/cwn/2010.02.09.html#1 if you are interested how.  

Thanks,

Daniel

[1]

module Key = struct
  type _ t = ..
end

module type W = sig
  type t
  type _ Key.t += Key : t Key.t
end

type 'a witness = (module W with type t = 'a)

let witness () (type s) =
 let module M = struct
   type t = s
   type _ Key.t += Key : t Key.t
 end
 in
 (module M : W with type t = s)

type ('a, 'b) eq = Eq : ('a, 'a) eq

let eq (type r) (type s) (r : r witness) (s : s witness)
  : (r, s) eq option
  =
  let module R = (val r : W with type t = r) in
  let module S = (val s : W with type t = s) in
  match R.Key with
  | S.Key -> Some Eq
  | _ -> None

type 'a key = 'a witness
type binding = B : 'a key * 'a -> binding
type dict = binding list

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