[Caml-list] GADT existential escape

[Caml-list] GADT existential escape

[Daniel Bünzli]

Hello,  

Is it possible to escape a GADT existential using some kind of witness the same way a universal type would allow me ? I think the answer is no, but I'd love to be proven wrong. 

Best,

Daniel

Re: [Caml-list] GADT existential escape

[Milan Stanojević]

What do you mean exactly?

Can you give some hypothetical example code ?

On Wed, Mar 18, 2015 at 8:29 PM, Daniel Bünzli
<daniel.buenzli@erratique.ch> wrote:
> Hello,
>
> Is it possible to escape a GADT existential using some kind of witness the same way a universal type would allow me ? I think the answer is no, but I'd love to be proven wrong.
>
> Best,
>
> Daniel
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

Re: [Caml-list] GADT existential escape

[Daniel Bünzli]

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

Re: [Caml-list] GADT existential escape

[Milan Stanojević]

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
>
>

Re: [Caml-list] GADT existential escape

[Daniel Bünzli]

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

Re: [Caml-list] GADT existential escape

[Jeremy Yallop]

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.

Re: [Caml-list] GADT existential escape

[Jeremie Dimino]

On Thu, Mar 19, 2015 at 10:44 AM, Daniel Bünzli
<daniel.buenzli@erratique.ch> wrote:
> tried to check, but Core fails on me in the toplevel

Core should work in the toplevel, why is it failing?

> Trying the following [1] self-contained implementation of the idea [1] the compiler still complains about escaping types.

You need to help the typer a bit:

let lookup : type a. 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 :> a)
  in
  find d

-- 
Jeremie

Re: [Caml-list] GADT existential escape

[Daniel Bünzli]

Thanks Jerem{y,ie} for the answers !  

Now I'm naively trying to backport this using exceptions — I'm conservative and old fashioned. But I'm failing to type this Eq value, any hints maybe ?  

module W : sig
  type 'a t
  val w : 'a t
end = struct
  type 'a t = unit
  let w = ()
end

module type W = sig
  type t
  exception E of t W.t
end

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

let witness () (type s) =
  let module M = struct
    type t = s
    exception E of t W.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.E W.w with
  | S.E _ -> Some Eq (* Compiler screams here. *)
  | _ -> None



N.B. As it stands this is slightly less efficient than using open variants, since you'd have to allocate an exn value for checking equality.  

Best,

Daniel

Re: [Caml-list] GADT existential escape

[Daniel Bünzli]

Le jeudi, 19 mars 2015 à 12:05, Jeremie Dimino a écrit :
> Core should work in the toplevel, why is it failing?

> ocaml
OCaml version 4.01.0
Findlib has been successfully loaded. Additional directives:
#require "package";; to load a package
#list;; to list the available packages
#camlp4o;; to load camlp4 (standard syntax)
#camlp4r;; to load camlp4 (revised syntax)
#predicates "p,q,...";; to set these predicates
Topfind.reset();; to force that packages will be reloaded
#thread;; to enable threads
# #require "core";;
[…]
/Users/dbuenzli/.opam/4.01.0/lib/sexplib_unix/sexplib_unix.cma: loaded
/Users/dbuenzli/.opam/4.01.0/lib/core: added to search path


# #require "core";;am/4.01.0/lib/core/core.cma: loaded
Error: Reference to undefined global `Condition'


Here's a bit of config info:

> opam config report
# OPAM status report
# opam-version 1.2.0
# self-upgrade no
# os darwin
# external-solver aspcud
# criteria -count(removed),-notuptodate(request),-count(down),-notuptodate(changed),-count(changed),-notuptodate(solution)*
# jobs 1
# repositories 1* (http), 1 (version-controlled)
# pinned 16 (version control)
# current-switch 4.01.0
# last-update 2015-03-15 10:44



> opam info core -f installed-version
111.28.01 [4.01.0]

Re: [Caml-list] GADT existential escape

[Jeremie Dimino]

On Thu, Mar 19, 2015 at 11:34 AM, Daniel Bünzli
<daniel.buenzli@erratique.ch> wrote:
> # #require "core";;am/4.01.0/lib/core/core.cma: loaded
> Error: Reference to undefined global `Condition'

