Return to Answer

You can get an important hint to solution by thinking how to make the yin-yang puzzle work in a typed language, see this question. OCaml computes the type of yin and yang to be ('a -> 'a) as 'a, which is a recursive type equal to its own function space. Such a type is precisely what it takes to implement the untyped $\lambda$-calculus in a typed language.

You can get an important hint to solution by thinking how to make the yin-yang puzzle work in a typed language, see this question. OCaml computes the type of yin and yang to be ('a -> 'a) as 'a, which is a recursive type equal to its own function space. Such a type is precisely what it takes to implement the untyped $\lambda$-calculus in a typed language.

Clearly, the let statements are just a convenience. Without them, and with 'callcc' expanded out, we get:

So the essence of the yin-yang puzzle is just self-application of self-application. How appropriate!

Clearly, the let statements are just a convenience. Without them, and with callcc expanded out, we get:

So the essence of the yin-yang puzzle is just self-application of self-application. How appropriate! As a last step, we can put in the print_char statements again, to get a one-liner:

(fun x -> x (fun k -> print_char '@'; x k)) (fun x -> x (fun k -> print_char '*'; x k)) (fun x -> x)

You can get an important hint from thinking about how to make the yin-yang puzzle work in a typed language, see this question. OCaml computes the type of yin and yang to be ('a -> 'a) as 'a, which is a recursive type equal to its own function space. Such a type is precisely what it takes to implement the untyped $\lambda$-calculus in a typed language.

You can compute the CPS transform in the privacy of your mind. I do not have the time right now, but will come back to complete the answer. The morale is that you should be able to do this just with $\lambda$-calculus.

You can get an important hint to solution by thinking how to make the yin-yang puzzle work in a typed language, see this question. OCaml computes the type of yin and yang to be ('a -> 'a) as 'a, which is a recursive type equal to its own function space. Such a type is precisely what it takes to implement the untyped $\lambda$-calculus in a typed language.

You can compute the CPS transform in the privacy of your mind. Here is my version, written in Ocaml. To run it, you need to pass -rectypes to Ocaml:

let callcc f k = f k ;;
let yin c = callcc (fun x -> x x) (fun k -> print_char '@'; c k) ;;
let yang c = callcc (fun x -> x x) (fun k -> print_char '*'; c k) ;;
let _  = yin yang (fun x -> x) ;;

Clearly, the let statements are just a convenience. Without them, and with 'callcc' expanded out, we get:

(fun c -> (fun x -> x x) (fun k -> print_char '@'; c k))
(fun c -> (fun x -> x x) (fun k -> print_char '*'; c k))
(fun x -> x)

We could remove the print_char statement and $\eta$-reduce:

1. Start with:

    (fun c -> (fun x -> x x) (fun k -> c k))
    (fun c -> (fun x -> x x) (fun k -> c k))
    (fun x -> x)
   

2. Reduce fun k -> c k to c:

    (fun c -> (fun x -> x x) c) (fun c -> (fun x -> x x) c) (fun x -> x)
   

3. Reduce fun c -> (fun x -> x x) c to fun x -> x x:

    (fun x -> x x) (fun x -> x x) (fun x -> x)
   

So the essence of the yin-yang puzzle is just self-application of self-application. How appropriate!