Eio.Resource and Type-Safety

[mbarbin]

Hello Eio team,

I've been re-using the pattern from Eio.Resource in the provider project. Recently, I've spent some time trying to make the use of Obj.magic more robust in provider. You can see some of the discussions and efforts here.

During this process, I've encountered cases of invalid uses that lead to unfortunate results. I'm sharing one such case that is also applicable to Resource:

type ('a, 'impl, 'tag) Eio.Resource.pi += Trait : (unit, 'a, [ `A ]) Eio.Resource.pi

let a = (Trait : (unit, string, [ `A ]) Eio.Resource.pi)
let h = Eio.Resource.handler [ H (a, "hello") ]
let b = (Trait : (unit, int, [ `A ]) Eio.Resource.pi)

let%expect_test "crash" =
  let (i : int) = Eio.Resource.get h b in
  print_s [%sexp { is_int = (Obj.is_int (Obj.repr i) : bool) }];
  [%expect {| ((is_int false)) |}];
  ()
;;

I'm not sure if it is possible to address this issue. I'd be interested in discussions with the Eio team on this.

Thank you for your time and for Eio!

[Arogbonlo]

Hey @mbarbin

I think to address the type-safety issues with Eio.Resource and Obj.magic here, start by minimizing or eliminating Obj.magic whenever possible. This function bypasses OCaml’s strict type system, which can lead to unexpected runtime errors.
Also, redefine the types explicitly to ensure they match the expected type constraints.

[patricoferris]

Thanks @Arogbonlo for trying to help here, I think the use of the object module in this part of Eio is v. different to other places and necessary. The implementation could perhaps use a few comments because reading the code is pretty tricky (the API docs are good though).

[mbarbin]

Thanks @Arogbonlo that is sound advice. In this instance I've struggled in my attempts to remove the conceptually equivalent use of Obj.magic in my project, without success.

@patricoferris I also don't think it's possible to remove it without (perhaps invasive) changes to the exposed API. It would be sad if too many ergonomic aspects are lost in the process.

It's probably low priority given that cases like the one I shared only arise with invalid usage of the library. At any rate, I'll let you know if I find anything interesting. Thank you for looking into the issue.

[talex5]

Thanks @mbarbin, that's a problem, indeed!

Logically, a handler is a function like this:

  type ('t, 'tags) handler = { fn : 'impl. ('t, 'impl, 'tags) pi -> 'impl }

Then the magic shouldn't be needed. The array was intended to make it more efficient and ergonomic, but looks like it needs some revising!

Note that OCaml's object types solve this problem easily, so if you can use them without annoying people then that would be a better option.

(to keep the variance annotations you might need to do some magic on tags, but that should be safe since it's only a phantom parameter)

[mbarbin]

I can offer to have a look if you'd like since I'm already working on similar ideas for provider. No worries if you have other plans though, whatever makes most sense to you and the project. Thanks @talex5!

[talex5]

Please go ahead!

[mbarbin]

I was inspired by that famous TV show and decided to phone a friend on that one. This is joint work with @v-gb.

I propose to use this PR¹ as a preview. Please let me know what you think. I'd be happy to create a PR for Eio.Resource based on a similar approach. For Eio, it would seem we'd only need the equivalent of Provider.Trait.Create. We looked for ways to prevent segfaults by design, with or without Obj.magic in the code. This version was the only one we found that doesn't need the magic and keeps the ergonomics in check.

Footnotes

1. We encountered a scary dragon along the way, but luckily were able to return safe and sound. The underlying issue has been fixed by the compiler team. It is also not in the critical path for the changes. ↩

[mbarbin]

I started a draft following a similar approach.

I counted 22 Resource.pi extended constructors in the project.

• 17/22 were converted with the new Create functor
• 1/22 could be functorized
• 4/22 are giving me a hard time (I'm kinda stuck).

Details below:

Simple form

The 17/22 are of the simple form:

K : ('t, (module S with type t = 't), [> ty]) Resource.pi

They are compatible with the approach, and can be rewritten as:

module K : sig
  val pi : ('t, (module S with type t = 't), [> ty]) Resource.pi
end = Resource.Pi.Create (struct type 't iface = (module S with type t = 't) end)

Parametrized tags

The 5 remaining ones use another pattern. Consider lib_eio/net.ml/Network as an example:

Network : ('t, (module NETWORK with type t = 't and type tag = 'tag), [> 'tag ty]) Resource.pi

In this pattern, the signature has 2 types. Its second type is bound as a parameter of the last argument of pi (tag ty here).

I hadn't noticed this pattern before. I find it more tricky because the tags part of pi become more than a simple phantom type : if you do not tag your handler correctly, you are essentially writing unsafe code:

module type Trait = sig
  type t
  type a

  val get_a : t -> a
end

type ('a, 'impl, 'tag) Eio.Resource.pi +=
  | Trait :
      ( 't
      , (module Trait with type t = 't and type a = 'a)
      , [ `A of 'a ] )
        Eio.Resource.pi

let get_a (type tag) (Eio.Resource.T (t, ops) : [> `A of tag ] Eio.Resource.t) =
  let (module T) = Eio.Resource.get ops Trait in
  T.get_a t
;;

module Int_trait = struct
  type t = int
  type a = string

  let get_a = string_of_int
end

let h : (int, [> `A of int ]) Eio.Resource.handler =
  Eio.Resource.handler [ H (Trait, (module Int_trait)) ]
;;

let%expect_test "crash" =
  let (a : int) = get_a (T (42, h)) in
  print_s [%sexp { is_int = (Obj.is_int (Obj.repr a) : bool) }];
  [%expect {| ((is_int false)) |}]
;;

It looks like a potentially more concerning problem than the previous counter-example. All the more reasons for revising?

lib_eio/time.ml

• lib_eio/time.ml:
  • Clock

  type (_, _, _) Resource.pi +=
    | Clock : ('t, (module CLOCK with type t = 't and type time = 'time), [> 'time clock_ty]) Resource.pi

The type time ends up with 2 disjoint instances throughout the project, float and Mtime.t, so it is possible to functorize over it. I experimented with this idea here.

net & process

• lib_eio/net.ml:

  • Listening_socket
  • Network

• lib_eio/process.ml:

  • Process
  • Mgr

They are parametrized by [> Generic ] (which sometimes has [ Unix ]), so the parameter of the tag itself uses subtyping.

I don't know yet how to handle that part, and currently left it for future work. I am hoping this will not undermine the whole approach, but I am not confident.

[talex5]

Hmm, interesting.

I'm wondering about another possibility: what if we require users to provide a function (as above, but returning an option), and convert it to an array in Resource.handler by calling it once for each pi value.

I haven't tried it, but I think that would ensure that the values are sufficiently polymorphic.

It would mean that when defining a new API you'd have to list all the pi values, but would have the advantage of actually testing that they're all provided at handler definition time.

[mbarbin]

I'm wondering about another possibility: what if we require users to provide a function (as above, but returning an option), and convert it to an array in Resource.handler by calling it once for each pi value.

You may be ahead of me on this. I'm under the impression that the user provided pattern matching would only get you as far as the Create functor.

I am curious if you envision that this would make the compiler infer the type of the tags during handler creation. It's hard to know without trying, but my impression is that as long as the function to build a handler does not constrain the tags on its own, the API will still be subject to the sort of the counter-example number 2 (constructing a segfault by improperly casting the tags).

Such as in the current api:

val handler : 't binding list -> ('t, _) handler

I wonder if there is a construct in the language that could allow a unification of the tags while the bindings are joined (such as in a list, or pattern matching). Would using a object type instead of polymorphic variant in the tag phantom parameter give more power/flexibility?

The 2 remaining cases are essentially the moral equivalent of a parametrized OCaml class.

If the constrain for the parameter cannot be guaranteed via the tags, maybe a possible direction is to add more parameters to what's currently exposed:

val get : ('t, 'param, 'tags) handler -> ('t, 'param, 'impl, 'tags) pi -> 'impl

By the way, could you point me to an example in Eio for net and process that builds a handler that is not 'Unix. I couldn't find one (is it for compiling to javascript?). For example, lib_eio_posix.Process.Process_impl.tag = [ 'Generic | 'Unix ]. I'd like to better understand how the code makes use of this subtype for this tag parameter, for added context.

[mbarbin]

A little update on this. I continued to spend some time on this PR but I have nothing to show for it. I did try to thread through that extra 'param parameter I was mentioning in my previous message, and while it's possible to make progress in building things, this looks hm.. very complicated and verbose.

Another idea:

I was reading through the thread about capabilities on discuss, and wondered what things would look like under a different approach. This combines two ideas:

1. the first is to wrap the resource behind constructors so they can hide the existential row-polymorphism embedded in resources. Example of commits here: https://github.com/mbarbin/eio/tree/wrap-resource
2. once you have done that, you can replace the use of resource by a object type containing first class modules. Example of commit here: https://github.com/mbarbin/eio/tree/object-with-modules

Both these branches are very experimental, I just wanted to try and see if it was possible to get something to compile. I focused on just a few of the types to see what happens. CC @patricoferris from whom I read in the discuss thread:

How would this compare to an API with a to_flow for files and sockets? I’m leaning a little more towards something like that to help make some of the return types a little easier to use and document but it would be a huge breaking change and the fix is to add a lot of conversion functions.

and thought maybe something in that direction could at the same time, resolve the safety issue, and do some exploration along some of the pain points discussed in the thread. Very speculative / experimental things at this time, I have not much more to offer at this time. Thank you!

[mbarbin]

Edit: Another tentative approach that keeps the polymorphic convenience usage at call site without casting, and built on ocaml object, hopefully staying reasonably close to the current Eio. This is very on-going and exploratory: https://github.com/mbarbin/eio/tree/object-with-modules-exploratory and currently doesn't fully build yet. Perhaps that could serve as additional material to discuss if you want to have a meeting about this with the eio-devs. Happy end-of-year and talk soon.