But…Eio is low-level with an added capabilities layer on top 
eg Low_level (eio_linux.Eio_linux.Low_level)
The Eio main library is a ‘frontend’ on top of each of the platform backends. It should be possible to create alternatives frontends which don’t use capabilities. Right?
Can’t users that don’t want to use capabilities just circumvent them, e.g. by putting env in a global variable, so that having capabilities in Eio actually causes less fragmentation?
| Eio uses capabilities | Eio does not use capabilities | |
|---|---|---|
| User wants to use capabilities | ok | user has to rewrite (or at least carefully read) all of Eio |
| User does not want to use capabilities | user easily circumvents capabilities | ok |
One could even have a wrapper Unsafe_eio (maybe with a slightly less scary name) that handles storing the env in some global variable and passing it to all function, so that functions in Unsafe_eio are exactly those of Eio without the capability arguments. That’d probably be useful for people that want to transition from Lwt.
Maybe the concerns have been addressed and there’s viable workarounds. Then all we need to do is communicate that clearly. (This is still one of the threads that rank high when searching for Eio, since there’s been a lot of discussion.) This is what I would like to understand fully.
I think it would have been nice for a survey to have preceded Eio’s design, to see if people are interested in capabilities in the first place. Instead, what was marketed as the new default choice for concurrency in Ocaml 5.0 is causing fragmentation, and may cause people to just stick with lwt.
EDIT: It would be nice to have a survey now as well for people who adopted Eio. I get the sense that many of them are just bypassing capabilities and don’t want to mess with them.
Hey @sabine,
I thought I would add my own experience as a long-time user of Eio and regular(ish) contributor.
Eio’s capabilities can be used for reasoning about code (e.g. this function takes a Eio.Net.t it must want to talk/listen to the world). But in Eio, the Eio.Net.t is used to talk/listen to the outside world. I think this is where the line begins to blur for whether this is something for formal verification or for everyday users.
In some ways, this is great, it makes it much easier to mock certain interfaces and not have to do any horrible injection of code. For example, in Obuilder the function for executing processes is a reference so it can be changed in the unit tests. With Eio, you would provide a different Eio.Process.mgr at the top which will have been threaded through anyway. In fact you could do this to any of the interfaces you like for any Eio library which is pretty powerful! I’ve been toying with a container-based processing library for sandboxed execs – if it provides the interface then any Eio library that uses Eio.Process.run will get sandboxed execution for free, potentially with no changes to the library required.
The pain point for me is that the types are fairly cumbersome. Trying to create an http client?
type t = {
buffer_size : int;
cache : Cache.t;
net : 'a Eio.Net.t;
};;
Error: A type variable is unbound in this type declaration.
In field net: ([> [> `Generic ] Eio.Net.ty ] as 'a) Eio.Net.t
the variable 'a is unbound
If I go and look at the Eio.Net interface, it’s a bit… polymorphic variant soup. Which I think is a real shame as the actual interface if you get far enough is exceedingly well-designed in my opinion.
Do I want all that flexibility? Maybe. Maybe not. I just wanted to show that I don’t think the overhead is that much and maybe the rewards are worth it (I’m not saying I agree, more trying to help by providing more information).
IIUC, I haven’t seen a single library that uses Eio bypass capabilities.
Yes. It is very possible and not too difficult to build a library using the low level interfaces (as I posted about above: Monadic Library for Eio Capabilities? - #6 by patricoferris). You can see in the connect example no env is being accessed. You could go one step further than that example and just copy the Eio API exactly and drop the various capabilities. Eio has done a lot of the work of writing the C stubs and logic for handling IO for Unix-y systems and all of this can be reused without capabilities. It may be some work, as is the case in eio, to bring them together as a portable abstraction though – which is a fine thing to disagree with. Eio exposes the entire complexity of the various interfaces to users if they choose a specific platform (e.g. Eio_linux).
In my mind, capabilities are similar to types, in that they are tools to enforce invariants, and the Unsafe_eio wrapper I described corresponds to a wrapper Untyped_mylib that removes types from the interface of a typed library Mylib, e.g. just replacing all types by a dynamic type such as TypeScript’s any. In both case, for the user not interested in the invariants, not much would be gained by rewriting the library without the invariant-enforcing tool: a few function would pass around one less argument for Unsafe_eio, and a few dynamic type checks of inputs would be postponed from the entrance into the library to actual uses for Untyped_mylib. In fact, having the invariants checked in the library reduces the amount of bugs this user could be subject to, without requiring any knowledge about the invariant-enforcing tool since they are hidden by the wrapper.
I fully agree that we should strive for modular, additive, and opt-in whenever possible, but my impression is that for a library to provide opt-in invariant-enforcement without duplicating code, it has to be written in an invariant-enforcing way, with a wrapper to allow hiding invariant-related information.
(I also believe that the wrapper could be made as modular as the invariant-enforcing library, though for the capability-removing wrapper that might require a bit of thought, and some cooperation from the invariant-enforcing library)
I don’t know that it has to be ‘novel’ or ‘interesting’ or made up of little Lego pieces. It’s a concurrency library, every modern language has some form of this. OCaml has several. Building on top of Eio seems pretty reasonable to me. More importantly, it seems like it would preserve ecosystem cohesion. Everyone would agree on the types. Depending on the top Eio frontend layer, which is cross-platform and not particularly heavyweight, doesn’t seem like a big deal to me.
Wasn’t that mostly because people wanted a multicore concurrency library without a capabilities system? If an Eio frontend without capabilities had existed from the beginning, would those people still have written their own schedulers?
This is a nice consequence of the capabilities design choices and I can see how that could in some situations be useful.
Such type errors indeed look a little complex (as most errors around polymorphic variants do). Is it really necessary/useful to have polymorphic variants here?
Do you think there’s a reasonable way the types could be changed to make the errors more approachable?
I don’t have an answer to this question but I find it’s the main pain point in Eio. And my problem is not even so much the type error message, but it’s the undocumented aspect of the library. There is a policy language embedded (EDSL) in the OCaml type language and it’s not clear, to me, how this embedding is done.
I will try to develop my thought. I see two distinct points in the use of capabilities:
First, let see what is a capability. Suppose you have a function foo : bytes -> .... Since it takes a byte as an argument ,foo can do anything it wants with this bytes and uses any function in the Bytes module. The purpose of a capability system is to restrict what foo can do with its bytes argument: it’s an access control policy system. So a capability is in fact a pair (authority, resource), hence the aphorism “don’t separate designation from authority”. Here resource denotes a value of the language (say a bytes) and authority is a set of functions that you can use on your resource (say a subpart of the module Bytes). But, since the authority part of the capability is limiting the right you get on the resource and you want to avoid privilege escalation, you have to hide this pair behind an existential such that you can’t project the resource outside the pair in order to use it with any kind of method. In other words a capability, seen as a programming value, is an object (as in Object Oriented Programming).
That’s why:
In Eio, capabilities are represented as object (as in OOP) but it’s not the only way to do this. For instance, I don’t find that @talex5 is fair with Haskell in his Lambda capabilities blog post. In Haskell, if you want to write code in this style you just have to constraint each safety critical resource by a type class, and to audit such code: just look at the type classes used.
More generally if you want to write code in a object-capabilities idiom in language such as Haskell, Rust or Golang, you could follow these advises:
I would say that most (consuming) generic codes in those language are already written in this style. The capability idiom only affect the way safety critical resource are produced: they have to come with a certificate (an authority) limiting the right you have on the resource. I would add that this idiom can’t be safely practice in Golang since a capability consumer can still match on the resource type and gain privilege escalation.
The comparison to these languages leads to my second point: the policy access language. In those languages they will not use something really new, and the error message will be common. But here, with Eio, we have to learn the object type language (we could have use the module type one) and there is also polymorphic variant? Why? What do they mean? How do we interpret the policy rules on a resource from the type of a capability? I did not find where it is documented and explained. To me it’s the most important part of the feature (and not the syntactic impact on code): since we are encoding policy rules in our code, how do we write and read them?
I think all of this shows that this is a layer of complexity we didn’t sign up for. As OCaml users, we just want a working and appealing concurrency solution – one that tempts us to give up lwt. OCaml’s type system isn’t powerful enough to manage this additional baggage without bogging users down in complexity. This isn’t how you create community consensus.
Indeed, Eio is far more than just a library for concurrency/parallelism. Furthermore, even if I find the idea of capabilities very interesting (that’s a notion and a conception of security I learned from Eio), it’s not the only way to solve safety problem. For instance, @dinosaure who writes unikernel can do this by restricting the number of system call allowed by his code, and maybe that’s why he wrote his own effect based scheduler.
OCaml type system can do a lot, but it’s not sure any user wants to pay that price just to have more safety control on their code. For instance, IIRC @c-cube wrote a simpler version of access control with [R|W] phantom type on bytes but I guess he stopped using it. And he also wrote his own effect-based scheduler.
The rest of this comment is more for people interested by philosophy of law and how it relates to object-capabilities system. I mostly thinking out loud since I only start reading about capabilities last week but I’ve been reading Kant’s philosophy for more than 25 years.
Since capabilities system deal with the right some code have regarding some resources, It must have some analogy with how the law works among human beings, and indeed it has. First of all, when I said that Curry-Howard was a particular case of a more general principle (not only use to study the analogy between computation and mathematical proof) I was serious. Let’s look at what Kant said about the formal structure of a State (his philosophy of law can be seen as a typing theory of roman law):
In other words, a State is formally structure like an Aristotelian syllogism (this is due to the formal structure of human mind: reason, understanding and the faculty of judgment, structure that we project in the constitution of our States).
That’s exactly what we got with a capability:
and that’s what I explained when I draw the correspondence between type class/trait system and Aristotelian syllogistic. The purpose of the authority is to rule out some uses of the resource, and the purpose of the system is to enforced the law. It can do it absolutely a priori if it is encoded in the static type system (a world with precogs à la Minority Report, system that will be fundamentally despotic if applied to human beings).
For the record, Kant also used this analogy in his famous Perpetual Peace to describe the distinction between a representative and a despotic constitution.
and in the french version I have, there is this additional remark in parentheses:
He also made an interesting use of syllogistic in an article about copyright (with a problem about concurrency), but I only know a french version freely accessible; De l’illégitimité de la contrefaçon des livres.
FWIW, I find this theory of 3 powers way obsolete, and clinging to it one of the main reasons for the rapid rise of all sorts of assholes. (You know who I mean.) The only civilized States (ahem) which still retain even the most basic stability are unitary parliamentary systems where the executive is a mere extension of the legislative.
–
Ian
It can’t be obsolete, that’s how human mind is formally structure (“Know thyself” was Socrates’ motto)
And you contradict yourself:
So there is still an executive and a legislative power. What your describe is the form of the government which can be republican or despotic.
But I don’t really understand what you mean by “a mere extension”? If the legislative executes (as a mere extension) the law he gave to himself, for sure it’s a despotic constitution, and it will indeed be easy for the head of State to get rid of those he considers to be asshole. But maybe you just had in mind parliamentary system that still relies on the triadic theory of state constitution and are republican.
BTW, I know that Gödel claimed to have found a inner contradiction in the constitution od United States, known as Gödel’s loophole, that allowed it to be transformed into a dictatorship, but nobody know what it was.
To stop digressing and return to Eio, there are two extreme cases in the family of authorities: the asbence of authority and the absence of right on the resource (think of interface {} in Golang). The former is the equivalent of Obj.magic and allow to bypass the capabilities system to acquire any right on a resource, that’s what @talex5 describes at the end of his blog post with thread-local storage.
As far as I can tell, it ends up mostly being a design trade-off. I think using objects is marginally better in terms of the error message, but it is still a little confusing and with the added downside that objects are less used in OCaml in general so there is less examples/docs in the wild about them. For example, if you switch back to an old enough Eio you get the same issue:
type t = {
src : Eio.Flow.source;
}
let of_source x = {
src = x;
}
Results in
Values do not match:
val of_source : Eio.Flow.source -> t
is not included
val of_source : #Eio.Flow.source -> t
The type Eio.Flow.source -> t is not compatible with the type #Eio.Flow.source -> t
Type
Eio.Flow.source =
< probe : 'a. 'a Eio.Generic.ty -> 'a option;
read_into : Cstruct.t -> int;
read_methods : Eio.Flow.read_method list >
is not compatible with type
#Eio.Flow.source as 'b =
< probe : 'a. 'a Eio.Generic.ty -> 'a option;
read_into : Cstruct.t -> int;
read_methods : Eio.Flow.read_method list; .. >
Type < > is not compatible with type 'b
This problem goes away if you no longer need subtyping – but (afaik) you either need the object system or polymorphic variants to have subtyping in OCaml. So the question really becomes is all this subtyping necessary?
I think there are two conflicting design decisions in terms of the use of subtyping in Eio (setting aside whether you do this with objects or polymorphic variants) and that is code reuse. For example, if I open a network connection I can pass the socket directly to Eio.Flow.copy_string. That’s becauses files, sockets, stdout etc. are all “flows”. This is really nice, however, I don’t think this is particularly apparent from the types themselves. For example, here is how you connect to a socket:
val connect :
sw:Switch.t ->
[> 'tag ty ] t ->
Sockaddr.stream ->
'tag stream_socket_ty Std.r
Compare this to perhaps a more conventional connect:
val connect :
sw:Switch.t ->
Sockaddr.stream ->
stream_socket
A newcomer doesn’t need to ask:
[> ...] mean?'tag variable?ty mean?Std.r?Then the user most also work out that 'tag stream_socket_ty Std.r will just work with Eio.Flow.copy_string. Let’s take a look at Eio.Flow.copy_string.
val copy_string : string -> _ sink -> unit
A new user needs to make the link between 'tag stream_socket_ty Std.r and _ sink. I think this is a pretty big ask. I think this is a big ask even for seasoned OCaml developers (it ultimately ends up looking at this polymorphic variant).
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.
The capabilities having this subtyping is also a little hard to remove at this point. In questions (2) I asked “what is the 'tag” variable. This is used to provide backend specific details via the capability. For example, the standard environment provided by the Eio_unix backend tags the network capability with the 'Unix tag which means you can safely use those unix-y sockets with functions like send_msg alongside anything in the normal Eio.Net module
Hopefully this helps explain some of the design decisions, use of subtyping and capabilities in Eio.
I think that subtyping is an important features of capabilities, but what we really want is subtyping between authorities (and we get it with subtyping in the module system).
I don’t consider myself as a developper, the main thing I do with OCaml is to torture its type system, and sure it was (and still is in some way) a big ask. After following some links, I ended on this documentation page on resources with this definition:
type -'tags t = T : ('t * ('t, 'tags) handler) -> 'tags t
So I suppose this is the definition of a capacity : a pair of (resource, authorities) packed behind an existential. Here the 'tags phantom type seems to encode what we can do with the resource. It is contravariant because we’re using polymorphic variant, so a disjunction should be interpreted as a conjunction of authority ([read|write] means that we can read and write on our resource, as @c-cube has done in one of his library).
But with such a copy_string interface:
val copy_string : (module Sink with type t = 'sink) -> string -> 'sink -> unit
(* or shorter *)
val copy_string : (module S : Sink) -> string -> S.t -> unit
can’t we get rid of polymorphic variant tags ? Isn’t this tags only here to track subtyping between the handlers part of the -'tags t type?
The idea with capabilities is to replace a monomorphic code with a polymorphic one (it is polymorphic in 'sink in the previous signature). That’s why it’s easy to mock (it is polymorphic) and safe (thanks to theorem for free à la Wadler, we know this code can only use the authorities defined by the Sink signature). In order to stay close to the orginal monoprhic code, Eio packs the module and the value together in an object-like value (an existential GADT): this way we still get one argument, and not two (the module and the resource). But, doing so, we lose the ability to directly do subtyping on the module-authority part of the capability, hence we have to introduce polymorphic variant.
If find just a little bit awkard to introduce polymorphic variant to encode in the type system a subtyping relationship that it already knows (subtyping between module) just because we have unnecessarily hidden it (behind an existential): the existential is not necessary from a consumer point of view, the safety of capabilities comes from the theorem for free part of the polymorphic code.
Do you know why they replace object by polymorphic variant? In the documentation of the Resource module, it is stated:
I could plead guilty to not liking objects (because they’re rarely the kind of type I need), but I find that the use of polymorphic variant is far more confusing for this use case.
I think I finally find what I was searching in the documentation but, honestly, I did the bad experience to feel like Asterix facing “The Place that Sends you Mad” in his twelves tasks. Was it design by french administration?
My main concern was: how is written the policy access language on resources? It appears that it is indeed the module type language. But to find the policy access rules, you first have to understand it is hidden under a Pi submodule. For instance, in the Eio.Flow.Pi you find this module type signature:
module type SINK = struct
type t
val single_write : t -> Cstruct.t list -> int
val copy : t -> src: _ source -> unit
end
And, as far as I understand, it is the method that should satisfied a _ sink. But it would have been clearer if the row-type variable of sink was a row-type variable of an object class and not one of a polymorphic variant. We could do so by maintaining the signature language to describe policy access.
Now, suppose you want to define your own sink resource, and not only use the ones built in Eio, you first have to implements the above SINK signature. Then you could use the Eio.Flow.Pi.sink function:
val sink : (module SINK with type t = 't) -> ('t, sink_ty) Resource.handler
and finally, equipped with this handler, all you have to do is package it correctly with a resource using the Resource.T constructor:
type -'tags t = T : ('t * ('t, 'tags) handler) -> 'tags t
I do not have difficulties to answer your four questions (but I’m not a newcomer, I’m used with type trickery and I know subtyping and row polymorphism), but I still wonder why they used a polymorphic variant 'tags type (which should have been named 'traits, since it seemed to be used to implement a kind of traits system in OCaml).
First of all, the [> ...] despite its appearance is in fact a polymorphic type (hence the error message). Let stay with the _ sink resources. A sink provide two traits : write and flow, and that’s what states the ty suffixed type (documentation):
type sink_ty = [` W | `Flow]
and then you have the definition of the row-polymorphic sink type:
type 'a sink = ([> sink_ty] as 'a) Std.r
The [> ..] indeed defines a family of types (hence the polymorphism): it is the family of all supertypes of [sink_ty], and when you get one such supertype you give it the type variable name 'a. It may be clearer with this naming scheme:
type 'kind sink = ([> sink_ty] as 'kind) Std.r
where 'kind is the type of the kind of sink you got, for instance a two_way_ty one. Basically, a _ sink value claims implementing the sink_ ty traits and maybe more (the maybe more is the source of the row type variable). It is the equivalent of the <sink; ..> object type that states that you must implements the methods of the sink object and maybe more (hence the ellipsis ..). If you use OCaml classes, the type #my_class is an abbreviation for the row-polymorphic <my_class; .. > object type. And it seems that’s what used Eio before.
Now, you may wonder why using row-polymorphism?[1] It is for subtyping (a core feature of capabilities system: the principle is to delegate some of the rights you own on a resource, but not necessarily all your rights, hence you must have subtyping) and convenience: without row-polymorphism you have to explicitly upcast your values.
Suppose you have a two_way (a supertype of sink) value v : _ two_way then you can use copy_string directly:
copy_string "OCaml" v
without such polymorphism you will have to explicitly cast your value:
copy_string "OCaml" (v :> sink)
There is still something that I can’t explain to myself: why using polymorphic variant and not object? With object we already have a type hierarchy (objects understand subtyping) and here we have to mimic this hierarchy by creating a mirror of it (contravariantly) in the polymorphic variant world. The Resource module implements its own dynamic method dispatch with these two functions:
val get : ('t, 'tags) handler -> ('t, 'impl, 'tags) pi -> 'impl
val get_opt : ('t, _) handler -> ('t, 'impl, _) pi -> 'impl option
So why doing by hand what we have for free with objects? What are the benefits of all the type trickery implemented in the Resource module? I’m pretty sure that no newcomers (even most OCaml programmers not used with advanced uses of type system) can understand it, and yet it’s the heart of the whole capabilities system. In fact, a Std.r(that is in fact a Resource.t) is an existential GADT type equivalent to an object type. Usually I don’t like objects because I then lost access to the packed value (the one of type 't in the GADT) but here, it’s a feature of a capabilities system to hide the resource in order to avoid privilege escalation.
[1]: The use of first-class module to avoid row-polymorphism seems difficult to practice since methods of resources may consume others resources, resource may contain resources and so on.
I respond to myself. After some reflexion, I fear that the security model of Eio is broken by the dynamic dispatch as exposed by the Resource module.
let foo (src : _ Flow.source) =
let (Resource.T (t, ops)) = src in
match Resource.get_opt ops Sink with
| Some (module M) -> (* I gain write access to my source *)
| None -> (* everything is fine)
Normally, if I pass a _ Flow.two_way to fooit should not be allowed to write to it, but I will fall in the Some branch and foo has gained privilege it should not have.
Eio indeed currently favors that particular convenience at call site. However, doesn’t it come with the downside that any type that contains a resource must have a type parameter? It’s something I recall struggling with when discovering Eio (“why is the Path.t type parametrized?”).
I’m unsure how important is the convenient casting in practice. Are folks using this a lot?
Another possibility would be to hide the kind, existentially:
type sink = Sink : ([> sink_ty] as 'kind) Std.r -> sink [@@unboxed]
The cast may be a little more verbose when needed, but that hides the complexity of the row parameter in most cases. Kind of a take on “If all you ever do is manipulate pathes with the Path API, why should you care about row-polymorphism?”. I’d be interested to learn more about the cons of this approach. Does it work at all in practice?
Hm, I never thought of that. Interesting!
I think my reluctance with objects would be that I’d find it hard to be convinced that there is no hidden bits of mutable state (e.g. private properties) somewhere. Manipulating the module language feels cleaner in that respect, as it should be clear to the user that no access to private top level reference is expected.
I wonder if you can go back to manipulating Objects for the lookup and typing parts of things, but still continue to using module signatures for the actual functionality. Something like this hybrid approach:
module type Doublable = sig
type t
val double : t -> t
end
module type Repeatable = sig
type t
val repeat : t -> t
end
let double (type a) (o : < d : (module Doublable with type t = a) ; .. >) a =
let module D = (val o#d) in
D.double a
;;
let repeat (type a) (o : < r : (module Repeatable with type t = a) ; .. >) a =
let module R = (val o#r) in
R.repeat a
;;
let quadruple (type a) (o : < d : (module Doublable with type t = a) ; .. >) a =
let module D = (val o#d) in
a |> D.double |> D.double
;;
let double_then_repeat
(type a)
(o :
< d : (module Doublable with type t = a)
; r : (module Repeatable with type t = a)
; .. >)
a
=
let module D = (val o#d) in
let module R = (val o#r) in
a |> D.double |> R.repeat
;;
module Doublable_int = struct
type t = int
let double x = x * 2
end
module Doublable_float = struct
type t = float
let double x = x *. 2.
end
let%expect_test "double" =
let o =
object
method d = (module Doublable_int : Doublable with type t = int)
end
in
print_s [%sexp (double o 3 : int)];
[%expect {| 6 |}];
let o =
object
method d = (module Doublable_float : Doublable with type t = float)
end
in
print_s [%sexp (double o 3. : float)];
[%expect {| 6 |}];
()
;;
module Versatile_int = struct
type t = int
let double x = x * 2
let repeat x = Int.of_string (Int.to_string x ^ Int.to_string x)
end
let%expect_test "repeat" =
let o =
object
method d = (module Versatile_int : Doublable with type t = int)
method r = (module Versatile_int : Repeatable with type t = int)
end
in
print_s [%sexp (repeat o 3 : int)];
[%expect {| 33 |}];
print_s [%sexp (double o 3 : int)];
[%expect {| 6 |}];
print_s [%sexp (quadruple o 3 : int)];
[%expect {| 12 |}];
print_s [%sexp (double_then_repeat o 3 : int)];
[%expect {| 66 |}];
()
;;