It's because core depends on threads. You need to type #thread before
requiring "core".

-- 
Jeremie

Re: [Caml-list] GADT existential escape

[Daniel Bünzli]

Le jeudi, 19 mars 2015 à 12:34, Daniel Bünzli a écrit :
> Now I'm naively trying to backport this using exceptions — I'm conservative and old fashioned. But I'm failing to type this Eq value, any hints maybe ?

My guess is that by going through the `exn` type you are loosing the type variable so it doesn't seem to be possible to use exceptions to encoding the open variant type here.  

Daniel

Re: [Caml-list] GADT existential escape

[Milan Stanojević]

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

Yup, sorry, I just wrote the code without checking it.

Re: [Caml-list] GADT existential escape

[Milan Stanojević]

> N.B. As it stands this is slightly less efficient than using open variants, since you'd have to allocate an exn value for checking equality.
>

Exceptions and open variants are actually exactly the same.
"exception" is basically a syntactic sugar now.
exception Foo of int is the same as type exn += Foo of int.

Re: [Caml-list] GADT existential escape

[Daniel Bünzli]

Le jeudi, 19 mars 2015 à 17:46, Milan Stanojević a écrit :
> Exceptions and open variants are actually exactly the same.

Well apparently not. It seems that open variants are more expressive.  

Daniel

Re: [Caml-list] GADT existential escape

[Frédéric Bour]

Indeed, open variants can have type parameters.
But exceptions really are sugar over a non-parameterized open variant.

On 19/03/2015 18:14, Daniel Bünzli wrote:
> Le jeudi, 19 mars 2015 à 17:46, Milan Stanojević a écrit :
>> Exceptions and open variants are actually exactly the same.
> Well apparently not. It seems that open variants are more expressive.
>
> Daniel
>
>
>

Re: [Caml-list] GADT existential escape

[Milan Stanojević]

On Thu, Mar 19, 2015 at 1:15 PM, Frédéric Bour
<frederic.bour@lakaban.net> wrote:
> Indeed, open variants can have type parameters.
> But exceptions really are sugar over a non-parameterized open variant.

If your OCaml version supports open variants, then exceptions and open
variants are exactly the same.
For example, this is legal code:
type exn += Foo : 'a list -> exn

Re: [Caml-list] GADT existential escape

[Jeremy Yallop]

Daniel Bünzli wrote:
>> N.B. As it stands this is slightly less efficient than using open variants, since you'd have to allocate an exn value for checking equality.

Milan Stanojević:
> Exceptions and open variants are actually exactly the same.

More precisely, the exn type is a particular extensible variant with
some additional syntactic sugar.  The exn type doesn't support GADT
constructors (since it doesn't have type parameters), so it can't be
used to implement the typed keys under discussion -- at least, not in
the same way as Core's extensible-variant-based implementation.

The point here, though, is that Daniel's code allocates:

    match R.E W.w with

while the version using open variants does not allocate:

    match A.Key with

Jeremy.

Re: [Caml-list] GADT existential escape

[Alain Frisch]

On 03/19/2015 06:41 PM, Jeremy Yallop wrote:
> The exn type doesn't support GADT
> constructors (since it doesn't have type parameters)

Note that even if exn doesn't have type parameters, it supports the GADT 
syntax to define constructors with existentials:


exception A: 'a * ('a -> string) -> exn;;


-- Alain

Re: [Caml-list] GADT existential escape

[Yaron Minsky]

Core_kernel has the code you want, and I believe does not require threads, FWIW.

y

On Thu, Mar 19, 2015 at 7:59 AM, Jeremie Dimino <jdimino@janestreet.com> wrote:
> On Thu, Mar 19, 2015 at 11:34 AM, Daniel Bünzli
> <daniel.buenzli@erratique.ch> wrote:
>> # #require "core";;am/4.01.0/lib/core/core.cma: loaded
>> Error: Reference to undefined global `Condition'
>
> It's because core depends on threads. You need to type #thread before
> requiring "core".
>
> --
> Jeremie
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs