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.

Ungrounded

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.

Ungrounded

I attempted the this in SML but ran into the same limitation on recursive (circular) types. – Monica

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

Drouin

This is very cool but you have not used continuations, which are at the heart of the yin yang puzzle. Don't get me wrong, what you did is neat, it's just not the original puzzle. Instead you used the λ-calculus, as your solution can is rewritten with pure functions. C# does not really have first-class continuations, does it? Unfortunately, I cannot write the equivalent OCaml code here. Should I post it as a separate answer? – Ungrounded

I think it does use continuations. It just doesn’t use call-with-current-continuation, which C# doesn’t have. My program is what you get after the first transformation that a compiler would have to do to a program with call/cc. Just because it compiles away call/cc doesn’t mean that it compiles away continuations. – Drouin

Right. Still, while the original looks scary and confusing, this one looks just confusing :-) – Ungrounded

@AndrejBauer: Your question wasn’t about scariness or confusion, but whether “the puzzle makes sense in a typed language”. – Drouin

This discussion is pointless because it is largely a matter of opinion whether you've changed the puzzle "too much". In any case, the answer is, that the puzzle makes sense in a language with sufficiently recursive types (but then, anything makes sense in such a language). – Ungrounded

I think the term "continuation" is specific enough to claim that C# doesn’t actually have them. However, this answer clearly shows that a static type system would not get in the way, because the type of the continuation is easily definable in C#. – Rowland

Answer 3

_{See also my answer to how the yin yang puzzle works, which I had to figure out an answer to before I could answer this one.}

Being a "typed" language does not, by itself, make the difference to whether this puzzle is expressible in it (no matter how vague the term "typed language" is). However, to answer your question most literally: yes, it’s possible, because Scheme itself is a typed language: each value has a known type. This is obviously not what you meant, so I assume you mean whether this is possible in a language where each variable is assigned a permanent type that never changes (a.k.a. "statically typed language").

Moreover, I’ll assume that you want the spirit of the puzzle preserved when expressed in some language. Obviously it’s possible to write a Scheme interpreter in x86 machine code, and obviously it’s possible to write an x86 machine code interpreter in a typed language which only has integer data types and function pointers. But the result isn’t in the same "spirit". So to make this more precise, I will place an extra requirement: the result must be expressed using true continuations. Not an emulation, but real full-on continuations.

So, can you have a statically typed language with continuations? It turns out you can, but you might still call it cheating. For example, in C#, if my continuations were defined as "function that takes an object and returns an object", where "object" is a type that can hold anything at all, will you find this acceptable? What if the function takes and returns a "dynamic"? What if I have a "typed" language where every function has the same static type: "function", without defining the types of arguments and return types? Is the resulting program still in the same spirit, even though it uses true continuations?

My point is that the "statically typed" property still allows for a huge amount of variation in the type system, enough to make all the difference. So just for fun, let’s consider what the type system would need to support in order to qualify as non-cheating by any measure.

The operator call/cc(x) can also be written as x(get/cc), which is much easier to comprehend in my opinion. Here, x is a function that takes a Continuation and returns a value, while get/cc returns a Continuation. Continuation has all traits of a function; it can be called with one argument, and will sort of substitute the value passed in to wherever get/cc that created it was originally located, additionally resuming execution at that point.

This means that get/cc has an awkward type: it’s a function, but the very same location will eventually return a value whose type we don’t know yet. Suppose however, that in the spirit of statically-typed languages, we require the return type to be fixed. That is, when you call the continuation object, you can only pass in values of a predefined type. With this approach, the type of the continuation function can be defined with the recursive expression of the form T = function T->T. As pointed out by a friend, this can type actually be declared in C#: public delegate T T(T t);!

So there you have it; being "typed" does not preclude nor guarantee that you can express this puzzle without altering its nature. However, if you allow for the static type "can be anything" (known as object in Java and C#), then the only other thing you need is support for true continuations, and the puzzle can be represented no problem.

---

Approaching the same question from a different perspective, consider my rewrite of the puzzle into something more reminiscent of a traditional statically-typed imperative language, which I explained in the linked answer:

yin = (function(arg) { print @; return arg; })(get-cc);
yang = (function(arg) { print *; return arg; })(get-cc);
yin(yang);

Here, the type of yin and yang never changes. They always store a "continuation C that takes a C and returns a C". This is very much compatible with static typing, whose only requirement is that the type doesn’t change next time you execute that code.

Rowland

Thanks for a verbose answer, but you are not really answering my question. I explicitly asked about static typing a la ML. I thought I was clear enough about that in my question, but perhaps not. Javascript does not really add anything to the answer because, just like scheme, it is not statically typed. Translated into less verbose but more precise language, your answer is that we need the recursive type α = α → α. This is interesting as eff tells me the equation in question is α = α → β. Must α = β? – Ungrounded

@AndrejBauer Firstly, "explicitly" is definitely false :) And secondly, I am talking about a statically typed language; I am not talking about JavaScript. I did mention JS syntax once; I will remove that. – Rowland

What would be more explicit than "I am trying to write an equivalent piece of code in a typed language, such as SML/NJ, but it is giving me typing errors"? I suppose the word "static" is missing. Ok, I'll add it just to make you look bad ;-) Anyhow, it's not important. – Ungrounded

@AndrejBauer In my defense, I’ve never heard of that language, and "typing errors" can come up at runtime too :) Anyway, glad you’ve got your answer. – Rowland

You got the type right, it's α = α → α and not α = α → β, as reported by a typing error in eff. OCaml can compute the types, see my updated answer. Also, the correct conclusion is that the yin yang puzzle is essentially untyped in the sense that the types of yin and yang are the same as the types needed to give typing to the untyped λ-calculus. – Ungrounded

@AndrejBauer I guess that’s a matter of word definitions. As long as we think the same thing (it’s something that takes one like itself and returns one like itself) then it doesn’t matter which words you use to describe it... – Rowland

I think we're saying more or less the same thing, except that you're using informal terminology, while I am referring to exact mathematical concepts (recursive types). – Ungrounded