I’m experimenting a little bit with effects (incl. the ad hoc syntax) and am stuck on the following example.
type _ eff += Wait : 'a list eff;;
type _ eff += Wait : 'a list eff
let append = fun l1 ->
let rec loop = function
| [] -> perform Wait
| x::xs -> x :: loop xs
in
fun l2 ->
try_with loop l1 { effc = fun Wait -> Some (fun k -> continue k l2) };;
Line 6, characters 36-77:
Error: This field value has type
'a list eff -> (('a list, 'c list) continuation -> 'c list) option
which is less general than
'b. 'b eff -> (('b, 'd) continuation -> 'd) option
However I don’t really see if and how I could make this example work?
I very much doubt you can make it work that way. Indeed, the effect handler needs to react to any kind of Wait request, be it of type int list, float list, etc. But the only thing it has at hand is the list l2, which at a given time has a single type. Obviously, as we can see your whole code, we know that the loop function can only perform Wait requests with the type of the list l1. But since the loop function is not annotated with the type of the effects it can raise, this piece of information is missing from the typechecker.
A possible way to solve the issue (not tested) is to declare the Wait effect inside the append function using a local module, so that its type is not arbitrary but directly tied to the type of l1. Said otherwise, there is no longer a single global Wait effect, there is a fresh Wait effect created every time append is called. (This does not seem like a good idea from an operational point of view, but who knows.)
let append (type a) (l1: a list) =
let open struct
type _ eff += Wait: a list eff
end in
let rec loop = function
| [] -> perform Wait
| x::xs -> x :: loop xs in
fun (l2: a list) ->
try_with loop l1 { effc =
fun (type b) (e: b Effect.t) ->
match e with
| Wait -> Some (fun (k : (b, _) continuation) -> continue k l2)
| _ -> None }
I am a bit surprised by the amount of type annotations I had to write. I guess this is an argument in favor of the native syntax, since it points the compiler toward the correct types:
let append (type a) (l1: a list) =
let open struct
type _ eff += Wait: a list eff
end in
let rec loop = function
| [] -> perform Wait
| x::xs -> x :: loop xs in
fun (l2: a list) ->
try loop l1 with effect Wait, k -> continue k l2
Anyway, in both cases, the important point is that I had to create a fresh effect Wait to be able to explicitly give it the same type as l1. (But I cannot explain why I also had to explicitly give the type of l2.)
Thanks! I had tried to tie l1’s and l2’s types but hadn’t thought of this way to also tie the type of Wait. Indeed, for the record, here is the type error when not explicitly specifying that of l2:
let append (type a) : a list -> _ -> a list = fun l1 l2 ->
let open struct
type _ eff += Wait: a list eff
end in
let rec loop = function
| [] -> perform Wait
| x::xs -> x :: loop xs in
try loop l1 with effect Wait, k -> continue k l2;;
Error: The value l2 has type 'a but an expression was expected of type a list
This instance of a list is ambiguous:
it would escape the scope of its equation
I’ve seen that pattern before and was curious about the runtime impact too. For example, CCHet in the containers-data library defines a new exception type for each map key instantiated (and exceptions are just a special case of extensible variants). I don’t recall seeing any performance or memory impacts with that, so maybe the compiler handles this case more intelligently than one would guess. Are there any maintainers who could comment?
At runtime, a local exception (or extensible type constructor) declaration boils down to the allocation of a heap-allocated block of size 1. In practice, this is unlikely to make any difference performance-wise.
This figure is a bit too optimistic. The block actually has size 2 because it also keeps track of the name of the effect / exception for tracing purpose. If you add to that the cost of the local module needed to store the effect (is it possible to do without a local module?), you end up with 5 memory words per effect. And it is not just a matter of memory consumption, you also have to take into account the runtime cost. Indeed, the allocation of a system-wide unique identifier for the effect / exception has to be thread-safe, which incurs a small but not negligible cost.