Does the yin yang continuations puzzle make sense in a typed language?

Question

This question is related to "How the yin-yang puzzle works?". The yin yang example of continuations in scheme looks like this, according to Wikipedia article:

(let* ((yin      ((lambda (cc) (display #\@) cc) (call-with-current-continuation (lambda (c) c))))    (yang      ((lambda (cc) (display #\*) cc) (call-with-current-continuation (lambda (c) c))))) (yin yang)) 

I am trying to write an equivalent piece of code in a (edit: statically) typed language, such as SML/NJ, but it is giving me typing errors. So either the puzzle does not type, or I am misunderstanding the scheme syntax. What would the above piece of code look like in SML or Ocaml (with callcc extension)?

By the way, what is the source of the puzzle? Where did it come from?

Edit: I think I know the answer. We need a recursive type t satisfying t = t -> s for some type s.

Edit of edit: No it is not, the answer is a recursive type t satisfying t = t -> t.

Answer 1

I think I am going to answer my own question. I will show two solutions, one in eff and another in Ocaml.

eff

We are going to work with eff (I am blowing my own horn here, see below for another way in OCaml with Oleg's delimcc extension.) The solution is explained in the paper Programming with algebric effects and continuations.

First we define shift and reset in eff:

type ('a, 'b) delimited = effect   operation shift : (('a -> 'b) -> 'b) -> 'a end  let rec reset d = handler   | d#shift f k -> with reset d handle (f k) ;; 

Here is the yin yang puzzle transcribed into eff:

let y = new delimited in   with reset y handle     let yin = (fun k -> std#write "@" ; k) (y#shift (fun k -> k k)) in     let yang = (fun k -> std#write "*" ; k) (y#shift (fun k -> k k)) in       yin yang 

But eff complains about it that it can't solve the type equation α = α → β. At present eff cannot handle arbitrary recursive types, so we are stuck. As a way of cheating, we can turn off type checking to see if at the very least the code does what it is supposed to:

$ eff --no-types -l yinyang.eff @*@**@***@****@*****@******@*******@********@*********@*******... 

Ok, it's doing the right thing, but the types are not powerful enough.

OCaml

For this example we need Oleg Kiselyov's delimcc library. The code is as follows:

open Delimcc ;;  let y = new_prompt () in   push_prompt y (fun () ->     let yin = (fun k -> print_string "@" ; k) (shift y (fun k -> k k)) in     let yang = (fun k -> print_string "*" ; k) (shift y (fun k -> k k)) in       yin yang) 

Again, Ocaml won't compile because it hits a recursive type equation. But with the -rectypes option we can compile:

ocamlc -rectypes -o yinyang delimcc.cma yinyang.ml 

It works as expected:

$ ./yinyang @*@**@***@****@*****@******@*******@********@*********@... 

OCaml computes that the type of yin and yang is ('a -> 'a) as 'a, which is its way of saying "a type α such that α = α → α". This is precisely the type characteristic of the untyped λ-calculus models. So there we have it, the yin yang puzzle essentially uses features of the untyped λ-calculus.

Answer 2

It is possible to declare a recursive functional type in C#, a statically-typed language:

delegate Continuation Continuation(Continuation continuation); 

This definition is equivalent to ML’s α : α → α.

Now we can “translate” the yin-yang puzzle into C#. This does require a transformation for the call/cc, and we need to do the transformation twice because there are two of them in it, but the result still looks very much like the original and still has a yin(yang) call in it:

Continuation c1 = cc1 => {     Continuation yin = new Continuation(arg => { Console.Write("@"); return arg; })(cc1);     Continuation c2 = cc2 =>     {         Continuation yang = new Continuation(arg => { Console.Write("*"); return arg; })(cc2);         return yin(yang);     };     return c2(c2); }; c1(c1); 

Clearly now, the variable yang is only in local scope, so we can actually optimise it away:

Continuation c1 = cc1 => {     Continuation yin = new Continuation(arg => { Console.Write("@"); return arg; })(cc1);     Continuation c2 = cc2 => yin(new Continuation(arg => { Console.Write("*"); return arg; })(cc2));     return c2(c2); }; c1(c1); 

Now, we realise that those little inline functions really just output a character and otherwise do nothing, so we can unwrap them:

Continuation c1 = cc1 => {     Console.Write("@");     Continuation yin = cc1;     Continuation c2 = cc2 =>     {         Console.Write("*");         return yin(cc2);     };     return c2(c2); }; c1(c1); 

Finally, it becomes clear that the variable yin is redundant too (we can just use cc1). To preserve the original spirit though, rename cc1 to yin and cc2 to yang and we get our beloved yin(yang) back:

Continuation c1 = yin => {     Console.Write("@");     Continuation c2 = yang =>     {         Console.Write("*");         return yin(yang);     };     return c2(c2); }; c1(c1); 

All of the above are the same program, semantically. I think the end-result is a fantastic C# puzzle in itself. So I would answer your question by saying: yes, clearly it makes a lot of sense even in a statically-typed language :)