Added more code about searchability, and added more comments

Natinfi.hs

@@ -2,24 +2,36 @@
 
 import Control.Monad.Instances
 import Coalgebra
+import Search
 
 -- F X = 1 + X
 type F = Maybe
 
 -- This will give the fixpoint, ie a coalgebra, because F is a functor
+-- There is an element for every natural number, and an infinity element
 type Natinfi = Nu F
 
--- The semantics from the following coalgebra to Natinfi is "the selection function" (I hope)
+-- The semantics from the following coalgebra to Natinfi is "the selection function"
 -- In some sense this behaviour searches through all natural numbers
+-- (searching for a witness x such that p x = True, in contrast to the paper)
 instance Coalgebra F (Natinfi -> Bool) where
 	psi p
-		| p (phi Nothing) == False = Nothing
+		| p (phi Nothing) == True = Nothing
 		| otherwise = Just (\x -> p $ phi $ Just x)
 
--- On "numbers" bigger that one, return True
-test :: Natinfi -> Bool
-test p = case q of
-		Nothing -> True
+-- http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ says:
+-- "What is going on here is that computable functionals are continuous"
+-- In this case Natinfi is compact, so any computable predicate is known when we only inverstigate at depth n (for some n)
+-- Hence forsome and others will always terminate.
+test1 :: Natinfi -> Bool
+test1 p = case q of
+		Nothing -> False
+		Just y -> True
+	where q = psi p
+
+test2 :: Natinfi -> Bool
+test2 p = case q of
+		Nothing -> False
 		Just y -> False
 	where q = psi p
 
@@ -30,6 +42,15 @@ toInt s = case q of
 		Just y -> 1 + toInt y
 	where q = psi s
 
+sNatinfi :: Searchable Natinfi
+sNatinfi = S (semantics :: (Natinfi -> Bool) -> Natinfi)
+
+output :: (Natinfi -> Bool) -> String
+output p
+	| forsome sNatinfi p == True = "There is an example, namely: " ++ (show $ toInt $ find sNatinfi p)
+	| otherwise = "For all elements p is false"
+
 main :: IO ()
 main = do
-	putStrLn $ show $ toInt $ (semantics test :: Natinfi)
+	putStrLn $ output test1
+	putStrLn $ output test2

Search.hs

@@ -0,0 +1,16 @@
+module Search where
+
+import Control.Monad.Instances
+import Coalgebra
+
+-- from http://math.andrej.com/2008/11/21/a-haskell-monad-for-infinite-search-in-finite-time/
+-- Here we search for elements x such that p x = True
+-- If there is none, it may lie
+newtype Searchable a = S {find :: (a -> Bool) -> a}
+
+search :: Searchable a -> (a -> Bool) -> Maybe a
+search xs p = let x = find xs p in if p x then Just x else Nothing
+
+forsome, forevery :: Searchable a -> (a -> Bool) -> Bool
+forsome xs p = p(find xs p)
+forevery xs p = not(forsome xs (\x -> not(p x)))