Re: Polymorphic variant + phantom type as a witness

[Gleb Alexeyev <gleb.alexeev@gmail.com>]

I've been pondering about something along these lines (if I understand 
it correctly, it seems to resemble what Jacques Garrigue proposed - 
passing a witness as extra argument to every effectful function).

I didn't think it through and haven't use it in practice, so I don't 
know whether it's usable, but anyway:

module type Permission = sig
   type 'a t
end

module Permission : Permission = struct
   type 'a t = unit
   (* here we need some means to cook new permissions - this is the part 
I didn't think through *)
end

module type SafeEffect = sig
   (* signatures of effectful primitives to be used instead of functions 
from Pervasives *)
   val print : [> `IO] Permission.t -> string -> unit
   val setref : [> `State] Permission.t -> 'a ref -> 'a -> unit
end

module SafeEffect : SafeEffect = struct
   (* implementation ignores the witness *)
   let print _ s = print_endline s
   let setref _ r x = r := x
end

module Example = struct
   module S = SafeEffect

   let use_io effect () = (S.print effect "bar"; 42)

   let global_n = ref 0

   let use_state effect () =
     S.setref effect global_n 42

   let use_both effect () =
     use_io effect ();
     use_state effect ()
end


The inferred signatures expose the effects:
     val use_io : [> `IO ] Permission.t -> unit -> int
     val use_state : [> `State ] Permission.t -> unit -> unit
     val use_both : [> `IO | `State ] Permission.t -> unit -> unit