CODEWITHSUNDEEP
ocaml
Demi
Demi

Reputation: 3611

How does this OCaml code work?

The following OCaml code creates a universal type (not mine, from Jane Street's website):

module Univ : sig
   type t 
   val embed: unit -> ('a -> t) * (t -> 'a option) 
end = struct
   type t = bool -> unit
   let embed () =
    let r = ref None in
    let put x =
     let sx = Some x in
     fun b -> r := if b then sx else None
    in
    let get f =
     f true;
     let res = !r in
     f false; res
    in
    put, get
end

creates a universal type. In it, a call to embed () creates a 2-tuple of functions. The first function in the tuple stores an arbitrary value in the closed-over ref cell; the second function retrieves it. If the wrong value of type t is given to the second function, it returns None instead. However, it appears to me that this would cause the ref cell to be cleared and thus further attempts to retrieve the value to fail, which does not happen. Also, I do not understand in general what happens when passed a wrong value to the projection function get.

Upvotes: 2

Views: 162

Answers (1)

Pierre Chambart
Pierre Chambart

Reputation: 1489

When embed is called, a fresh reference r and two fresh closures for the functions put and get are allocated. When some put is called it returns a fresh function (let's call it the setter) that also has r in its closure.

  • If that setter is given to the corresponding get, the r captured in both closure is the same, hence when get calls f true, it modifies the r in get closure, and let res = !r read a Some value.

    let get f =
  f true;         (* assign the shared reference r *)
  let res = !r in (* read   r *)
  f false;        (* clear  r *)
  res

  • If the setter is given to a non-corresponding get, the r captured by get and the setter is not the same. (let's call them r1 and r2)

    let get f =
  f true;         (* assign r1 *)
  let res = !r in (* read   r2 *)
  f false;        (* clear  r1 *)
  res

    Since the get takes care of always clearing r, we know that before calling get, r2 is None. Hence get will return None.

Upvotes: 7

Related Questions