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: | 2008-07-04 (13:05) |
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