-- part 1 data Nat = Z | S Nat deriving (Eq, Ord, Show); num 0 = Z num n = S (num (n-1)) seven = num 7 inf = S inf -- part 2 -- not-equal (!=) is still semidecidable -- seven != infinity => True -- inf /= inf => no answer -- equal (==) is *not* semidecidable -- inf == inf => no answer -- less-than-infinity *is* semidecidable -- seven < inf => True -- inf < seven => False -- part 3 instance Num Nat where Z + b = b (S a) + b = S (a + b) Z * b = Z (S a) * b = b + (a * b) abs n = n signum Z = Z signum (S _) = S Z fromInteger = num -- now we can do some arithmetic -- notice in particular that we can calculate inf + seven -- or inf * seven -- and it delivers the right answer -- we can also answer questions like -- inf * seven> two -- returns True -- part 4 -- caution: DOES NOT WORK PROPERLY example p = if p Z then Z else S (example(p.S)) -- caution: DOES NOT WORK PROPERLY counterexample p = example (not . p) -- so for example -- very good isBig x = x> seven -- very good isSeven x = x == seven -- very good isSolution x = x*x + x == num 6 -- totally wrong isSolution' x = x*x + x == num 7 -- part 5 -- caution: DOES NOT WORK PROPERLY example p = if p Z then Z else S (example(p.S)) example p = tryFrom p Z tryFrom p x = if p x then x else tryFrom p (S x) -- caution: DOES NOT WORK PROPERLY counterexample p = example (not . p) -- so for example -- very good isBig x = x> seven -- very good isSeven x = x == seven -- very good isSolution x = x*x + x == num 6 -- totally wrong isSolution' x = x*x + x == num 7 -- this, however, works flawlessly exists p = p x where x = example p -- likewise forall p = p c where c = counterexample p isNotOneHalf x = x + x /= num 1 -- forall (\x -> not (x * x + x == num 7))