They have a simple example:

``````// A generator effect with one operation
effect yield<a>
fun yield( x : a ) : ()

// Traverse a list and yield the elements
fun traverse( xs : list<a> ) : yield<a> ()
match xs
Cons(x,xx) -> { yield(x); traverse(xx) }
Nil        -> ()

fun main() : console ()
with fun yield(i : int)
println("yielded " ++ i.show)
[1,2,3].traverse
``````

How to convert this into OCaml? My attempt:

``````open Effect
open Deep

type _ t += Yield : 'a -> 'a t

let yield x = ignore (perform (Yield x))

let rec traverse = function
| x :: xx ->
yield x;
traverse xx
| [] -> ()

let main () = try_with traverse [1; 2; 3] {
effc = fun (eff : int t) ->
match eff with
| Yield x ->
Some (fun k ->
Printf.printf "yielded %d\n%!" x;
continue k x)
| _ -> None
}

let () = main ()
``````

Yields an error:

``````dune exec ./e.exe
File "e.ml", lines 15-21, characters 9-15:
15 | .........fun (eff : int t) ->
16 |     match eff with
17 |     | Yield x ->
18 |       Some (fun k ->
19 |         Printf.printf "yielded %d\n%!" x;
20 |         continue k x)
21 |     | _ -> None
Error: This field value has type
int t -> ((int, unit) continuation -> unit) option
which is less general than
'b. 'b t -> (('b, 'a) continuation -> 'a) option
``````

Your attempt just needs a couple of tweaks:

``````type _ t += Yield : int -> unit t
``````

and:

``````Some (fun (k : (a, unit) continuation) ->
Printf.printf "yielded %d\n%!" x;
continue k ())
``````

(note that the type annotation is necessary).

Cheers,
Nicolas

Interesting, but itâ€™s not exactly the same, right The Koka yield effect can yield any value, not just int.

Thereâ€™s no problem yielding values of any type, but then you cannot simply use `Printf.printf` to print them

Cheers,
Nicolas

Right, my main problem is

``````with fun yield(i : int)
``````

vs

``````effc = fun (eff : int t) ->
match eff with
| Yield x ->
``````

In Koka you can narrow the type of the effect payload, but in OCaml you canâ€™tâ€¦I suppose unless you add some kind of runtime type description to the payload.

The koka `traverse` expresses in its type the constraint that it only uses `yield` on the type of the list elements.
Ocaml doesnâ€™t have typed effects so this constraint canâ€™t be expressed and you have to monomorphize.

Maybe you could try something with first class modules like the following but it gets kinda heavy and probably a bad idea

``````
module type Yielder = sig
type a
type _ Effect.t += Yield : a -> unit Effect.t
end

let mk_yield (type a) () = (module struct
type nonrec a = a
type _ Effect.t += Yield : a -> unit Effect.t
end : Yielder with type a = a)

let yield (type a) (y:(module Yielder with type a = a)) (x:a) : unit =
let module Y = (val y) in
Effect.perform (Y.Yield x)

let rec traverse y = function
| x :: xx ->
yield y x;
traverse y xx
| [] -> ()

let effc (type b) (y:(module Yielder with type a = int)) (eff:b Effect.t)
: ((b,unit) Effect.Deep.continuation -> unit) option =
let module Y = (val y) in
match eff with
| Y.Yield x ->
Some (fun k ->
Printf.printf "yielded %d\n%!" x;
Effect.Deep.continue k ())
| _ -> None

let main () =
let y = mk_yield () in
Effect.Deep.try_with (traverse y) [1; 2; 3] {
effc = fun eff -> effc y eff
}
``````
1 Like

Itâ€™s not a matter of narrowing types, itâ€™s a matter of the way effects are typed in Koka vs OCaml. This is the only meaningful difference in the two examples, as the rest is just translation.

If you trace down the type variable `a` in the Koka example, youâ€™ll see that at all times itâ€™s available everywhere thanks to the effect typeâ€¦ or in approximate OCaml 6? syntax:

``````effect 'a yield = Yield : 'a -> unit
val traverse : 'a list -['a yield]-> unit
``````

whereas OCamlâ€™s way of typing effects (using GADTs and extensible variants and only typing the declaration) disallows such connection between the type constructor and the data constructor to be made, and disallows a similar connection to be made on the `traverse` arrowâ€¦ in other words the `a` is existential and functions canâ€™t say much about the types of the effects they perform:

``````type 'ret Effect.t += Yield : 'a -> unit Effect.t
(* notice the difference in type variables 'ret and 'a *)
val traverse : 'a list -> unit
(* and notice the lack of a type equality between list element and the effect *)
``````

â€¦

Writing a handler for the Koka version is simple; the type of elements in the list is the same as the type of elements in the effect (we know that because `traverse` tells us that), and a specialized handler is even possible and can be type-checked because we have enough type infoâ€¦

