A type puzzle with permissions.

[Drup]

Here is a nice puzzle for type apprentices: Figure out a signature of M so that this works

module rec M : sig
  type +'a cap
  type r = [`R]
  type w = [`W]
  val r : r cap
  val rw : 'any cap

  type +'a env
  val create : 'a cap -> 'a env

  val read : _ env -> int
  val write : w env -> int -> unit

  type +'a txn
  val txn : ?c:'a cap -> 'a env -> ('a txn -> 'r) -> 'r
  val readT : _ txn -> int
  val writeT : w txn -> int -> unit

end = struct

  type r = M.r
  type w = M.w

  type _ cap = C
  let r = C
  let rw = C

  type _ env = E
  let create C = E

  let read E = 1
  let write E _ = ()
   
  type _ txn = T
  let txn ?c:_ E f = f T
  let readT T = 1
  let writeT T _ = ()
end
open M
open M


let envr = create r
let envw = create rw

let i = read envr
let i2 = read envw

let () = write envw 2
let () = write envr 1 (* MUST FAIL *)

let _ = txn envw @@ fun t -> readT t
let _ = txn envw @@ fun t -> writeT t

let _ = txn envr @@ fun t -> readT t
let _ = txn envr @@ fun t -> writeT t (* MUST FAIL *)

let _ = txn ~c:r envw @@ fun t -> readT t
let _ = txn ~c:r envw @@ fun t -> writeT t (* MUST FAIL *)

The current version works, but as the downside that this doesn't:

let f env =
  let i = txn ~c:r env @@ fun t -> readT t in
  write env i

[madroach]

That's why I use permission types of [`R] and [`R | `W], because the former is a subtype of the latter:

let f env =
  let i = txn ~c:r (env : [> `R | `W] env : > [`R ] env) @@ fun t -> readT t in
  write env i

[Drup]

@madroach Except you have to use a type cast for this to work, even for txn ~c:r envw @@ fun t -> readT t, which is extremely user-hostile.

[madroach]

It certainly is. You already suggested to remove the phantom type from Env.t. The only reason I see to keep it is consistency. The only other way to palliate this issue I can think of is good documentation… I don't mind either way of tackling this issue.

[madroach]

This can be closed?

[Drup]

Let's keep it open, if someone can think of something nice :)