What is the significance of a 'witness' in OCaml(or FP)?

[hyphenrf]

@Mohan_Radhakrishnan

I am wondering if the following example is another use case. Maps and Hash Tables - Real World OCaml has details of comparator_witness

But I can’t relate your example and this.

The need for a witness is a consequence of how Base and Core implement maps and sets (allowing them to be constructed using FCMs^[1], which loses the path of application in the type, i.e. Set.t instead of Set.Make(Mod).t). OCaml’s applicative/generative functor applications^[2] allow you to unify/distinguish implementations in a sound way without witnesses if you wish.

The source of confusion, which I am just guessing please correct me if I’m wrong, is because the witness here does double-duty: carrying runtime-useful data (the comparator function etc) and type metadata (the phantom^[3] type parameter 'witness–the comparator construct itself witnesses the 'witness so it should’ve been named 'witnessed perhaps :P).

The two duties can be separated into two constructs if you wish.

If you look at the Base.comparator docs:

Comparison and serialization for a type, using a witness type to distinguish between comparison functions with different behavior.

type ('a, 'witness) t = private {

1. compare : 'a -> 'a -> int;
2. sexp_of_t : 'a -> Sexp.t;

}

emphasis mine:

('a, 'witness) t contains a comparison function for values of type 'a. Two values of type t with the same 'witness are guaranteed to have the same comparison function.

so that is the invariant this witness upholds through its type.

when you make a Set via its functor, its type will carry the witness of the element’s comparator. That is why StringIntTupleSet and StringIntTupleSetofSet do not share the same witness–the comparison function is lifted to work on sets for the second module. It isn’t useful that they share the same witness anyway, they’re entirely different functions even if just considering their type alone (check each module’s Elt.comparator).