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