Re: [Caml-list] GADT existential escape

["Milan Stanojević" <milanst@gmail.com>]

This is doable in OCaml.
Core has one possible implementation.
https://github.com/janestreet/core_kernel/blob/master/lib/type_equal.mli#L171

type 'a key = 'a Type_equal.Id.t

let lookup dict key =
   List.find_map disct ~f:(function
    | B (key', a) ->
      match Type_equal.Id.same_witness key key' with
      | None -> None
      | Some T -> Some a)
;;

You can also check out Univ and Univ_map modules in Core.

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

https://blogs.janestreet.com/a-universal-type/


On Wed, Mar 18, 2015 at 9:07 PM, Daniel Bünzli
<daniel.buenzli@erratique.ch> wrote:
> Le jeudi, 19 mars 2015 à 01:39, Milan Stanojević a écrit :
>> Can you give some hypothetical example code ?
> type 'a key = ?
> type binding = B : 'a key * 'a -> binding
> type dict = binding list
> let lookup : dict -> 'a key -> 'a option = fun d k -> ?
>
> Is it possible to specify a `'a key` type that allows `lookup` (with the obvious semantics) to be written ? This is trivial to achieve with a universal type, see http://mlton.org/PropertyList
>
> Best,
>
> Daniel
>
>