Browse thread
Polymorphic variant as a witness?
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
| Date: | -- (:) |
| From: | Gleb Alexeyev <gleb.alexeev@g...> |
| Subject: | Re: Polymorphic variant + phantom type as a witness |
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