Hello,
I came across this term when I was following the new Java features(Screenshot is attached). It was a JVMLS session. Dreading to ask as my FP knowledge is minimal but even Java is introducing these. I also looked at some SO answers and collected these.
Recommended reading Types as Proof - Matt Diephouse. I was originally introduced to the witness pattern by my former colleague, Matt. In his article, Matt provides a deeper theoretical context for the witness pattern and showcases some excellent practical examples.
Witnesses - Will Crichton. In his article, Will demonstrates the witness pattern using Rust programming language. I also recommend checking out other articles from his series on Type-Driven APIs in Rust..
Theory: Proof-Carrying Data and Hearsay Arguments - Chiesa, Tromer Examples: Zupass - Github
I will try to make it simple to understand: a ‘witness’ is a runtime value (usually a constructor) whose only semantic purpose is to carry/drive type information. Your types encode invariants and the ability to construct these runtime values proves those invariants hold. That is the significance of it.
Suppose you want to write a sudo function which gives its callers the admin capability by looking up the user identifier on some allowlist (assuming authentication is already done, so let’s just focus on authorization), that capability can be considered an unforgeable witness which allows those callers to execute other privileged functions. The following is a sketch, not directly executable:
(* sudo.mli *)
(* the witnesses, cannot be constructed outside this module *)
type admin = private Admin (* or abstract or whatever works best for you *)
(* call [sudo username func] *)
val sudo : User.t -> (admin option -> ‘a) -> ‘a
and
(* sudo.ml *)
type admin = Admin
module Users = Set.Make(User)
let sudoers = ... (* to be updated or read from a config etc *)
let sudo user operation =
operation (if Users.mem user sudoers (* or check by group etc *)
then Some Admin else None)
privileged functions would then require the witnessSudo.admin:
val read_motd : unit -> string
val read_logs : Sudo.admin -> string list
I hope this example demystifies it. As you can see the only purpose of Admin (the witness) is to allow you to call functions expecting admin (the type). The functions do nothing with this token semantically. The token exists purely to make it a type error to call these functions if you can’t produce it.
This capability-style is just one use-case but I find it the simplest to explain vs more type-expressive features.
But I can’t relate your example and this. This seems to be a provision to provide different comparators.
I needed a Set of some data and I wanted to compare(PPX_Compare is used elsewhere ) and remove duplicates.
open Core
open Tinyest
module StringIntTuple = struct
module T = struct
type t = string * expr
[@@deriving_show]
let compare (x0, y0) (x1, y1) =
match String.compare x0 x1 with
0 -> compare_expr y0 y1
| c -> c
let t_of_sexp tuple = Tuple2.t_of_sexp String.t_of_sexp expr_of_sexp tuple
let sexp_of_t tuple = Tuple2.sexp_of_t String.sexp_of_t sexp_of_expr tuple
end
include T
include Comparable.Make(T)
end
module StringIntTupleSet = Set.Make(StringIntTuple )
module StringIntTupleSetofSet = Set.Make(StringIntTupleSet ) (* Need a list of Sets.Seems to need another 'comparator_witness` *)
let s = StringIntTupleSetofSet.of_list (set @set1)
The type of set is the following.
This needs the witness for purely comparison.
(StringIntTuple.t, StringIntTupleSet.Elt.comparator_witness) Set_intf.Set.t
list
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.
Comparison and serialization for a type, using a witness type to distinguish between comparison functions with different behavior.
type ('a, 'witness) t = private {
compare : 'a -> 'a -> int;
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).
If I understand this correctly, this means that this witness is a comparator implementation matching the type I want to compare. That was my interpretation too.
