Jason (jcreed) wrote,
Jason
jcreed

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: andrej, constructive, equality, logic, streams
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 13 comments