Monadic Library for Eio Capabilities?

Learning
67

You don’t need this existential GADT, it is equivalent to the simply defined type sink = [sink_ty] Std.r. The type that will indeed be used if we get rid of row-polymorphism to favor explicit casting at call site.

Sure you can. It was discussed in the topic A proper OCaml I/O layer.

Basically, with your Doublable signature:

module type Doublable = sig
  module type S = sig
    type t
    val double : t -> t
  end

  (* the super type of all doublable values *)
  type doublable

  (* a generic, and only real way to produce a doublable *)
  val make : (module D : S) -> D.t -> doublable

  module Top : S with type t = doublable

 (* then any generic methods on doublable go there *)

 val foo : (module D : S) -> D.t -> ...
 val bar : (module D : S) -> D.t -> ...
 val baz : (module D : S) -> D.t -> ...
end

And you can implements the doublable type with an object and even expose it publicly. To be honest, what I really miss in Eio API is this generic make constructor for all the kinds of resources it propose.

In fact when you do OOP, you systematically apply the generic functions foo, bar and baz with the same first class module, namely Top, the one that states that all doublable are doublable (a real truism, I know). And that’s what I usually dislike in OOP idiom: in order to use generically a value as doublable, you first have to upcast it in the supertype that represents the object, which most of the time is a complete non sense and an insult to human mind.

When you do subtyping between two objects types, it really amounts to do subtyping between their corresponding module signatures. That’s why I proposed the & module type operator, to be on par with the object type language. If you have two signatures S1 and S2 you will have <S1.top; S2.top> = <(S1&S2).top> (where the type top denotes the supertype of all values satisfying these signatures, seen as an OOP object and that Rust call a trait object).

I would qualify this as a fundamental security bug of the current Eio implementation: downcasting must be forbidden in a capability system, otherwise there is no more guaranty of any kind.

Edit: one thing that’s missing in OCaml is the possibility to use first-class module with classes (because they are indeed deeply related).

class doublable (module M : S with type t = 'a) (x : 'a) = object end;;
Error: Modules are not allowed in this pattern