[Caml-list] More existential escapes (or possibly first class polymorphism)

["David Allsopp" <dra-news@metastack.com>]

Daniel's recent thread inspired to revisit a recent problem I'd had but had
given up on, with a most inelegant solution. Although what I have no is much
less inelegant, I'm wondering if it can be improved further by a trick or
some such which I can't spot.

I have a GADT containing keys where the type parameter denotes the value
type (my actual use case has many more constructors):

type _ token = Block : int -> string token
             | Role : string -> unit token

and I then want to be able to store these in a structure where I can look
them up by token value. So I define:

type binding = B : ('a token * 'a) -> token

to store a binding and:

type (_, _) eq = Eq : ('a, 'a) eq

let test_key (type r) (type s) (r : r token) (s : s token) : (r, s) eq
option =
  match (r, s) with
    (Role r, Role s) when r = s ->
      Some Eq
  | (Block r, Block s) when r = s ->
      Some Eq
  | _ ->
      None

and so I can define [find] in a manner very like Daniel's in
https://sympa.inria.fr/sympa/arc/caml-list/2015-03/msg00109.html

Given that this application is for a specific set of keys, rather than for a
universal type, I'd quite like to define [iter], which is where I've hit a
bit of inelegance:

let iter f script =
  let rec iter = function
    binding::script ->
      f binding;
      iter script
  | [] ->
      ()
  in
    iter script

but this means that the function passed needs to match on type binding,
which I'd prefer to be hidden:

let f = function
  B(Role role, ()) ->
    Printf.printf "Role %s\n%!" role
| B(Block n, code) ->
    Printf.printf "Block %d\n%!" n code

Is there a way to write [iter] such that it has signature [('a token -> 'a
-> unit) -> binding list -> unit]?

My closest attempt so far is to start with:

let iter f script =
  let rec iter = function
    B(key, binding)::script ->
      f key binding;
      iter script
  | [] ->
      ()
  in
    iter script

which obviously doesn't work because the type of [key] and [binding] in
[iter] escape their scope. Now, if my understanding is correct, the problem
here isn't so much that the existentials escape their scope, but that [f] is
monomorphic. So, if I define a record type:

type f = {f : 'a . 'a token -> 'a -> unit}

then I can alter the definition of iter to allow a polymorphic function to
be passed

let iter {f} script =
  ...

and I can get to a version of [iter] where the functions don't need to know
about the internals of type binding, but they do need to be passed wrapped
up as {f: foo}.

Is there some other wizardry on offer which can allow the polymorphic nature
of [f] to be inferred?


David