I’m trying to model a set of permissions as polymorphic variants, used later as phantom type in signatures to control required permissions to call certain functions. In the snippet below Permissions module represents premissions and their constructing functions (which are supposed to verify if caller can have those, mocked with some token check), the Db module represents some database calls that we want to protect, and a set of functions at the top are “test cases”, the ones with _ok should not have type errors, while the ones with _fail should have type errors. Code is presented below. For this version the last test fails as polymorphic variants do not compose on their own (trying some coersions did not help either). If I return open polymorphic variants from Permissions functions, insufficient_permission_fail test actually passes and does not give type error, because polyvariants unify down to the value where expected set of constructors is listed. I wonder if this can be working with OCaml type system, my knowledge is definitely not enough to make it work
open Base
module Permissions : sig
type 'a t
val verify_read : string -> ([> `Read ] t, string) Result.t
val verify_write : string -> ([> `Write ] t, string) Result.t
val verify_delete : string -> ([> `Delete ] t, string) Result.t
val verify_all : ('a t, string) Result.t list -> ('a t, string) Result.t
end = struct
type 'a t = unit
let verify_read token = if String.(token = "foo") then Ok () else Error "invalid token"
let verify_write token = if String.(token = "bar") then Ok () else Error "invalid token"
let verify_delete token =
if String.(token = "baz") then Ok () else Error "invalid token"
;;
let verify_all results = Result.all_unit results
let can_write = Caml.Obj.magic
let can_also_write = Caml.Obj.magic
end
module Db : sig
val get_stuff : [ `Read ] Permissions.t -> string -> string
val put_stuff : [ `Read | `Write ] Permissions.t -> string -> string -> unit
end = struct
let get_stuff _perm key =
ignore key;
"stuff"
;;
let put_stuff _perm key value =
ignore key;
ignore value;
()
;;
end
let single_permission_ok () =
let open Result.Let_syntax in
let token = "whatever" in
let%bind permissions = Permissions.verify_read token in
Db.get_stuff permissions "my_key" |> ignore;
return ()
;;
let single_permission_mismatch_fail () =
let open Result.Let_syntax in
let token = "whatever" in
let%bind permissions = Permissions.verify_write token in
Db.get_stuff permissions "my_key" |> ignore;
return ()
;;
let insufficient_permission_fail () =
let open Result.Let_syntax in
let token = "whatever" in
let%bind permissions = Permissions.verify_read token in
Db.put_stuff permissions "my_key" "my_value";
return ()
;;
let multiple_permissions_ok () =
let open Result.Let_syntax in
let token = "whatever" in
let%bind permissions =
[ Permissions.verify_write token; Permissions.verify_read token ]
|> Permissions.verify_all
in
Db.put_stuff permissions "my_key" "my_value";
return ()
;;
In your code you return closed variants when creating permissions, and have fixed set of functions that create all required combinations.
I’m willing to create somthing more generic, as with, say, 4 permissions you’ll have a lot of such functions creating all required permutations, that’s why I tried returning open variants so that OCaml infers the type when I pass some list of validator functions, each returning one permission. But with open variants, they end up unifying with the type that is used as a guard in function, which was supposed to check if provided type has required constructors, not add them there
I don’t think you can compute the union of permissions at the type level, like your verify_all is trying to do. You can however request all permissions at once:
type 'a read_perm = Yes : [> `Read ] read_perm | No : [< `Write | `Delete] read_perm
type 'a write_perm = Yes : [> `Write ] write_perm | No : [< `Read | `Delete] write_perm
type 'a delete_perm = Yes : [> `Delete] delete_perm | No : [< `Read | `Write ] delete_perm
module Perm : sig
type 'a t constraint 'a = [< `Read | `Write | `Delete]
val verify : string -> r:'a read_perm -> w:'a write_perm -> d:'a delete_perm -> 'a t
end = struct
type 'a t = unit constraint 'a = [< `Read | `Write | `Delete]
let verify_read token (type a) (p : a read_perm) = match p with
| No -> ()
| Yes -> if token = "foo" then failwith "read"
let verify_write token (type a) (p : a write_perm) = match p with
| No -> ()
| Yes -> if token = "bar" then failwith "write"
let verify_delete token (type a) (p : a delete_perm) = match p with
| No -> ()
| Yes -> if token = "qux" then failwith "delete"
let verify token ~r ~w ~d =
verify_read token r ; verify_write token w ; verify_delete token d
end
(notice how negation is represented by listing all the positive cases… so while not exponential, it’s still quadratic to write this code.)
Usage yields the expected types:
let r__ = Perm.verify "x" ~r:Yes ~w:No ~d:No
let _w_ = Perm.verify "x" ~r:No ~w:Yes ~d:No
let __d = Perm.verify "x" ~r:No ~w:No ~d:Yes
let rw_ = Perm.verify "x" ~r:Yes ~w:Yes ~d:No
let r_d = Perm.verify "x" ~r:Yes ~w:No ~d:Yes
let _wd = Perm.verify "x" ~r:No ~w:Yes ~d:Yes
let rwd = Perm.verify "x" ~r:Yes ~w:Yes ~d:Yes
(*
val r__ : [ `Read ] Perm.t
val _w_ : [ `Write ] Perm.t
val __d : [ `Delete ] Perm.t
val rw_ : [ `Read | `Write ] Perm.t
val r_d : [ `Delete | `Read ] Perm.t
val _wd : [ `Delete | `Write ] Perm.t
val rwd : [ `Delete | `Read | `Write ] Perm.t
*)
Interestingly, it’s not possible to request no permissions at all!
let ___ = Perm.verify "x" ~r:No ~w:No ~d:No
(* Error: [...] These two variant types have no intersection *)
For completeness, functions which requires permissions should use an open type:
val get_stuff : [> `Read ] Perm.t -> string -> string
(* ^ at least the permission to read *)
edit: A less fancy alternative:
type yes = YES and no = NO
type 'a perm = Yes : yes perm | No : no perm
module Perm : sig
type 'a t
val verify : r:'r perm -> w:'w perm -> d:'d perm -> <read:'r; write:'w; delete:'d> t
end = struct
type 'a t = unit
let verify ~r ~w ~d = ()
end
let ___ = Perm.verify ~r:No ~w:No ~d:No
let r__ = Perm.verify ~r:Yes ~w:No ~d:No
let _w_ = Perm.verify ~r:No ~w:Yes ~d:No
let __d = Perm.verify ~r:No ~w:No ~d:Yes
let rw_ = Perm.verify ~r:Yes ~w:Yes ~d:No
let r_d = Perm.verify ~r:Yes ~w:No ~d:Yes
let _wd = Perm.verify ~r:No ~w:Yes ~d:Yes
let rwd = Perm.verify ~r:Yes ~w:Yes ~d:Yes
(*
val ___ : < delete : no; read : no; write : no > Perm.t
val r__ : < delete : no; read : yes; write : no > Perm.t
val _w_ : < delete : no; read : no; write : yes > Perm.t
val __d : < delete : yes; read : no; write : no > Perm.t
val rw_ : < delete : no; read : yes; write : yes > Perm.t
val r_d : < delete : yes; read : yes; write : no > Perm.t
val _wd : < delete : yes; read : no; write : yes > Perm.t
val rwd : < delete : yes; read : yes; write : yes > Perm.t
*)
(* resulting types are more verbose, but we can define short forms: *)
type read = <read:yes>
module Op : sig
val get_stuff : <read;..> Perm.t -> unit
end = struct
let get_stuff _ = ()
end
let () = Op.get_stuff rw_
Wow, thanks @art-w ! Looks like what I need. Fancy GADT magic, I’ll try to figure out how it works one day
I like the second “less fancy” option, it seems lightweight to write by hand, for the first one one would need some ppx probably to generate the boilerplate, but that seems doable.
Check out @octachron’s solution to a similar question I posed on StackOverflow. The idea is to use polymorphic variants to represent the on/off status of each permission, then wrap these inside an object phantom type where the method names represent the specific permissions. Adapting it for your use case could look something like:
type on = [`On]
type off = [`Off]
type any = [ on | off ]
type +'a t constraint 'a = < read: [< any ]; write: [< any ]; delete: [< any ] >
val get_user_count : < read:on; ..> t -> int
val delete_all_users : < delete:on; ..> t -> unit
As noted in the answer, this technique would be most suited to a small fixed set of permissions, as you seem to have here.
