Packing GADT constructors in iterable data structure

Learning
6

There are various methods of working with existential types. In the case of searching for the first S, string is a concrete type and so all you need is an annotation:

let rec first_s = function
  | [] -> None
  | Pack (S _ as s, f)::_ -> Some (s, (f : string -> bool))
  | _::rest -> first_s rest

It’s also possible to iterate over the contents of the packed. A function argument would usually leak the existential type and fail to compile, but we can avoid this by requiring the function to be polymorphic, which does not result in the type escaping:

type polymorphic_observe = {
  f : 'a. 'a t -> ('a -> bool) -> unit;
} [@@unboxed]

let iter f list =
  List.iter (function Pack (t, g) -> f.f t g) list

You can likewise define map, fold, etc. I find programming in this way to be clumsy and unpleasant, but it is possible.

4 Likes