Explicitly polymorphic function inside a universally quantified record field (e.g., an effect handler)?

Learning
, ,
1

How do I define an explicitly polymorphic function inside a universally quantified record field, e.g., inside an effect handler?

Here is a MWE:

open Effect
open Effect.Deep

type _ Effect.t += Eff : ('a -> 'a) t

let rec handler =
  (* let tricky : 'b. 'b -> 'b = fun v -> try_with Fun.id v handler in (* <-- Does not work here... *) *)
  {
    effc =
      (fun (type a) (eff : a t) ->
        (* let tricky : 'b. 'b -> 'b = fun v -> try_with Fun.id v handler in (* <-- ...nor here *) *)
        match eff with
        | Eff -> Some (fun (k : (a, _) continuation) -> continue k tricky)
        | _ -> None);
  }
(* But the following works: *)
and tricky : 'b. 'b -> 'b = fun v -> try_with Fun.id v handler

let comp () =
  let id = perform Eff in
  id ()

let () = try_with comp () handler

With tricky inside the record field, I get an error

10 |         let tricky : 'b. 'b -> 'b = fun v -> try_with Fun.id v handler in
                                         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This definition has type 'b -> 'b which is less general than
         'b0. 'b0 -> 'b0

but when I take it out of the handler definition, the code type-checks.
I also tried wrapping tricky as a universally quantified object method, but it didn’t work as well.

My guess is that there is a problem unifying a monomorphized(?) tricky inside continue k tricky with the explicitly polymorphic definition inside handler.

  1. What is the exact cause of the issue of defining tricky inside handler? I read Chapter 6 and Chapter 7 of the OCaml manual multiple times without much success.
  2. Is my workaround the best solution? Is there a way to put tricky in handler and satisfy the type-checker?

Thank you.

2

I suspect that the issue is that handler has a non-polymorphic type inside its own definition, but a polymorphic one outside.
Can you try adding an annotation let rec handler : 'a . 'a effect_handler and see if it changes anything ?

1 Like
3

This is not an effect returning a polymorphic function, it’s an effect returning a monomorphic function at an existential type.
Maybe you want

type poly_fun = { f : 'a. 'a -> 'a }
type _ Effect.t += Eff : poly_fun t

?

IDK if that helps your compilation issues.

1 Like
4

Yes, it works like charm! So a value needs to be explicitly polymorphic in order to have some other polymorphic value type-check…

5

Thank you for correcting that type _ Effect.t += Eff : ('a -> 'a) t is not a function returning a polymorphic function, you are correct indeed!

6

So here is the correct code reflecting the comments from @vlaviron and @SkySkimmer:

open Effect
open Effect.Deep

type poly_fun = { f : 'a. 'a -> 'a }
type _ Effect.t += Eff : poly_fun t

let rec handler : 'a. 'a effect_handler =
  {
    effc =
      (fun (type a) (eff : a t) ->
        match eff with
        | Eff ->
            Some
              (fun (k : (a, _) continuation) ->
                continue k { f = (fun v -> try_with Fun.id v handler) })
        | _ -> None);
  }

let comp () =
  let id = perform Eff in
  id.f ()

let () = try_with comp () handler

Thanks again!

7

In this case, the definition of tricky depends on handler:

let tricky : 'b. 'b -> 'b = fun v -> try_with Fun.id v handler

If you assume that handler has type alpha effect_handler for some alpha, then tricky has type alpha -> alpha. You cannot generalize this to a fully polymorphic type because the alpha comes from outside the definition of tricky. This is more or less what happens if you let the type-checker infer the type of handler.
But if you know that handler has type 'a. 'a effect_handler, then the definition of tricky gets a type that is still something like alpha -> alpha, but with an alpha that was created during type inference of tricky, so it can be generalized to 'b. 'b -> 'b.

I think that the section of the manual on polymorphic recursion (here) is the most relevant to your case, although this is the first time I’ve seen a need for polymorphic recursion annotations on non-functional values.

1 Like