``````val handler : (unit -['a yield]-> 'b) -> unit -> 'b
(fun () -> traverse [1; 2; 3]) : unit -[int yield]-> unit
``````

A handler for the OCaml version cannot assert such equalities, not with `traverse` written as it is.
Indeed, in OCaml you could do the following:

``````let rec traverse : int list -> unit = function
| [] -> ()
| x :: xs -> perform (Yield "I am not an int"); traverse xs
``````

To handle an existential, you canâ€™t make any assumptions about it except what it gives you to work with; an unconstrained existential is more-or-less useless. Itâ€™s not possible to â€śnarrowâ€ť it as youâ€™d expect.

â€¦

To cope with such difference, you need to at the very least pass the function which touches `'a` as another field, you may choose to use `printf` as the field, but the more specific you are, the less useful the dynamic nature of effect handlers becomes (that you can choose different behaviors for the same effect). I chose an ad-hoc constraint that there also exists a function capable of taking the existential variable and returning a string:

``````type _ Effect.t += Yield : { value : 'a; show : 'a -> string } -> unit Effect.t

let rec traverse : ('a -> string) -> 'a list -> unit
= ...
let main () =
...
| Yield {value; show} -> Some
(fun (k : ...) -> ... (show value); continue k ())
``````

that way, the handler can use the provided `show` field to convert the existential to a type it knows, and make use of it.

This is the minimal change, something more robust would be what @SkySkimmer beat me to writing, because it brings back the ability to talk about `a` outside of the effect declaration (at that cost youâ€™re seeing :P)

1 Like

Actually I feel writing it like this is a bit closer to Koka:

``````module Yield (A : sig type t end) = struct
type a = A.t
type _ Effect.t += Yield : a -> unit Effect.t
let perform x = Effect.perform (Yield x)
let handler h f x = Effect.Deep.try_with f x {
effc = fun (type a) (e : a Effect.t) : ((a,_) Effect.Deep.continuation -> _) option ->
match e with
| Yield x -> Some (fun k -> h x; Effect.Deep.continue k ())
| _ -> None
}
end
module type YieldT = sig
type a
val handler : (a -> unit) -> ('t -> 'u) -> 't -> 'u
val perform : a -> unit
end

let rec traverse (type a) (module Y : YieldT with type a = a) (xs : a list) : unit =
let rec go = function
| x :: xx -> Y.perform x; go xx
| [] -> ()
in
go xs

let main () =
let module Y = Yield(Int) in
Y.handler (fun i -> Printf.printf "yielded %d\n%!" i)
(traverse (module Y)) [1; 2; 3]
``````

EDIT: nevermind, extensible variants bit me.
I edited it to also handle properly not just typecheck. It looks less like Koka now. Ah well, canâ€™t have cute things :')

``````type t = ..
module Functor () = struct
type t += X
end

module A = Functor()
module B = Functor()

let test = match A.X with B.X -> true | _ -> false
(* test = false *)
``````
3 Likes

Nice! I think both you and SkySkimmer are saying the same thing, basically you have to monomorphize. `Yield(Int)` does the trick in this case.

Another take, with less modules: (edit: â€¦ on a second read of the topic, I had missed the very similar solution by @hyphenrf !)

``````open Effect.Deep

let with_yield (type x) handler fn =
let open struct
open Effect
type _ t += Yield : x -> unit t
let yield x = perform (Yield x)
type 'a k = ('a, unit) continuation
end in
try_with fn yield {
effc = fun (type a) (eff : a Effect.t) -> match eff with
| Yield x -> Some (fun (k : a k) -> handler x (k : unit k))
| _ -> None
}
``````

Usage:

``````let traverse xs yield = List.iter yield xs

let () =
with_yield (fun x k -> Format.printf "yielded %i@." x ; continue k ())
@@ traverse [ 1 ; 2 ; 3 ]

let () =
with_yield (fun x k -> Format.printf "yielded %C@." x ; continue k ())
@@ traverse [ 'a' ; 'b' ]
``````

The issue with this solution is that the `yield` effect must be passed explicitly to `traverse`â€¦ since we donâ€™t yet have imaginary syntax for typed effects to pass it implicitly and guarantee that the effect doesnâ€™t escape its handler scope (perhaps with a `local` mode on the `yield` parameter?):

``````   type 'a yield = 'a -> unit

val traverse : 'a list -> 'a yield -> unit
(* val traverse : 'a list  -['a yield]-> unit *)
``````

(It also makes it obvious that we can avoid effects entirely for this example:)

``````let () = traverse [ 1 ; 2 ; 3 ] (Format.printf "yielded %i@.")
let () = traverse [ 'a' ; 'b' ] (Format.printf "yielded %C@.")
``````
3 Likes

I like this! It highlights the thing Iâ€™ve been trying to do to answer the following

Well, rather â€śpassing the type manually to a properly polymorphic function, packaged in a module, instead of having it be automatically inferredâ€ť, that it is just a side-effect(ha) of our approaches in lifting the harder typing bits to the module system, and not fundamental to the effect typing problem.

I tried to answer that by playing with the ocaml-implicits PR and trying to retrieve both inference and effect-passig through that path, but this is rather clean way to do it. Thanks :)!

Since Kokaâ€™s `effect fun` / `with fun` is single-shot at the tail, expressing them in OCaml is pretty natural. Koka doesnâ€™t even expose the continuation (instead youâ€™d use `effect ctl` / `with ctl`). I also like the note about the equivalence of traverse in this instance to iter. Weâ€™re not really making use of the dynamic-binding facility of the effect.

The thing about extensible variants & functors made me wonder why the effects team went with this design (vs polymorphic variants, which at least to me are the first to come to mind when thinking about a nice way to stage the feature in its untyped version to later be typed). Itâ€™s obvious there was a rope to walk here, Iâ€™m just interested in the details of it all and the design process.