Trying to make "anonymous types"

“Anonymous types” is a term I made up because I don’t know what to call the thing I want. I was looking at the Haskell library, “Justified containers”—specifically Data.Map.Justified and its code. To summarize, the library uses phantom types to ensure keys are present in a given map so lookup operations (the equivalent of Map.S.find) will never fail. Needless to say, I wanted to see if it would be possible to do something similar in OCaml.

This is my initial attempt:

module type S = sig
  type 'a map_t
  type key_t
  type 'ph key
  type ('ph, 'elt) map
  val with_map : 'elt map_t -> (('ph, 'elt) map -> 'a) -> 'a
  val mem : key_t -> ('ph, 'elt) map -> 'ph key option
  val find : 'ph key -> ('ph, 'elt) map -> 'elt
end

module Justified (M: Map.S) :
  S with type key_t := M.key and type 'a map_t := 'a M.t
= struct

  type 'ph key = M.key
  type ('ph, 'elt) map = 'elt M.t

  let with_map map f = f map

  let mem key map =
    if M.mem key map then Some key
    else None

  let find = M.find
end

module StringMap = Map.Make(String)
module JstringMap = Justified(StringMap)

let () =
  JstringMap.with_map (StringMap.of_list ["foo", 1; "bar", 2]) @@ fun m1 ->
  JstringMap.with_map (StringMap.of_list ["baz", 3]) @@ fun m2 ->
  match JstringMap.mem "foo" m1 with
  | None -> print_endline "nope"
  | Some foo ->
    Printf.printf "%d\n" (JstringMap.find foo m1);
    (* we want this to be a type error *)
    Printf.printf "%d\n" (JstringMap.find foo m2)

The desired effect is that m1 and m2 would have different types, so trying to fetch the “proven key” from m2 is simply a type error.

As I suspected, this is not what happens. Both m1 and m2 receive the type ('a, int) map and my key (type 'a key), which was proven for m1, when used with m2 is considered well typed and simply fails at runtime. We can modify the end of the program to explicitly fill in the phantom type, and it produces the desired effect:

type m1
type m2

let () =
  JstringMap.with_map (StringMap.of_list ["foo", 1; "bar", 2]) @@
  fun (m1: (m1, int) JstringMap.map) ->
  JstringMap.with_map (StringMap.of_list ["baz", 3]) @@
  fun (m2: (m2, int) JstringMap.map) ->
  match JstringMap.mem "foo" m1 with
  | None -> print_endline "nope"
  | Some foo ->
    Printf.printf "%d\n" (JstringMap.find foo m1);
    (* we want this to be a type error *)
    Printf.printf "%d\n" (JstringMap.find foo m2)

Now the program fails to compile (which is good in this case) because the phantom type of key does not match the phantom type of m2.

However, this solution is manifestly idiotic. It puts the onus on the library consumer to create unique types for every map they want to use and to annotate maps manually, which, aside from being a lot of typing, is also error-prone.

Hence the desire for an “anonymous type”. What I mean is that I’d like with_map to somehow fill in the phantom type variable with a random, unique type. From looking at the Haskell code, it looks like it “just does it”, but I’m not particularly fluent in Haskell and I wonder if something I don’t fully understand is happening with forall ph. in some of the type declarations. This is the Haskell code I’m looking at.

Is there a way to do something similar in OCaml? I keep thinking about existential types, but I don’t know how they would apply in this case. (it’s almost the opposite: making a type disappear where there was one, whereas I want to make a type appear where there was none)

I found a way to do something with existential types after all! I added the wrap GADT (to be renamed…), which makes the phantom type of the map existential. When unwrapped in client code, the phantom type is set to a unique, generated type—i.e. an existential type—and m1 and m2 no longer have the same type.

module type S = sig
  type 'a map_t
  type key_t
  type 'ph key
  type ('ph, 'elt) map
  type _ wrap =
    Map : ('ph, 'elt) map -> 'elt wrap
  val with_map : 'elt map_t -> ('elt wrap -> 'a) -> 'a
  val mem : key_t -> ('ph, 'elt) map -> 'ph key option
  val find : 'ph key -> ('ph, 'elt) map -> 'elt
end

module Justified (M: Map.S) :
  S with type key_t := M.key and type 'a map_t := 'a M.t
= struct

  type 'ph key = M.key
  type ('ph, 'elt) map = 'elt M.t
  type _ wrap =
    Map : ('ph, 'elt) map -> 'elt wrap

  let with_map map f =
    f (Map map)

  let mem key map =
    if M.mem key map then Some key
    else None

  let find = M.find
end

module StringMap = Map.Make(String)
module JstringMap = Justified(StringMap)

let () =
  JstringMap.with_map (StringMap.of_list ["foo", 1; "bar", 2]) @@
  fun (Map m1) ->
  JstringMap.with_map (StringMap.of_list ["baz", 3]) @@
  fun (Map m2) ->
  match JstringMap.mem "foo" m1 with
  | None -> print_endline "nope"
  | Some foo ->
    Printf.printf "%d\n" (JstringMap.find foo m1);
    (* This is now a type error! *)
    Printf.printf "%d\n" (JstringMap.find foo m2)

I’ll leave this “unsoved” for a little while in case anyone has additional thoughts or possibly a more elegant solution.

Are you using this in some publicly accessible code anywhere?

I’m considering adding it to Dromedary and a half - GADT Gallery but I prefer adding a link to a source code repo.

Uh… not yet!

I just wrote it this morning. I’ll add some comments, write a short readme and put it on github for you.

1 Like

The difference between your with_map type and the one in Haskell is that in the Haskell implementation, the ph Type variable is bound in the forall inside the continuation, whereas in yours it’s only bound on the outside.
This is called higher rank polymorphism (because you can have functions that take other functions as parameters that are themselves polymorphic).

OCaml does actually support this but only indirectly. You’re allowed to write a higher rank type as long as you wrap it in a record.

So in your case that would be

type ('elt, 'a) with_map_cont =
    {  run : 'ph. ('ph, 'elt) map -> 'a
    }
val with_map : 'elt map_t -> ('elt, 'a) with_map_cont -> 'a
1 Like

So in this case it requires the same amount of boilerplate as with a GADT?

Still, it looks like an interesting solution. I might try it.

The code is github’d.

3 Likes