Module Core_kernel.Perms
These types are intended to be used as phantom types encoding the permissions on a given type.
Basic Usage
Here's a hypothetical interface to an on-off switch which uses them:
open Perms.Export
module Switch : sig
type -'permissions t
val create : unit -> [< _ perms] t
val read : [> read] t -> [`On | `Off]
val write : [> write] t -> [`On | `Off] -> unit
end
Note that the permissions parameter must be contravariant -- you are allowed to forget that you have any particular permissions, but not give yourself new permissions.
You can now create different "views" of a switch. For example, in:
let read_write_s1 : read_write Switch.t = Switch.create ()
let read_only_s1 = (read_write_s1 :> read t)
read_write_s1
and read_only_s1
are physically equal, but calling Switch.write read_only_s1
is a type error, while Switch.write read_write_s1
is allowed.
Also note that this is a type error:
let s1 = Switch.create ()
let read_write_s1 = (s1 :> read_write t)
let immutable_s1 = (s1 :> immutable t)
which is good, since it would be incorrect if it were allowed. This is enforced by:
1. Having the permissions parameter be contravariant and the only way to create a t
be a function call. This causes the compiler to require that created t
s have a concrete type (due to the value restriction).
2. Ensuring that there is no type that has both read_write
and immutable
as subtypes. This is why the variants are `Who_can_write of Me.t
and `Who_can_write
of Nobody.t
rather than `I_can_write
and `Nobody_can_write
.
Note that, as a consequence of 1, exposing a global switch as in:
module Switch : sig
...
val global : [< _ perms] t
end
would be a mistake, since one library could annotate Switch.global
as an immutable Switch.t
, while another library writes to it.
More Usage Patterns
The standard usage pattern is as above:
- The permissions type parameter is contravariant with no constraints.
- The result of creation functions is a
t
with [< _ perms]
permissions. - Functions which take a
t
and access it in some way represent that access in the type.
The reason for having creation functions return a t
with [< _ perms]
permissions is to help give early warning if you create a t
with a nonsensical permission type that you wouldn't be able to use with the other functions in the module.
Ideally, this would be done with a constraint on the type in a usage pattern like this:
- The permissions type parameter is contravariant with constraint
[< _ perms]
. - The result of creation functions is a
t
with no constraint on the permissions. - Functions which take a
t
and access it in some way represent that access in the type.
Unfortunately, that doesn't work for us due to some quirks in the way constraints of this form are handled: In particular, they don't work well with [@@deriving sexp]
and they don't work well with included signatures. But you could try this usage pattern if you don't do either of those things.
For some types you may expect to always have read permissions, and it may therefore by annoying to keep rewriting [> read]
. In that case you may want to try this usage pattern:
- The permissions type parameter is contravariant with constraint
[> read]
. - The result of creation functions is a
t
with [< _ perms]
permissions. - Functions which take a
t
and access it in some way represent that access in the type, except that you don't have to specify read permissions.
However, the standard usage pattern is again preferred to this one: constraint
has lots of sharp edges, and putting [> read]
instead of _
in the types provides explicitness.