*basically*is the same thing — because of what you

*can't*do with nat → bool. Contravariance is weird like that!

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