How to express Koka home page example?

Learning
1

On the Koka home page: The Koka Programming Language

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
2

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

3

Interesting, but it’s not exactly the same, right :slight_smile: The Koka yield effect can yield any value, not just int.

4

There’s no problem yielding values of any type, but then you cannot simply use Printf.printf to print them :slight_smile:

Cheers,
Nicolas

5

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.

6

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
7

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
8

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 :')

For anyone curios, it was this:

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
9

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.

10

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
11

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.