The thing that still has my brain in loops is that there is a definable, decidable equality on (nat → bool) → bool. Even though it's a function type! Even though — in fact, because — it's a crazy higher-order function type! This other post of his goes into some more detail about it.
I just had to translate the code over to ML to satisfy myself that it really works. It's instructive I think to see how Haskell's laziness winds up as explicit stream operations in ML.
signature S =
sig
type cantor
(* the main magic *)
val find : (cantor -> bool) -> cantor
val exists : (cantor -> bool) -> bool
val all : (cantor -> bool) -> bool
(* isomorphism of cantor with int -> bool *)
val nth : cantor -> (int -> bool)
val make : (int -> bool) -> cantor
(* equality testing *)
val equal : (cantor -> bool) -> (cantor -> bool) -> bool
(* some sample cantor predicates *)
val p1a : cantor -> bool
val p1b : cantor -> bool
val p2 : cantor -> bool
(* testing *)
val test : unit -> unit
end
structure M :> S =
struct
datatype front = @ of bool * cantor
withtype cantor = unit -> front
infix 1 @
fun find cp () =
let fun after x y = cp (fn () => (x @ y))
in
if exists (after false)
then false @ find (after false)
else true @ find (after true)
end
and exists p = p (find p)
and all p = not (exists (not o p))
fun nth c n = nth' (c()) n
and nth' (x @ c) 0 = x
| nth' (x @ c) n = nth c (n-1)
fun make' f = (f(0) @ make (fn x => f(x+1)))
and make f () = make' f
fun equal f g = all (fn a => (f a : bool) = g a)
fun p1a c = nth c 2 andalso (false orelse nth c 0)
fun p1b c = nth c 2 andalso nth c 0
fun p2 c = nth c 2 andalso nth c 1
fun test () =
let
fun runtest t b =
print (if t() = (b : bool)
then "Passed!\n"
else "Failed!\n")
in
runtest (fn () => equal p1a p1b) true;
runtest (fn () => equal p1a p1a) true;
runtest (fn () => equal p1a p2) false;
runtest (fn () => equal p1b p2) false;
runtest (fn () => equal p2 p2) true;
()
end
end