(* This file describe an isomorphism of types in OCaml between int -> int -> unit and int -> unit, obtained through game semantics.
Strictly speaking it is not an isomorphism in OCaml because the type int is bounded, however doing the same code with
unbounded integers such as with Big_int would yield an isomorphism. *)
(* First of all, we introduce a looping function, that will serve as the initial value for our higher-order reference *)
let loop () =
print_string "Entering infinite loop...";
let rec aux () = aux () in aux()
let empty n p = loop()
(* Here is the family of bijections between nN and N, where N is the set of natural numbers *)
let phi n i k =
n*k + i
let phiback n k =
let q = k/n and p = k mod n in (p, q)
(* Here is the first component of the isomorphism, going from int -> int -> unit to int -> unit *)
let iso f =
let count = ref(0) and func = ref(empty) in
fun n ->
let (p, q) = phiback (!count + 1) n in
if p = 0 then
let x = f q in
count := !count + 1;
let c = !count in
func := (let g = !func in
(fun n ->
if n = c then x
else g n))
else !func p q
(* Here is the second component, going from int -> unit back to int -> int -> unit *)
let isoback f =
let count = ref(0) in
fun n ->
(f (phi (!count + 1) 0 n);
count := !count +1;
let c = !count in
fun p ->
f (phi (!count + 1) c p))
let compose f g = fun x -> ((fun y -> f(y)) (g(x)));;
(* With this, we claim that (compose iso isoback) and (compose isoback iso) are both equivalent to the identity, i.e. that they
act as the identity in any context. We should have more tests here... Here is one. *)
let x = ((compose isoback iso) (fun n -> (print_int n; flush stdout); fun p -> (print_int (n+p); flush stdout))) 5 in x 6; x 7