[Caml-list] Obj.magic for polymorphic identifiers

[Caml-list] Obj.magic for polymorphic identifiers

[Romain Bardou]

Hello,

I'm considering using Obj.magic and as the type-checker can no longer
ensure type safety, I decided to come here for advice.

I want to implement the trick with GADTs where you test equality of
unique identifiers, and if they match this adds an equality constraint
on types. I want this code to be small and well abstracted in a module
so that if this module is safe, then using this module cannot cause a
seg fault.

Here is the signature of my module:

(************************************************************************)
(** Polymorphic identifiers. *)

(** The type of identifiers associated to type ['a]. *)
type 'a t

(** Make a new, fresh identifier.
    This is the only way to obtain a value of type [t]. *)
val fresh: unit -> 'a t

(** Type constraint which is conditioned on identifier equality. *)
type (_, _) equal =
  | Equal: ('a, 'a) equal
  | Different: ('a, 'b) equal

(** Equality predicate. *)
val equal: 'a t -> 'b t -> ('a, 'b) equal

(** Convert an identifier to an integer.
    The integer is guaranteed to be unique for each call to {!fresh}. *)
val to_int: 'a t -> int
(************************************************************************)

and here is the implementation:

(************************************************************************)
type 'a t = int

let fresh =
  let counter = ref (-1) in
  fun () ->
    incr counter;
    !counter

type (_, _) equal =
  | Equal: ('a, 'a) equal
  | Different: ('a, 'b) equal

let equal (type a) (type b) (a: a t) (b: b t): (a, b) equal =
  if a = b then
    (Obj.magic (Equal: (a, a) equal): (a, b) equal)
  else
    Different

let to_int x =
  x
(************************************************************************)

Finally, here is a test program:

(************************************************************************)
open Polid

let () =

  let x = fresh () in
  let y = fresh () in

  let eq (type a) (type b) (t: a t) (u: b t) (a: a) (b: b) =
    match equal t u with
      | Equal ->
          if a = b then "true" else "false"
      | Different ->
          "false"
  in

  print_endline (eq x y 5 "salut"); (* false *)
  print_endline (eq x x 5 5); (* true *)
  print_endline (eq x x 5 9); (* false *)
  print_endline (eq y y "test" "salut"); (* false *)
  print_endline (eq y y "test" "test"); (* true *)
  print_endline (eq y x "salut" 5); (* false *)
  (* print_endline (eq x x 5 "salut"); (\* type error *\) *)
  (* print_endline (eq y y "salut" 5); (\* type error *\) *)

  ()
(************************************************************************)

It relies heavily on the fact that "fresh ()" cannot be generalized as
'a t is abstract.

A typical use case is as follows: I have two heterogeneous association
lists (using GADTs for existential types). As I iterate on one of those
lists, I need to find the corresponding item in the other list. As I
unpack the existential, the type-checker cannot prove that the
existential types are equal, hence the need for a runtime check (a call
to Polid.equal).

Can you find any reason why this would not be safe, or any better way to
implement this?

Thank you,

-- 
Romain Bardou
-- 
Romain Bardou
Cryptosense
96bis boulevard Raspail, 75006 Paris, France
+33 (0)9 72 42 35 31

Re: [Caml-list] Obj.magic for polymorphic identifiers

[Jeremie Dimino]

[-- Attachment #1: Type: text/plain, Size: 1403 bytes --]

On Tue, Apr 22, 2014 at 9:03 AM, Romain Bardou <romain@cryptosense.com>wrote:

> I want to implement the trick with GADTs where you test equality of
> unique identifiers, and if they match this adds an equality constraint
> on types. I want this code to be small and well abstracted in a module
> so that if this module is safe, then using this module cannot cause a
> seg fault.
>
> Here is the signature of my module:
> [...]
>

We do exactly this at Jane Street in our type_equal module:

https://github.com/janestreet/core_kernel/blob/master/lib/type_equal.ml#L87

Note that using the open_types branch of ocaml [1] there is a cool way to
do this:

(************************************************************************)
type 'a key = ..

type (_, _) equal =
  | Equal: ('a, 'a) equal
  | Different: ('a, 'b) equal

module type S = sig
  type t
  type 'a key += T : t key
end

type 'a t = (module S with type t = 'a)

let fresh (type a) () =
  let module M = struct
    type t = a
    type 'a key += T : t key
  end in
  (module M : S with type t = a)

let equal (type a) (type b)
      (module A : S with type t = a)
      (module B : S with type t = b)
  : (a, b) equal =
  match A.T with
  | B.T -> Equal
  | _   -> Different

let to_int = Hashtbl.hash
(************************************************************************)

  [1] http://caml.inria.fr/mantis/view.php?id=5584

-- 
Jeremie

[-- Attachment #2: Type: text/html, Size: 2457 bytes --]

Re: [Caml-list] Obj.magic for polymorphic identifiers

[Goswin von Brederlow]

On Tue, Apr 22, 2014 at 09:31:13AM +0100, Jeremie Dimino wrote:
> On Tue, Apr 22, 2014 at 9:03 AM, Romain Bardou <romain@cryptosense.com>wrote:
> 
> > I want to implement the trick with GADTs where you test equality of
> > unique identifiers, and if they match this adds an equality constraint
> > on types. I want this code to be small and well abstracted in a module
> > so that if this module is safe, then using this module cannot cause a
> > seg fault.
> >
> > Here is the signature of my module:
> > [...]
> >
> 
> We do exactly this at Jane Street in our type_equal module:
> 
> https://github.com/janestreet/core_kernel/blob/master/lib/type_equal.ml#L87
> 
> Note that using the open_types branch of ocaml [1] there is a cool way to
> do this:
> 
> (************************************************************************)
> type 'a key = ..
> 
> type (_, _) equal =
>   | Equal: ('a, 'a) equal
>   | Different: ('a, 'b) equal
> 
> module type S = sig
>   type t
>   type 'a key += T : t key
> end
> 
> type 'a t = (module S with type t = 'a)
> 
> let fresh (type a) () =
>   let module M = struct
>     type t = a
>     type 'a key += T : t key
>   end in
>   (module M : S with type t = a)
> 
> let equal (type a) (type b)
>       (module A : S with type t = a)
>       (module B : S with type t = b)
>   : (a, b) equal =
>   match A.T with
>   | B.T -> Equal
>   | _   -> Different
> 
> let to_int = Hashtbl.hash
> (************************************************************************)
> 
>   [1] http://caml.inria.fr/mantis/view.php?id=5584
> 
> -- 
> Jeremie

Now that is a good reason to have open types. I've tried (and failed)
to do something like this without resorting to magic and the only way
I found was to declare a big GADT that has a constructor for every
possible type and match all possible equal pairs. That realy doesn't
scale well.


Would it be possible for someone familiar with the patch to create a
pull request for it on git? Maybe that way it could be merged in
faster.

MfG
	Goswin

Re: [Caml-list] Obj.magic for polymorphic identifiers

[Dmitry Grebeniuk]

Hello.

  It's perfectly doable without Obj at all.
  I needed "semi-typed" values quite often, so
decided to write reusable library "cadastr" [1]
that handles them, along with "untyped methods",
structural [de]composition (hence [de]serialization
based on value structure) and more.

  Things you need could be written like:

$ ocaml
        Objective Caml version 3.12.1

# #use "topfind";;
[...]
# #require "cadastr";;
[...]
# open Cdt;;
# let hlist = [ubox ti_int 123; ubox ti_string "qwe"; ubox ti_bool true];;
val hlist : Cdt.ubox list =
  [{ub_store = <fun>; ub_uti = <obj>}; {ub_store = <fun>; ub_uti = <obj>};
   {ub_store = <fun>; ub_uti = <obj>}]
# let dump ub =
  let uti = ub.ub_uti in
  if uti == (ti_string :> uti) then uget_exn ti_string ub else
  if uti == (ti_int :> uti) then string_of_int (uget_exn ti_int ub) else
  if uti == (ti_bool :> uti) then string_of_bool (uget_exn ti_bool ub) else
  "<unknown>";;
val dump : Cdt.ubox -> string = <fun>
# List.iter (fun ub -> print_endline (dump ub)) hlist;;
123
qwe
true
- : unit = ()
#

  As for "methods" I 've mentioned above,

# List.iter (fun ub ->
  let ushow = get_meth_untyped "show" ub.ub_uti in
  let ures = u_app ushow ub in
  print_endline (uget_exn ti_string ures)
  ) hlist;;
123
"qwe"
True
- : unit = ()
#

  However there is some runtime cost on such
"untyped" values.


[1] https://bitbucket.org/gds/cadastr , but it doesn't
    compile with OCaml >= 4.  It can be fixed;
    I'll do it if someone will want to use it.

Re: [Caml-list] Obj.magic for polymorphic identifiers

[Goswin von Brederlow]

On Thu, Apr 24, 2014 at 06:30:24PM +0300, Dmitry Grebeniuk wrote:
> Hello.
> 
>   It's perfectly doable without Obj at all.
>   I needed "semi-typed" values quite often, so
> decided to write reusable library "cadastr" [1]
> that handles them, along with "untyped methods",
> structural [de]composition (hence [de]serialization
> based on value structure) and more.
> 
>   Things you need could be written like:
> 
> $ ocaml
>         Objective Caml version 3.12.1
> 
> # #use "topfind";;
> [...]
> # #require "cadastr";;
> [...]
> # open Cdt;;
> # let hlist = [ubox ti_int 123; ubox ti_string "qwe"; ubox ti_bool true];;
> val hlist : Cdt.ubox list =
>   [{ub_store = <fun>; ub_uti = <obj>}; {ub_store = <fun>; ub_uti = <obj>};
>    {ub_store = <fun>; ub_uti = <obj>}]

How do you encode a

type foo = Foo | Bar

Someone has to implement a ti_foo for it.

> # let dump ub =
>   let uti = ub.ub_uti in
>   if uti == (ti_string :> uti) then uget_exn ti_string ub else
>   if uti == (ti_int :> uti) then string_of_int (uget_exn ti_int ub) else
>   if uti == (ti_bool :> uti) then string_of_bool (uget_exn ti_bool ub) else
>   "<unknown>";;

Here you have to match every possible type, which doesn't scale. Or
you limit yourself to structure, which is unsound for retrieving the
original type.

> val dump : Cdt.ubox -> string = <fun>
> # List.iter (fun ub -> print_endline (dump ub)) hlist;;
> 123
> qwe
> true
> - : unit = ()
> #

So you can print the values. But how to you get them back?
Where is your

val unbox : type a . uti -> Cdt.ubox -> a

(which isn't well typed like that)
 
>   As for "methods" I 've mentioned above,
> 
> # List.iter (fun ub ->
>   let ushow = get_meth_untyped "show" ub.ub_uti in
>   let ures = u_app ushow ub in
>   print_endline (uget_exn ti_string ures)
>   ) hlist;;
> 123
> "qwe"
> True
> - : unit = ()
> #
> 
>   However there is some runtime cost on such
> "untyped" values.
> 
> 
> [1] https://bitbucket.org/gds/cadastr , but it doesn't
>     compile with OCaml >= 4.  It can be fixed;
>     I'll do it if someone will want to use it.

MfG
	Goswin

Re: [Caml-list] Obj.magic for polymorphic identifiers

[Dmitry Grebeniuk]

Hello.

>> # open Cdt;;
>> # let hlist = [ubox ti_int 123; ubox ti_string "qwe"; ubox ti_bool true];;
>> val hlist : Cdt.ubox list =
>>   [{ub_store = <fun>; ub_uti = <obj>}; {ub_store = <fun>; ub_uti = <obj>};
>>    {ub_store = <fun>; ub_uti = <obj>}]
>
> How do you encode a
>
> type foo = Foo | Bar
>
> Someone has to implement a ti_foo for it.

  I do not encode type foo anyhow, if its structure is
not needed, like in Romain's example.  As for ti_foo,
you are right:
  let ti_foo : foo #ti = new ti_simple "foo" ()
is enough to box/unbox values of type foo using
ti_foo.  (Also type name is not needed, but it eases
values introspection, so I always use meaningful
type names here.  Type annotation is not needed
too, in most cases.)

>>   if uti == (ti_string :> uti) then uget_exn ti_string ub else

> Here you have to match every possible type, which doesn't scale.

  It's just Romain's example encoded with my library.
Of course this approach doesn't scale, but second
piece of code ("show" method) scales well.

> Or you limit yourself to structure, which is unsound
> for retrieving the original type.

  Sorry, can't understand what you mean here;
but maybe other parts of my reply answer this.

> Where is your
>
> val unbox : type a . uti -> Cdt.ubox -> a
>
> (which isn't well typed like that)

  Of course it's not typed.  One has to provide
"witness" for this operation.  Both examples had
such "unbox":

uget_exn : #tti 'a -> ubox -> 'a

  So, no magic.  But no Obj too!

  Answering further possible questions:
- What if 'a and 'b, where 'a <> 'b, will have the
same "runtime type information"?  --
It's impossible.  ('a and 'b could _look_ different
due to type aliases or module abstractions,
but they have the same "original type")
- What if one creates two distinct "runtime type
informations" for given 'a, how will this work?  --
It won't work: once a "witness" was used to
create ubox, only this "witness" can be used to
retrieve typed value.
  (however I do some kind of "inheritance" on
"witnesses" and untyped methods dictionaries
that allows me to use some tricks like redefining
"show" or "cmp" methods leaving possibility
to work with uboxes using different typeinfos,
but it's not essential here.)

Re: [Caml-list] Obj.magic for polymorphic identifiers

[Leo White]

> Now that is a good reason to have open types. I've tried (and failed)
> to do something like this without resorting to magic and the only way
> I found was to declare a big GADT that has a constructor for every
> possible type and match all possible equal pairs. That realy doesn't
> scale well.
>
>
> Would it be possible for someone familiar with the patch to create a
> pull request for it on git? Maybe that way it could be merged in
> faster.
>
> MfG
> 	Goswin

As it happens they have just been merged:

https://github.com/ocaml/ocaml/commit/b56dc4b3df8d022b54f40682a9d5d4168c690413

Regards,

Leo