Everone's favorite Ljubljanian logician, Andrej Bauer, made a fascinatingly counterintuitive blog post about the type (nat → bool) → bool. There's more stuff you can do there than you think, if you're a die-hard intuitionist — or a computer scientist, which 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
```

Tags:
• #### (no subject)

Had a good bunch of discussions with Sean and Alyssa at work. Supposed to be stupid hot this weekend when we were planning to do the final cleanup of…

• #### (no subject)

Started moving some stuff into the new place in Astoria! Basically just books, but pretty much all our books made it there. Made a Zipcar reservation…

• #### (no subject)

Got lease signed! Movin' to Astoria imminently, I guess. Restaurant situation seems incredibly good over there.

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic